mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x✝ : ↥{a, b}
x : α
hx : x ∈ {a, b}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
      obtain rfl | rfl := hx
      · exact ⟨0, rfl⟩
      · exact ⟨1, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv y

Tactic:
simp only [← e.tgt_eq]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: case e'_2.e'_6
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_3✝ : nerveEquiv (nerveEquiv.symm x₀) = x₀
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
⊢ homEquiv (edgeMk f₀₁) = f₀₁

Tactic:
apply homEquiv_edgeMk

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
e_5✝ : nerveEquiv (nerveEquiv.symm x₂) = x₂
⊢ homEquiv (edgeMk f₁₂) = f₁₂

Tactic:
apply homEquiv_edgeMk

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
⊢ homEquiv (edgeMk f₀₂) = f₀₂

Tactic:
apply homEquiv_edgeMk

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
A : Δ[n].Subcomplex
x : ↑(Δ[n].nonDegenerate d)
⊢ ↑(nonDegenerateEquiv'.symm (nonDegenerateEquiv' x)) ∈ A.obj (op ⦋d⦌) ↔ face ↑(nonDegenerateEquiv' x) ≤ A

Tactic:
face_nonDegenerateEquiv' x,

Goal state after:
n d : ℕ
A : Δ[n].Subcomplex
x : ↑(Δ[n].nonDegenerate d)
⊢ ↑(nonDegenerateEquiv'.symm (nonDegenerateEquiv' x)) ∈ A.obj (op ⦋d⦌) ↔ Subcomplex.ofSimplex ↑x ≤ A
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i j =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
by
        rcases j with (_ | _ | j) <;> cases i <;> aesop

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
ComplexShape.σ_ε₂ c₁ c₁₂ i₁ h₂,

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂' * c₂.ε₁ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₁ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
HomologicalComplex₂.d₁_eq _ _ h₃ _ _ (by rw [← h, ComplexShape.next_π₁ c₂ c h₃]),

Goal state after:
case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (i₁, i₂) •
        ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ (c₁.next i₁)).f i₂ ≫
          (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c (c₁.next i₁) i₂ (c.next j) ⋯) ≫
      hom₁ h₁ f₂ F c (c.next j) j
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom q' (-p)).op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
obtain rfl : q' = -q := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
hp : p + -p = 0
hq : q + -q = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom (-q) (-p)).op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : CochainComplex C ℤ} (x : X ≅ Y), CochainComplex.plus C X → CochainComplex.plus C Y

Tactic:
rintro _ _ e ⟨n, _⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : CochainComplex C ℤ
e : X✝ ≅ Y✝
n : ℤ
h✝ : X✝.IsStrictlyGE n
⊢ CochainComplex.plus C Y✝
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0

Tactic:
← assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl) ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl) ≫ s.π - g ≫ biprod.inr ≫ s.π = 0

Tactic:
← assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl) ≫ s.π - (g ≫ biprod.inr) ≫ s.π = 0
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom q' (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom

Tactic:
obtain rfl : q' = -q := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q : ℤ
hp : p + -p = 0
hq : q + -q = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ ¬c.Rel j i

Tactic:
by rwa [← e.rel_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : (cofibrations C).IsStableUnderCobaseChange
hf : Cofibration f
⊢ Cofibration (pushout.inr f g)

Tactic:
rw [cofibration_iff] at hf ⊢
  exact MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g).flip hf

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
⊢ (functor r).IsLocalization W

Tactic:
apply Functor.IsLocalization.mk'

Goal state after:
case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
⊢ Localization.StrictUniversalPropertyFixedTarget (functor r) W (Quotient r)

case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
⊢ Localization.StrictUniversalPropertyFixedTarget (functor r) W W.Localization
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hX : A.op X✝
hY : B.op Y✝
⊢ ∃ Z a b, A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hX : A.op X✝
hY : B.op Y✝
Z : C
a : unop Y✝ ⟶ Z
b : Z ⟶ unop X✝
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.unop
⊢ ∃ Z a b, A.op Z ∧ B.op Z ∧ a ≫ b = f
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
t : TStructure C
inst✝ : P.IsTriangulated
h : P.HasInducedTStructure t
A : P.FullSubcategory
⊢ ∃ X Y, ∃ (_ : t.le 0 X.obj) (_ : t.ge 1 Y.obj), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
by
    obtain ⟨X, Y, hX, hY, f, g, h, hT, ⟨X', hX', ⟨e⟩⟩, ⟨Y', hY', ⟨e'⟩⟩⟩ :=
      h.exists_triangle_zero_one A.1 A.2
    exact ⟨⟨X', hX'⟩, ⟨Y', hY'⟩, (t.le 0).prop_of_iso e hX.le,
      (t.ge 1).prop_of_iso e' hY.ge,
      P.fullyFaithfulι.preimage (e.inv ≫ f),
      P.fullyFaithfulι.preimage (g ≫ e'.hom),
      P.fullyFaithfulι.preimage (e'.inv ≫ h ≫ e.hom⟦(1 : ℤ)⟧' ≫
          (P.ι.commShiftIso (1 : ℤ)).inv.app ⟨X', hX'⟩),
      isomorphic_distinguished _ hT _ (Triangle.isoMk _ _ e.symm (Iso.refl _) e'.symm)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsGE (P.ι.mapTriangle.obj (((P.tStructure t).triangleLEGE n₀ n₁ h).obj { obj := T.obj₂, property := h₂ })).obj₃ n₁

Tactic:
dsimp; rw [← P.tStructure_isGE_iff]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
φ : T.obj₂ ⟶ T'.obj₂
a✝ b : ℤ
h₀ : t.IsLE T.obj₁ a✝
h₁' : t.IsGE T'.obj₃ b
h : a✝ < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
c : T.obj₃ ⟶ T'.obj₃
comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂
comm₃ : T.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T'.mor₃
⊢ ∃ f, f.hom₂ = φ

Tactic:
exact ⟨{ hom₁ := a, hom₂ := φ, hom₃ := c }, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
sq :
  CommSq (f ≫ iResolutionObj Y) (iResolutionObj X) (terminal.from (resolutionObj Y)) (terminal.from (resolutionObj X))
⊢ ∃ g, iResolutionObj X ≫ g = f ≫ iResolutionObj Y

Tactic:
exact ⟨sq.lift, sq.fac_left⟩

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)

Tactic:
← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)

Tactic:
← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁))) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
Equivalence.counitInv_app_functor,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              H₃.map (eL.functor.map (eL.unit.app (L₁.obj X₁))) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ (w.structuredArrowDownwards (Opposite.unop X₂)).map
        (StructuredArrow.homMk (StructuredArrow.Hom.right φ.unop).left.unop ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f')).left)
          (StructuredArrow.right (Opposite.unop f')).hom.unop (StructuredArrow.hom (Opposite.unop f')).left.unop ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left)
        (StructuredArrow.right (Opposite.unop f)).hom.unop (StructuredArrow.hom (Opposite.unop f)).left.unop ⋯)

Tactic:
ext
          exact Quiver.Hom.op_inj
            ((CostructuredArrow.proj _ _).congr_map (StructuredArrow.w φ.unop))

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map (Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = (isoOfHom L W₂ R.w ⋯).inv ≫ y

Tactic:
← assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ (L.map (Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv) ≫ y = (isoOfHom L W₂ R.w ⋯).inv ≫ y