mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.LeftInverse (⇑(derivationQuotKerTotal R S).liftKaehlerDifferential)
    ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun

Tactic:
intro x

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : (S →₀ S) ⧸ kerTotal R S
⊢ (derivationQuotKerTotal R S).liftKaehlerDifferential
      (((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun x) =
    x
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.RightInverse (⇑(derivationQuotKerTotal R S).liftKaehlerDifferential)
    ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun

Tactic:
intro x

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : Ω[S⁄R]
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential x) =
    x
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
· obtain rfl := c.next_eq' h
    exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
x✝ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
h₁ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i
h₂ : f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
⊢ f = g

Tactic:
← cancel_mono (𝟙 _)

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
x✝ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
h₁ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i
h₂ : f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
⊢ f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra A B
inst✝ : Algebra S B
⊢ RingHom.ker (algebraMap A B) • ⊤ ≤ (kerToTensor R A B).ker

Tactic:
Submodule.smul_eq_map₂

Goal state after:
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra A B
inst✝ : Algebra S B
⊢ Submodule.map₂ (LinearMap.lsmul A ↥(RingHom.ker (algebraMap A B))) (RingHom.ker (algebraMap A B)) ⊤ ≤
    (kerToTensor R A B).ker
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i i' : ι
w : c.Rel i i'
⊢ (dNext i) f = C.d i i' ≫ f i' i

Tactic:
obtain rfl := c.next_eq' w
  rfl

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i) ≫ D.d i j + 0 = C.d i j ≫ (dNext j) hom + C.d i j ≫ hom j i ≫ D.d i j

Tactic:
eq2,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i) ≫ D.d i j + 0 = 0 + C.d i j ≫ hom j i ≫ D.d i j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (z₂ + z₂') h).v p q hpq = (z₁.comp z₂ h + z₁.comp z₂' h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by lia), add_v, comp_add]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hj : ¬c.Rel j (c.next j)
⊢ (desc φ α hα).f j = sndX φ j ≫ α.f j

Tactic:
by
  apply dif_neg hj

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝⁴ x✝³ x✝² : ℤ
x✝¹ : (ComplexShape.up ℤ).Rel x✝⁴ x✝³
x✝ : (ComplexShape.up ℤ).Rel x✝³ x✝²
⊢ AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁴ x✝³) ≫ AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝³ x✝²) = 0

Tactic:
by ext; simp [δ_δ]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
⊢ (i 0).symm = isoZero F A

Tactic:
ext X
        dsimp
        simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]

Goal state after:
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 : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
⊢ BinaryBiproductData T.obj₁ T.obj₃

Tactic:
exact
    { bicone :=
      { pt := T.obj₂
        fst := fst
        snd := T.mor₂
        inl := T.mor₁
        inr := inr
        inl_fst := by
          simp only [← cancel_mono T.mor₁, assoc, id_comp, eq, comp_sub, comp_id,
            comp_distTriang_mor_zero₁₂_assoc _ hT, zero_comp, sub_zero]
        inl_snd := comp_distTriang_mor_zero₁₂ _ hT
        inr_fst := by
          simp only [← cancel_mono T.mor₁, assoc, eq, comp_sub, reassoc_of% inr_snd,
            comp_id, sub_self, zero_comp]
        inr_snd := inr_snd }
      isBilimit := isBinaryBilimitOfTotal _ total }

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

Goal state before:
pp: case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ Quiver.Path.nil) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) Quiver.Path.nil

Tactic:
rw [Category.comp_id]
      rfl

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

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ F = G

Tactic:
by
  fapply Functor.ext
  · intro X
    rw [h_obj]
  · intro X Y f
    induction f with
    | nil => erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
    | cons g e ih =>
      erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
      simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]

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

Goal state before:
pp: case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (p.cons g))

Tactic:
rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]

Goal state after:
case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map g.toPath)
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).Full

Tactic:
whiskeringLeftFunctor'_eq

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 ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Full
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).Faithful

Tactic:
whiskeringLeftFunctor'_eq

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 ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful
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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (L.objObjPreimageIso Y).hom = F₁.map (L.objObjPreimageIso Y).hom ≫ τ'.app Y

Tactic:
τ'.naturality,

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ.app (L.obj (L.objPreimage Y)) ≫ F₂.map (L.objObjPreimageIso Y).hom =
    τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (L.objObjPreimageIso Y).hom
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')

Tactic:
by
  obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)
  dsimp at fac
  have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
    rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
  obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
  simp only [assoc] at fac'
  refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
  · simp only [comp₀, assoc, reassoc_of% fac]
  · simp only [comp₀, assoc, fac']
  · simp only [comp₀, assoc, ← reassoc_of% fac]
    exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ.inl
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
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀

Tactic:
rw [transfiniteIterate_succ _ _ _ hk']

Goal state after:
case succ.inl
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
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: case mp
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ → HasCardinalLT X κ ∧ HasCardinalLT Y κ

pp: case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ

Tactic:
· intro h
    exact ⟨h.of_injective _ Sum.inl_injective,
      h.of_injective _ Sum.inr_injective⟩

Goal state after:
case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT Y κ → HasCardinalLT (X ⊕ Y) κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
⊢ HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ

Tactic:
hasCardinalLT_sum_iff _ _ _ hκ

Goal state after:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
⊢ HasCardinalLT (Subtype P₁) κ ∧ HasCardinalLT (Subtype P₂) κ
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 (p₂.s ≫ u)

Tactic:
· dsimp [p₁, p₂]
        simp only [assoc]
        exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs (W.comp_mem _ _ w₂.hs hu))

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : P ≤ Q
⊢ P.shiftClosure A ≤ Q.shiftClosure A

Tactic:
by
  rintro X ⟨Y, a, i, hY⟩
  refine ⟨Y, a, i, h Y hY⟩

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

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
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang

Tactic:
obtain ⟨φ, ⟨e⟩⟩ : ∃ (φ : Arrow C), Nonempty (L.mapArrow.obj φ ≅ Arrow.mk f) :=
    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

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
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ F₁.map ((Q W).map f.f ≫ Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f ≫ Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
F₁.map_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ F₁.map ((Q W).map f.f) ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f ≫ Qinv f.s ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.Triangulated

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
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)

Tactic:
by
      rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
      rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp,
        Functor.map_comp, assoc, MorphismProperty.LeftFraction.map_comp_map_s_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
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
X : C
⊢ ∀ {Y : C} (x : X ≅ Y), P.extensionProduct Q X → P.extensionProduct Q Y

Tactic:
X'

Goal state after:
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
X X' : C
⊢ ∀ (x : X ≅ X'), P.extensionProduct Q X → P.extensionProduct Q X'
Module: Mathlib.Algebra.Homology.ShortComplex.Retract

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : QuasiIso f₂
⊢ QuasiIso f₁

Tactic:
by
  rw [quasiIso_iff] at hf₂ ⊢
  have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
    { i := Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left))
        (v := homologyMap (show T₁ ⟶ T₂ from h.i.right)) (by simp [← homologyMap_comp])
      r := Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left))
        (v := homologyMap (show T₂ ⟶ T₁ from h.r.right)) (by simp [← homologyMap_comp])
      retract := by ext <;> simp [← homologyMap_comp] }
  exact (MorphismProperty.isomorphisms C).of_retract h hf₂

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (shiftFunctor (DerivedCategory C) n).Additive

Tactic:
Localization.functor_additive_iff
    Qh (HomotopyCategory.subcategoryAcyclic C).trW

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (Qh ⋙ shiftFunctor (DerivedCategory C) n).Additive