More random widget experiments I guess

Changes

1 changed files (+31/-0)

• LaTeX.lean
  • @@ -1,3 +1,6 @@
    + import Mathlib.Tactic.Widget.CommDiag + import ProofWidgets.Component.Panel.GoalTypePanel + import ProofWidgets.Component.Panel.SelectionPanel import ProofWidgets.Component.HtmlDisplay open scoped ProofWidgets.Jsx
  • @@ -15,3 +18,31 @@ open ProofWidgets in
    I @= p \\end{CD}$$ "} /> + + + universe u + namespace CategoryTheory + open ProofWidgets + + /-- Local instance to make examples work. -/ + local instance : Category (Type u) where + Hom α β := α → β + id _ := id + comp f g := g ∘ f + id_comp _ := rfl + comp_id _ := rfl + assoc _ _ _ := rfl + + example {f g : Nat ⟶ Bool} : f = g → (f ≫ 𝟙 Bool) = (g ≫ 𝟙 Bool) := by + with_panel_widgets [GoalTypePanel] + intro h + exact h + + example {X Y Z : Type} {f i : X ⟶ Y} + {g j : Y ⟶ Z} {h : X ⟶ Z} : + h = f ≫ g → + i ≫ j = h → + f ≫ g = i ≫ j := by + with_panel_widgets [SelectionPanel] + intro h₁ h₂ + rw [← h₁, h₂]