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

Goal state before:
pp: 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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A))
        (kerTotal R A ⊔ Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
Submodule.map_sup,

Goal state after:
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A)) (kerTotal R A) ⊔
        Submodule.map (linearCombination A ⇑(D R A))
          (Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯ = Iso.refl (K.homology j)

Tactic:
ext : 1

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ (K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯).hom = (Iso.refl (K.homology j)).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

Tactic:
apply h

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₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂

Tactic:
by
  subst h₁; 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
⊢ ((dNext i) hom + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + (prevD j) hom)

Tactic:
have eq1 : prevD i hom ≫ D.d i j = 0 := by
      simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]

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
⊢ ((dNext i) hom + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + (prevD j) hom)
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
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
simp only [nullHomotopicMap']

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
simp only [nullHomotopicMap']

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
simp only [nullHomotopicMap']

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
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
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = 0

Tactic:
simp only [nullHomotopicMap']

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₀ = 0
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 : ι
hjk : c.Rel j (c.next j)
⊢ (inlX φ (c.next j) j hjk ≫
      if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j

Tactic:
dif_pos hjk,

Goal state after:
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 : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j) = hα.hom (c.next j) j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ ↑((Cocycle.equivHom F G) f₁) = ↑((Cocycle.equivHom F G) f₂)

Tactic:
exact h

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 : HomologicalComplex V c
g : C ⟶ D
e : HomotopyEquiv C D
hfg : Homotopy e.hom g
⊢ homotopyEquivalences V c g

Tactic:
exact ⟨e.copy hfg, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂

Tactic:
rintro X Y f g h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h✝ : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
⊢ (functor r ⋙ F₂).map f = (functor r ⋙ F₂).map g
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✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ ((shortComplexFunctor C c i).map f).τ₃ =
    (if c.Rel i (c.next i) then K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i)
        else f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ ((shortComplexFunctor C c i).obj L).g +
      ((shortComplexFunctor C c i).map g).τ₃

Tactic:
dsimp
    split_ifs with h
    · rw [ho.comm (c.next i)]
      dsimp [dFrom, dTo, fromNext, toPrev]
      rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]
    · abel

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
⊢ Functor.Linear R (functor r)

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.tacticLet__
   "let"
   (Term.letConfig [])
   (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" (Term.app `linear [`R `r `hr]))))
  ";"
  (Tactic.exact
   "exact"
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])

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 : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
by
  ext p q hpq
  dsimp
  simp only [shift_v', units_smul_v]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (map φ φ (𝟙 K) (𝟙 L) ⋯).f n = (𝟙 (mappingCone φ)).f n

Tactic:
simp [ext_from_iff _ (n + 1) n rfl, map]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
n : ℤ
⊢ (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯).f n = (map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm').f n

Tactic:
simp [ext_from_iff _ (n + 1) n rfl, map]

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

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
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : Preadditive D
inst✝³ : HasBinaryBiproducts D
K✝ L✝ : CochainComplex C ℤ
φ : K✝ ⟶ L✝
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
G : C ⥤ D
inst✝ : G.Additive
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
K L : CochainComplex C ℤ
f : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh f
⊢ (G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
exact ⟨_, _, _, ⟨(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.mapIso e ≪≫
      CochainComplex.mappingCone.mapTrianglehIso f G⟩⟩

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

Goal state before:
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
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
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
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
a✝ : F₂.IsTriangulated
this : NatTrans.CommShift e.symm.hom ℤ
⊢ F₁.IsTriangulated

Tactic:
exact isTriangulated_of_iso e.symm

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f ≫ (mappingConeHomOfDegreewiseSplitIso S σ).inv).f n =
    (-mappingCone.inr (homOfDegreewiseSplit S σ)).f n

Tactic:
have h := (σ (n + 1)).f_r

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
h : (S.map (eval C (ComplexShape.up ℤ) (n + 1))).f ≫ (σ (n + 1)).r = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (n + 1))).X₁
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f ≫ (mappingConeHomOfDegreewiseSplitIso S σ).inv).f n =
    (-mappingCone.inr (homOfDegreewiseSplit S σ)).f n
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 ℤ
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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : C ⥤ D
inst✝¹ : F.CommShift ℤ
inst✝ : F.IsTriangulated
⊢ F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₂ ≫ F.map h.m₁ =
    F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ ≫ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂

Tactic:
simpa using F.congr_map h.comm₁

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
⊢ L₂.IsLocalization W

Tactic:
by
  have h := Localization.inverts L₁ W
  rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h
  let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)
  let F₂ := Localization.Construction.lift L₂ h
  exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

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

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
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁ = F₂

Tactic:
suffices F₁.rightOp = F₂.rightOp by
      rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]

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
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁.rightOp = F₂.rightOp
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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩

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
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : (Φ.functor ⋙ L₂).IsLocalization W₁
this : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)
⊢ Φ.IsLocalizedEquivalence

Tactic:
exact IsLocalizedEquivalence.mk' Φ (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.map Φ.functor.asEquivalence.functor

Tactic:
exact h

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (iso L W F F' a).hom.app (L.obj X) =
    F'.map ((commShiftIso L a).inv.app X) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X) ≫
        (commShiftIso F a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Tactic:
by
  simp [commShiftOfLocalization.iso]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (iso L W F F' a).inv.app (L.obj X) =
    (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
      (commShiftIso F a).inv.app X ≫
        (Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X) ≫ F'.map ((commShiftIso L a).hom.app X)

Tactic:
by
  simp [commShiftOfLocalization.iso]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
⊢ CommShift (Lifting.iso L W F F').hom A

Tactic:
by
  let := Functor.commShiftOfLocalization L W A F F'
  constructor
  intro a
  ext X
  simp only [comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app,
    Functor.commShiftIso_comp_hom_app,
    Functor.commShiftOfLocalization_iso_hom_app,
    Category.assoc, ← Functor.map_comp, ← Functor.map_comp_assoc,
    Iso.hom_inv_id_app, Functor.map_id, Iso.inv_hom_id_app,
    Category.comp_id, Category.id_comp, Functor.comp_obj]

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

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
inst✝² : L.IsLocalization W
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ L.map φ.fst.f = L.map φ.snd.f

Tactic:
apply h

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
inst✝² : L.IsLocalization W
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ F.map (L.map φ.fst.f) = F.map (L.map φ.snd.f)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
κ' : Cardinal.{v}
hκ' : κ ≤ κ'
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ'

Tactic:
by simpa only [Cardinal.lift_le] using hκ'

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ LeftFractionRel f g

Tactic:
rw [← homMk_eq_iff_leftFractionRel, homMk_eq, homMk_eq]

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯

Tactic:
exact h

Goal state after: