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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (eqToHom ⋯).app x✝ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝) ≫
      (LaxMonoidal.ε (shiftMonoidalFunctor C A)).app (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝)

Tactic:
simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a } (MonoidalCategoryStruct.tensorUnit (Discrete A))).app 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
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤

Tactic:
rw [_root_.eq_top_iff]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ⊤ ≤ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).hom.app X =
    (shiftFunctor C 0).map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero C A).hom.app X

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_inv_app]

Goal state after:
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
r : R
x y : S
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
let : SMulZeroClass R S := inferInstance

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣r • x) = r • y𝖣x
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_4.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
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
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (Set.range fun x ↦ single ((algebraMap S B) ((algebraMap R S) x)) 1) ⊆ Set.range fun x ↦ single ((algebraMap S B) x) 1

Tactic:
exact Set.range_comp_subset_range (algebraMap R S)
    fun x => Finsupp.single (algebraMap S B x) (1 : B)

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.tmul.add
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
f✝ g✝ : A →₀ A
a✝¹ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) f✝)) = 0
a✝ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) g✝)) = 0
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (f✝ + g✝))) = 0

pp: case a.tmul.single
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
a✝ b✝ : A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (single a✝ b✝))) = 0

Tactic:
· simp [smul_add, *]

Goal state after:
case a.tmul.single
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
a✝ b✝ : A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (single a✝ b✝))) = 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)
i : ι
⊢ biprod.inl.f i ≫ biprod.snd.f i = 0

Tactic:
rw [← comp_f, biprod.inl_snd, zero_f]

Goal state after:
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₁₂
⊢ z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), sub_v, comp_sub]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Tactic:
by
  obtain rfl : e = d := by lia
  rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]

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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : (ComplexShape.up ℤ).Rel j i
⊢ i + -1 = j

Tactic:
dsimp at hij

Goal state after:
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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
⊢ i + -1 = j
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
    (↑(Cocycle.mk (Cochain.mk fun p q hpq ↦ homotopyCofiber.fstX φ p q hpq) 2 fst._proof_2 ⋯)).v i j hij ≫ φ.f j +
      homotopyCofiber.sndX φ i ≫ G.d i j

Tactic:
apply homotopyCofiber.d_sndX

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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ≅ Arrow.mk φ'
⊢ mapArrowHom φ φ' H α.hom ≫ mapArrowHom φ' φ H α.inv = 𝟙 (homotopyCofiber φ)

Tactic:
by rw [← mapArrowHom_comp, Iso.hom_inv_id, mapArrowHom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
⊢ Linear R (Quotient r)

Tactic:
letI := Linear.module r hr
  exact
    { smul_comp := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ a f g
        obtain ⟨f, rfl⟩ := (functor r).map_surjective f
        obtain ⟨g, rfl⟩ := (functor r).map_surjective g
        rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
      comp_smul := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ f a g
        obtain ⟨f, rfl⟩ := (functor r).map_surjective f
        obtain ⟨g, rfl⟩ := (functor r).map_surjective g
        rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul] }

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
⊢ F.mapCochainComplexShiftIso (a + b) = CommShift.isoAdd (F.mapCochainComplexShiftIso a) (F.mapCochainComplexShiftIso b)

Tactic:
ext
    rw [CommShift.isoAdd_hom_app]
    dsimp
    rw [id_comp, id_comp]
    simp only [CochainComplex.shiftFunctorAdd_hom_app_f,
      CochainComplex.shiftFunctorAdd_inv_app_f, HomologicalComplex.XIsoOfEq, eqToIso,
      eqToHom_map, eqToHom_trans, eqToHom_refl]

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

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
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n a n' : ℤ
hn' : n + a = n'
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
⊢ (fun γ ↦ γ.leftShift a n' hn') ((fun γ ↦ γ.leftUnshift n hn') γ) = γ

Tactic:
simp only [leftShift_leftUnshift]

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ (δ n m γ).v (p + a) q ⋯

Tactic:
δ_v n m hnm _ (p + a) q (by lia) (p + n') (p + 1 + a) (by lia) (by lia),

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫
          (γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q + m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ (F ⋙ G).map ((shiftFunctorAdd C a b).hom.app X) ≫
      e.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map
              ((commShiftIso H a).hom.app X ≫
                (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)) ≫
            (commShiftIso G b).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).inv.app (F.obj X)) =
    G.map (F.map ((shiftFunctorAdd C a b).hom.app X)) ≫
      e.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map (e.inv.app ((shiftFunctor C a).obj X) ≫ G.map ((OfComp.iso e a).hom.app X)) ≫
            (commShiftIso G b).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).inv.app (F.obj X))

Tactic:
congr 4

Goal state after:
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ (shiftFunctor E b).map
      ((commShiftIso H a).hom.app X ≫ (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)) =
    (shiftFunctor E b).map (e.inv.app ((shiftFunctor C a).obj X) ≫ G.map ((OfComp.iso e a).hom.app X))
Module: Mathlib.CategoryTheory.Triangulated.Functor

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
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
F : C ⥤ D
inst✝¹¹ : F.CommShift ℤ
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasZeroObject D
inst✝⁸ : Preadditive C
inst✝⁷ : Preadditive D
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
inst✝² : F.IsTriangulated
inst✝¹ : F.Full
inst✝ : F.Faithful
T : Triangle C
hT : F.mapTriangle.obj T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
mem : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
⊢ F.mapTriangle.obj T ≅ F.mapTriangle.obj (Triangle.mk T.mor₁ g h)

Tactic:
exact isoTriangleOfIso₁₂ _ _ hT (F.map_distinguished _ mem)
    (Iso.refl _) (Iso.refl _) (by simp)

Goal state after:
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
F : D ⥤ E
⊢ ((whiskeringLeft W.Localization D E).obj (equivalenceFromModel L W).functor ⋙
          (Construction.whiskeringLeftEquivalence W E).functor).obj
      F =
    (whiskeringLeftFunctor L W E).obj F

Tactic:
ext
      change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
      rw [Construction.fac]

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
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
⊢ ∀ ⦃X Y : W.Localization⦄ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f

Tactic:
by
      intro X Y f
      simpa only [← this] using! MorphismProperty.top_apply f

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
⊢ 𝟭 (W.Localization ⥤ D) = functor W D ⋙ inverse W D

Tactic:
by
      refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_
      · apply uniq
        simp [functor, inverse, fac]
      · apply natTrans_hcomp_injective
        ext X
        simp

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

Goal state before:
pp: case mp
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ W.Q.map f = W.Q.map g → L.map f = L.map g

pp: case mpr
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ L.map f = L.map g → W.Q.map f = W.Q.map g

Tactic:
· intro h
    let e := Localization.compUniqFunctor W.Q L W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]

Goal state after:
case mpr
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ L.map f = L.map g → W.Q.map f = W.Q.map g
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z : W.LeftFraction X Y
⊢ W (z.s ≫ 𝟙 z.Y')

Tactic:
by simpa only [Category.comp_id] using z.hs

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac L₁ h W₁.Q
this✝¹ : CatCommSq Φ.functor W₁.Q L₂ (G ⋙ F) := { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this✝ : G.Full
this : G.Faithful
⊢ L₁.IsLocalization W₁

Tactic:
have : G.EssSurj :=
    ⟨fun X ↦ ⟨W₁.Q.obj (L₁.objPreimage X), ⟨e.app _ ≪≫ L₁.objObjPreimageIso X⟩⟩⟩

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac L₁ h W₁.Q
this✝² : CatCommSq Φ.functor W₁.Q L₂ (G ⋙ F) := { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this✝¹ : G.Full
this✝ : G.Faithful
this : G.EssSurj
⊢ L₁.IsLocalization W₁
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ add' W (neg' W f) f = L.map 0

Tactic:
obtain ⟨α, rfl⟩ := exists_leftFraction L W f

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map ((L.objObjPreimageIso X).hom ≫ (f ≫ (L.objObjPreimageIso Y).inv + g ≫ (L.objObjPreimageIso Y).inv)) =
    G.map (L.objObjPreimageIso X).hom ≫
      (G.map f ≫ G.map (L.objObjPreimageIso Y).inv + G.map g ≫ G.map (L.objObjPreimageIso Y).inv)
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
← add_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
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map ((L.objObjPreimageIso X).hom ≫ (f + g) ≫ (L.objObjPreimageIso Y).inv) =
    G.map (L.objObjPreimageIso X).hom ≫
      (G.map f ≫ G.map (L.objObjPreimageIso Y).inv + G.map g ≫ G.map (L.objObjPreimageIso Y).inv)
⊢ G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map ((L.objObjPreimageIso X).hom ≫ (f + g) ≫ (L.objObjPreimageIso Y).inv) =
    G.map (L.objObjPreimageIso X).hom ≫
      (G.map f ≫ G.map (L.objObjPreimageIso Y).inv + G.map g ≫ G.map (L.objObjPreimageIso Y).inv)
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
← add_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
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map ((L.objObjPreimageIso X).hom ≫ (f + g) ≫ (L.objObjPreimageIso Y).inv) =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
⊢ G.Additive

Tactic:
refine ⟨fun {X Y f g} => ?_⟩
      have hL := essSurj L W
      have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
      rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
      rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
h : P ≤ Q
⊢ P ≤ Q ⊔ ⨆ a, Q.strictLimitsOfShape (J a) ∧
    ∀ (i : α), P.strictLimitsOfShape (J i) ≤ Q ⊔ ⨆ a, Q.strictLimitsOfShape (J a)

Tactic:
exact ⟨h.trans le_sup_left, fun a ↦
    (strictLimitsOfShape_monotone (J a) h).trans <|
      le_iSup (fun a ↦ Q.strictLimitsOfShape (J a)) a |>.trans le_sup_right⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨i, ⟨x, hx⟩⟩ => ⟨x, ⋯⟩

Tactic:
rintro ⟨_, h⟩

Goal state after:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ
val✝ : X
h : (⨆ i, P i) val✝
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, ⟨x, hx⟩⟩ => ⟨x, ⋯⟩)
        a =
      ⟨val✝, h⟩