mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = e₂.hom
| e₂.hom ≫ T₂.mor₂

Tactic:
← eq,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = e₂.hom
| h.choose.hom.hom₂ ≫ T₂.mor₂
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₁ = e₁.hom
| T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom

Tactic:
← eq,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₁ = e₁.hom
| T₁.mor₃ ≫ (shiftFunctor C 1).map h.choose.hom.hom₁
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = (Triangle.π₃.mapIso h.choose).hom ≫ T₂.mor₃

Tactic:
have eq := h.choose_spec.1
    dsimp at eq ⊢
    conv_lhs => rw [← eq, TriangleMorphism.comm₃]

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

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : (of V).obj v ⟶ b) (q : u ⟶ v), P p → P ((of V).map q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
⊢ P f

Tactic:
induction k generalizing f a with

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Epi ((opcyclesFunctor C c i).mapShortComplex.obj S).g

Tactic:
by
    have := hS.epi_g
    dsimp
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f₁ f₂ : { obj := X } ⟶ { obj := Y }
r : relations W f₁ f₂
⊢ (liftToPathCategory G hG).map f₁ = (liftToPathCategory G hG).map f₂

Tactic:
rcases r with ⟨⟩

Goal state after:
case id
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ : C
X Y : Paths (LocQuiver W)
⊢ (liftToPathCategory G hG).map (ψ₁ W (𝟙 X✝)) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))

case comp
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝¹ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y✝¹
⊢ (liftToPathCategory G hG).map (ψ₁ W (f✝ ≫ g✝)) = (liftToPathCategory G hG).map (ψ₁ W f✝ ≫ ψ₁ W g✝)

case Winv₁
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
w✝ : X✝ ⟶ Y✝
hw✝ : W w✝
⊢ (liftToPathCategory G hG).map (ψ₁ W w✝ ≫ ψ₂ W w✝ hw✝) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))

case Winv₂
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
w✝ : X✝ ⟶ X✝¹
hw✝ : W w✝
⊢ (liftToPathCategory G hG).map (ψ₂ W w✝ hw✝ ≫ ψ₁ W w✝) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝¹))
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful

Tactic:
apply @Functor.Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).Faithful

C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X

Tactic:
← eq,

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ τ₁.app (W.Q.obj X.as.obj) = τ₂.app (W.Q.obj X.as.obj)
Module: Mathlib.CategoryTheory.Localization.Equivalence

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_4, u_4} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X

Tactic:
ext
  dsimp [equivalence, Equivalence.mk]
  rw [liftNatTrans_app]
  dsimp [Lifting.iso]
  rw [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
⊢ ∀ (a : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z), LeftFractionRel b₁ b₂ → a.comp b₁ = a.comp b₂

Tactic:
rintro a b₁ b₂ ⟨U, t₁, t₂, hst, hft, ht⟩

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
⊢ a.comp b₁ = a.comp b₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_1.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z✝
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s
Z : C
p : u.Y' ⟶ Z
hp : W p
fac₄ : z₁.f ≫ w₁.f ≫ u.f ≫ p = z₂.f ≫ w₂.f ≫ u.s ≫ p
⊢ W ((b₁.s ≫ z₁.s) ≫ w₁.f ≫ u.f ≫ p)

Tactic:
simp only [assoc]

Goal state after:
case refine_1.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z✝
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s
Z : C
p : u.Y' ⟶ Z
hp : W p
fac₄ : z₁.f ≫ w₁.f ≫ u.f ≫ p = z₂.f ≫ w₂.f ≫ u.s ≫ p
⊢ W (b₁.s ≫ z₁.s ≫ w₁.f ≫ u.f ≫ p)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_1.refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
Z : C
u : w₁.Y' ⟶ Z
hu : W u
fac₃ : z₁.f ≫ w₁.s ≫ u = t₁ ≫ w₁.f ≫ u
⊢ (b.s ≫ z₁.s) ≫ w₁.s ≫ u = (b.s ≫ z₁.s ≫ w₁.s) ≫ u

Tactic:
simp only [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_1.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
Z : C
u : w₁.Y' ⟶ Z
hu : W u
fac₃ : z₁.f ≫ w₁.s ≫ u = t₁ ≫ w₁.f ≫ u
⊢ W ((b.s ≫ z₁.s) ≫ w₁.s ≫ u)

Tactic:
simp only [assoc]

Goal state after:
case refine_2.refine_1.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
Z : C
u : w₁.Y' ⟶ Z
hu : W u
fac₃ : z₁.f ≫ w₁.s ≫ u = t₁ ≫ w₁.f ≫ u
⊢ W (b.s ≫ z₁.s ≫ w₁.s ≫ u)
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
⊢ ⊤ ≤ φ ⊤

Tactic:
φtop

Goal state after:
case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
⊢ ⊤ ≤ ⊤
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : Cardinal.mk T₁ < κ
h₂ : Cardinal.mk T₂ < κ
⊢ Cardinal.mk (T₁ × T₂) < κ
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_2.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
q : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : z₂.s ≫ w₂.s ≫ q.s = z₁.s ≫ w₁.s ≫ q.f
eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s
Z : C
u : q.Y' ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f ≫ q.f ≫ u = t₁ ≫ w₂.f ≫ q.s ≫ u
⊢ W (p₁.s ≫ q.f ≫ u)

Tactic:
simp only [p₁, assoc, ← reassoc_of% fac₃]
        exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
          (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_3.refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
Z : C
u : w₂.Y' ⟶ Z
hu : W u
fac₄ : z₂.f ≫ w₂.s ≫ u = t₂ ≫ w₂.f ≫ u
⊢ (b.s ≫ z₂.s ≫ w₂.s) ≫ u = (b.s ≫ z₂.s) ≫ w₂.s ≫ u

Tactic:
simp only [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_3.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
Z : C
u : w₂.Y' ⟶ Z
hu : W u
fac₄ : z₂.f ≫ w₂.s ≫ u = t₂ ≫ w₂.f ≫ u
⊢ W ((b.s ≫ z₂.s ≫ w₂.s) ≫ u)

Tactic:
simp only [assoc]

Goal state after:
case refine_2.refine_3.refine_3
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
Z : C
u : w₂.Y' ⟶ Z
hu : W u
fac₄ : z₂.f ≫ w₂.s ≫ u = t₂ ≫ w₂.f ≫ u
⊢ W (b.s ≫ z₂.s ≫ w₂.s ≫ u)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
⊢ { Y' := z.Y', f := f.f ≫ z.f, s := g.s ≫ z.s, hs := ⋯ }.map F hF = f.map F hF ≫ g.map F hF

Tactic:
have := hF _ g.hs

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this : IsIso (F.map g.s)
⊢ { Y' := z.Y', f := f.f ≫ z.f, s := g.s ≫ z.s, hs := ⋯ }.map F hF = f.map F hF ≫ g.map F hF
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.Nonempty
inst✝ : Q.Nonempty
⊢ (P.extensionProduct Q).Nonempty

Tactic:
obtain ⟨Y, f, g, hT⟩ := distinguished_cocone_triangle₂ (0 : Q.arbitrary ⟶ P.arbitrary⟦(1 : ℤ)⟧)
  exact ⟨_, _, _, _, _, _, hT, P.prop_arbitrary, Q.prop_arbitrary⟩

Goal state after:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
hφφ' : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Tactic:
by
  rw [quasiIsoAt_iff_isIso_homologyMap] at hφ hφφ' ⊢
  rw [homologyMap_comp] at hφφ'
  exact IsIso.of_isIso_comp_left (homologyMap φ i) (homologyMap φ' i)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n m n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)

Tactic:
induction m with
  | zero => rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
  | succ m hm =>
    rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.ContainsZero
n m : ℕ
h : n ≤ m
⊢ P.extensionProductIter n ≤ P.extensionProductIter m

Tactic:
by
  induction m, h using Nat.le_induction
  case base => rfl
  case succ n m hnm h =>
    refine le_trans h ?_
    rw [extensionProductIter_succ]
    exact le_extensionProduct_right P

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.ContainsZero
⊢ P.isoClosure.trW.ContainsIdentities

Tactic:
exact ⟨fun X => ⟨_, _, _, contractible_distinguished X, prop_zero _⟩⟩

Goal state after: