mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ a ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (F ⋙ forget AddCommGrpCat) X X ≫ (F ⋙ forget AddCommGrpCat).map μ

Tactic:
Preadditive.mul_def X,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (F ⋙ forget AddCommGrpCat) X X ≫
        (F ⋙ forget AddCommGrpCat).map (SemiCartesianMonoidalCategory.fst X X + SemiCartesianMonoidalCategory.snd X X)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc 0 p
⊢ x ∈ Ioc 0 (0 + p)

Tactic:
rwa [zero_add]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f (0 + p)

Tactic:
rwa [zero_add]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))

Tactic:
rwa [zero_add]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
← comp_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (S.v₀₁ ≫ S.v₁₂).τ₁ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
← comp_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (S.v₁₂ ≫ S.v₂₃).τ₁ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
let x₂' := x₁ ≫ S.L₁.f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.single
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ (sum (single f' r ≫ single g' s) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (single g' s).sum fun f' r ↦ r • F.map f'

Tactic:
rw [single_comp_single _ _ f' g' r s]
        simp [mul_comm r s, mul_smul]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ S₁.v₂₃.τ₁ ≫ f.f₃.τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ

Tactic:
← comp_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ (S₁.v₂₃ ≫ f.f₃).τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.right b))) x =
    (hom (limit.π I.multicospan (WalkingMulticospan.right b))) y

Tactic:
← limit.w I.multicospan (WalkingMulticospan.Hom.fst b),

Goal state after:
case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      x =
    (hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      y
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
i : J.R
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))

Tactic:
have a := x.2 (WalkingMulticospan.Hom.fst i)
      have b := x.2 (WalkingMulticospan.Hom.snd i)
      rw [← b] at a
      exact a

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case false.false
property✝ : (false, false) ∈ {x | x.1 < x.2}
⊢ ⟨(false, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case false.true
property✝ : (false, true) ∈ {x | x.1 < x.2}
⊢ ⟨(false, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case true.false
property✝ : (true, false) ∈ {x | x.1 < x.2}
⊢ ⟨(true, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case true.true
property✝ : (true, true) ∈ {x | x.1 < x.2}
⊢ ⟨(true, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))

Tactic:
rw [← AddCommGrpCat.mono_iff_injective]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget₂ C Ab).map f)
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom S.g).ker = (ConcreteCategory.hom S.f).range

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (moduleCatMkOfKerLERange f g ⋯).Exact

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using! hfg

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
hij' : i ≤ j
k : ℕ
hk : i + k = j
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij

Tactic:
exact this k i j hk (by valid)

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
⊢ HasEqualizer f g

Tactic:
by
  let := IsCoreflexivePair.mk' r fr gr
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)

Tactic:
cases h

Goal state after:
case left.reflexion.left
⊢ (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)

case left.reflexion.right
⊢ (Hom.left.comp Hom.reflexion).comp Hom.right = Hom.left.comp (Hom.reflexion.comp Hom.right)

case left.reflexion.leftCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.leftCompReflexion)

case left.reflexion.rightCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.rightCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.rightCompReflexion)

case left.reflexion.id
⊢ (Hom.left.comp Hom.reflexion).comp (Hom.id one) = Hom.left.comp (Hom.reflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)

Tactic:
cases h

Goal state after:
case left.id.reflexion
⊢ (Hom.left.comp (Hom.id zero)).comp Hom.reflexion = Hom.left.comp ((Hom.id zero).comp Hom.reflexion)

case left.id.id
⊢ (Hom.left.comp (Hom.id zero)).comp (Hom.id zero) = Hom.left.comp ((Hom.id zero).comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case right.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)

Tactic:
cases h

Goal state after:
case right.reflexion.left
⊢ (Hom.right.comp Hom.reflexion).comp Hom.left = Hom.right.comp (Hom.reflexion.comp Hom.left)

case right.reflexion.right
⊢ (Hom.right.comp Hom.reflexion).comp Hom.right = Hom.right.comp (Hom.reflexion.comp Hom.right)

case right.reflexion.leftCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.right.comp (Hom.reflexion.comp Hom.leftCompReflexion)

case right.reflexion.rightCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.rightCompReflexion =
    Hom.right.comp (Hom.reflexion.comp Hom.rightCompReflexion)

case right.reflexion.id
⊢ (Hom.right.comp Hom.reflexion).comp (Hom.id one) = Hom.right.comp (Hom.reflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case right.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)

Tactic:
cases h

Goal state after:
case right.id.reflexion
⊢ (Hom.right.comp (Hom.id zero)).comp Hom.reflexion = Hom.right.comp ((Hom.id zero).comp Hom.reflexion)

case right.id.id
⊢ (Hom.right.comp (Hom.id zero)).comp (Hom.id zero) = Hom.right.comp ((Hom.id zero).comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)

Tactic:
cases h

Goal state after:
case reflexion.left.reflexion
⊢ (Hom.reflexion.comp Hom.left).comp Hom.reflexion = Hom.reflexion.comp (Hom.left.comp Hom.reflexion)

case reflexion.left.id
⊢ (Hom.reflexion.comp Hom.left).comp (Hom.id zero) = Hom.reflexion.comp (Hom.left.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)

Tactic:
cases h

Goal state after:
case reflexion.right.reflexion
⊢ (Hom.reflexion.comp Hom.right).comp Hom.reflexion = Hom.reflexion.comp (Hom.right.comp Hom.reflexion)

case reflexion.right.id
⊢ (Hom.reflexion.comp Hom.right).comp (Hom.id zero) = Hom.reflexion.comp (Hom.right.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case reflexion.leftCompReflexion.left
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case reflexion.leftCompReflexion.right
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.right = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case reflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case reflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case reflexion.leftCompReflexion.id
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case reflexion.rightCompReflexion.left
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case reflexion.rightCompReflexion.right
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case reflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case reflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case reflexion.rightCompReflexion.id
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)

Tactic:
cases h

Goal state after:
case reflexion.id.left
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.left = Hom.reflexion.comp ((Hom.id one).comp Hom.left)

case reflexion.id.right
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.right = Hom.reflexion.comp ((Hom.id one).comp Hom.right)

case reflexion.id.leftCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case reflexion.id.rightCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case reflexion.id.id
⊢ (Hom.reflexion.comp (Hom.id one)).comp (Hom.id one) = Hom.reflexion.comp ((Hom.id one).comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)

Tactic:
cases h

Goal state after:
case leftCompReflexion.left.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.left.comp Hom.reflexion)

case leftCompReflexion.left.id
⊢ (Hom.leftCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.left.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)

Tactic:
cases h

Goal state after:
case leftCompReflexion.right.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.right).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.right.comp Hom.reflexion)

case leftCompReflexion.right.id
⊢ (Hom.leftCompReflexion.comp Hom.right).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.right.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case leftCompReflexion.leftCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case leftCompReflexion.leftCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case leftCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case leftCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case leftCompReflexion.leftCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case leftCompReflexion.rightCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case leftCompReflexion.rightCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case leftCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case leftCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case leftCompReflexion.rightCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)

Tactic:
cases h

Goal state after:
case leftCompReflexion.id.left
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.left)

case leftCompReflexion.id.right
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.right)

case leftCompReflexion.id.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case leftCompReflexion.id.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case leftCompReflexion.id.id
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.leftCompReflexion.comp ((Hom.id one).comp (Hom.id one))