mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 2 3 _proof_299 _proof_364 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 2 3 _proof_299 _proof_364 ≫
        eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 3 4 _proof_364 _proof_365 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 3 4 _proof_364 _proof_365 ≫
        eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
⊢ CreatesLimit K R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : PreservesLimitsOfShape J R
⊢ PreservesLimitsOfShape J (comonadicRightAdjoint R)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : PreservesLimitsOfShape J R
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) :=
  comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape._proof_1 R
⊢ PreservesLimitsOfShape J (comonadicRightAdjoint R ⋙ R)

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_480
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_482
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_484
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_486
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_488
⊢ 2 < 5 + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
⊢ HasLimit F

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_491
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_493
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_495
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_497
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_499
⊢ 3 < 5 + 1

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_502
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_504
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_506
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_508
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_510
⊢ 4 < 5 + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_513
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_515
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_517
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_519
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_521
⊢ 5 < 5 + 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 0 + 1 ≤ 5

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_450✝

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 1 + 1 ≤ 5

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ = 𝟙 F

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_451✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ = 𝟙 G

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : C ⥤ D
⊢ F.map s ≫ F.map f = 𝟙 (F.obj B)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : C ⥤ D
⊢ F.map s ≫ F.map g = 𝟙 (F.obj B)

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 2 + 1 ≤ 5

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map left ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map left

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map right ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map right

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map reflexion ≫ H.map e₁ = H.map e₀ ≫ (G ⋙ H).map reflexion

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_452✝

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 3 + 1 ≤ 5

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H = mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
rw [Cocone.w G left, Cocone.w G right]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R✝
inst✝³ : MulSemiringAction M R✝
inst✝² : MulSemiringAction N R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : MulSemiringAction M R
a : M
⊢ a • 1 = 1

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_364✝ _proof_453✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R
inst✝³ : MulSemiringAction M R
inst✝² : MulSemiringAction N R
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N R
x : M
y : N
z : Ideal R
⊢ (x • y) • z = x • y • z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
by

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 : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 4 + 1 ≤ 5

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
⊢ Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S

Tactic:
by

Goal state after: