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

Goal state before:
pp: case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

Tactic:
simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using! congr_arg (· * e j) hx₁

Goal state after:
Module: Mathlib.Algebra.Ring.Action.ConjAct

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ∀ (a : ConjAct Rˣ), a • 0 = 0

Tactic:
simp [units_smul_def]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
⊢ |v - (of v).convs n| ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
refine (abs_sub_convs_le not_terminatedAt_n).trans ?_

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0

Tactic:
rw [← this Finset.univ, he.prod_one_sub, zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix) x y
⊢ c x y

Tactic:
rw [matrix_eq_sum_single x, matrix_eq_sum_single y]

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix) x y
⊢ c (∑ i, ∑ j, single i j (x i j)) (∑ i, ∑ j, single i j (y i j))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype (Submodule.comap p.subtype ((f.genEigenspace μ) k))

Tactic:
Submodule.map_comap_eq,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = p.subtype.range ⊓ (f.genEigenspace μ) k
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x y : FreeSemigroup α
⊢ (x * y).length = x.length + y.length

Tactic:
simp [length, Nat.add_right_comm]

Goal state after:
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case zero
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
⊢ (-1) ^ 0 * a * b = (-1) ^ 0 * (a * b)

Tactic:
simp only [npow_zero, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s⁻¹ = #↑s

Tactic:
by
  rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderTop α
a b : α
⊢ ↑(Ici a * Ioi b) ⊆ ↑(Ioi (a * b))

Tactic:
simpa using Set.Ici_mul_Ioi_subset' _ _

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ ∑ k ∈ range n, P k * r ^ k) = 0

Tactic:
simp_rw [← sum_apply _ _ (fun i x ↦ P i * x ^ i), fwdDiff_iter_finsetSum, sum_fn, ← smul_eq_mul,
    ← Pi.smul_def, fwdDiff_iter_const_smul, ← sum_fn]

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (∑ c ∈ range n, P c • Δ_[1]^[n] fun i ↦ i ^ c) = 0
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ { X := X✝, p := 𝟙 X✝, idem := ⋯ }.p ≫ f ≫ { X := Y✝, p := 𝟙 Y✝, idem := ⋯ }.p = f

Tactic:
simp only [comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom

Tactic:
rw [id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp }.p = p.f

Tactic:
by rw [hp, p_comp p]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
by
  subst H
  rw [δ_comp_δ_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = i.castSucc
⊢ X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
by
  subst H
  rw [δ_comp_δ_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    (((SimplexCategory.Truncated.inclusion n).op.lanAdjunction C).unit.app ((truncation n).obj X))

Tactic:
lanAdjunction_unit

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.lanUnit.app ((truncation n).obj X))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ

Tactic:
by
  subst H
  rw [δ_comp_δ_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) hi ≫ SimplexCategory.σ j).op = X.map (SimplexCategory.δ₀Iter i ⋯).op

Tactic:
SimplexCategory.δ₀Iter_σ ..

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.δ₀Iter i ⋯).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ₀Iter (i + 1) ⋯

Tactic:
by
  dsimp [σ, σ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ δ₀Iter i ⋯ ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
δ₀Iter_succ ..,

Goal state after:
case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ δ₀Iter i ⋯ ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter i ⋯ ≫ δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.op.N
⊢ opObjEquiv x.simplex ∈ X.nonDegenerate x.dim

Tactic:
by simpa only [opObjEquiv_mem_nonDegenerate_iff] using x.nonDegenerate

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
⊢ ∃ hf₁, (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x

Tactic:
obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁

Goal state after:
X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
⊢ ∃ hf₁, (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mk
n : ℕ
⊢ Δ[n].Finite

Tactic:
exact finite_of_hasDimensionLT _ (n + 1) inferInstance

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
⊢ (↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ 0 = 𝟙 ((stdSimplex.obj Δ).left _⦋n⦌)

Tactic:
ext φ
    apply objEquiv.injective
    apply SimplexCategory.Hom.ext
    ext i : 2
    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
      objEquiv, Equiv.ulift, uliftFunctor]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
⊢ { f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } = 0

Tactic:
by
    ext i₂
    exact shape₁ i₁ i₁' h i₂

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
by_cases h : c₁.Rel i₁ (c₁.next i₁)
  · simp [totalAux.d₁_eq' _ c₁₂ h]
  · simp [d₁_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
by
  by_cases h : c₁.Rel i₁ (c₁.next i₁)
  · simp [totalAux.d₁_eq' _ c₁₂ h]
  · simp [d₁_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + y = n'
i₁✝ i₂✝ : ℤ
hi✝ : (up ℤ).π (up ℤ) (up ℤ) (i₁✝, i₂✝) = n'
⊢ (K.ιTotal (up ℤ) i₁✝ i₂✝ n' hi✝ ≫
      (K.totalDesc fun p q hpq ↦
          (p * y).negOnePow •
            (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) ≫
        ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) =
    K.ιTotal (up ℤ) i₁✝ i₂✝ n' hi✝ ≫ 𝟙 ((K.total (up ℤ)).X n')

Tactic:
simp only [ι_totalDesc_assoc, Linear.units_smul_comp, Category.assoc, ι_totalDesc,
      Linear.comp_units_smul, XXIsoOfEq_inv_ιTotal, smul_smul, Int.units_mul_self, one_smul,
      comp_id]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
⊢ (commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom ≫
      whiskerRight (F.map₂CochainComplex.flip.map g) (shiftFunctor (CochainComplex D ℤ) n) =
    (shiftFunctor (CochainComplex C₁ ℤ) n).whiskerLeft (F.map₂CochainComplex.flip.map g) ≫
      (commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom

Tactic:
ext K₁ d

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
K₁ : CochainComplex C₁ ℤ
d : ℤ
⊢ (((commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom ≫
              whiskerRight (F.map₂CochainComplex.flip.map g) (shiftFunctor (CochainComplex D ℤ) n)).app
          K₁).f
      d =
    (((shiftFunctor (CochainComplex C₁ ℤ) n).whiskerLeft (F.map₂CochainComplex.flip.map g) ≫
              (commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom).app
          K₁).f
      d
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : toHom (mk x) = 0
⊢ x ∈ coboundaries K L n

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : x ∈ coboundaries K L n
⊢ toHom (mk x) = 0

Tactic:
· simp only [coboundaries, exists_prop, AddSubgroup.mem_mk, AddSubmonoid.mem_mk,
      AddSubsemigroup.mem_mk, Set.mem_ofPred_eq]
    rw [toHom_mk, HomotopyCategory.quotient_map_eq_zero_iff] at h
    obtain ⟨γ, h⟩ := Cochain.equivHomotopy _ _ h.some
    simp only [Cochain.ofHom_zero, add_zero, Cocycle.equivHomShift_symm_apply,
      Cocycle.cochain_ofHom_homOf_eq_coe, Cocycle.rightShift_coe] at h
    exact ⟨n - 1, by simp, n.negOnePow • γ.rightUnshift _ (by lia),
      by simp [Cochain.δ_rightUnshift _ _ _ _ _ (zero_add n), smul_smul, ← h]⟩

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : x ∈ coboundaries K L n
⊢ toHom (mk x) = 0
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : ∃ X f h_1, ∃ (_ : Triangle.mk f h h_1 ∈ distinguishedTriangles), P X
⊢ Function.Bijective fun f ↦ f ≫ h

Tactic:
obtain ⟨Y₁, f, g, hT, hY₁⟩ := hh

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
⊢ Function.Bijective fun f ↦ f ≫ h
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Q.map (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom =
    𝟙 (Q.obj (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0))) ≫ Q.map (K.ιTruncLE 0) ≫ e₂.hom

Tactic:
rw [id_comp]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Q.map (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom = Q.map (K.ιTruncLE 0) ≫ e₂.hom
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasProduct A
inst✝¹ : HasProduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ ∏ᶜ A
b : Y ⟶ ∏ᶜ B
sq : CommSq t p (Limits.Pi.map f) b
⊢ sq.HasLift

Tactic:
have sq' (j : J) :
        CommSq (t ≫ Pi.π _ j) p (f j) (b ≫ Pi.π _ j) :=
      ⟨by rw [← Category.assoc, ← sq.w]; simp⟩
    exact ⟨⟨{ l := Pi.lift (fun j ↦ (sq' j).lift) }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.asEquivalence.functor.map i) (G.asEquivalence.functor.map p) ↔ HasLiftingProperty i p

Tactic:
rw [G.asEquivalence.toAdjunction.hasLiftingProperty_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i (G.asEquivalence.inverse.map (G.asEquivalence.functor.map p)) ↔ HasLiftingProperty i p
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p

Tactic:
#adaptation_note /-- Prior to nightly-2026-05-07, the next three lines were just
  ```
  simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
    ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
  ```
  This is a temporary repair, and authors/maintainers are encouraged to either find a better repair,
  or identify a minimal example of an underlying problem in Lean.
  -/
  change HasLiftingProperty (G.asEquivalence.functor.map i) (G.asEquivalence.functor.map p) ↔ _
  rw [G.asEquivalence.toAdjunction.hasLiftingProperty_iff]
  simp only [← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
  exact MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.inv.naturality p).symm)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : Q.i₀ ≫ sq.lift = i ≫ P.i₀
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f

Tactic:
simp [reassoc_of% this]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : Q.i₁ ≫ sq.lift = i ≫ P.i₁
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g

Tactic:
simp [reassoc_of% this]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
this :
  (HomotopyCategory.subcategoryAcyclic C).trW ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).mor₁ ↔
    HomotopyCategory.subcategoryAcyclic C ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).obj₃
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f

Tactic:
← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
this :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).mor₁ ↔
    HomotopyCategory.subcategoryAcyclic C ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).obj₃
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z) →
    ∃ Z g h, ∃ (_ : Triangle.mk f.hom g h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) Z

Tactic:
rintro ⟨Z, a, b, h, hZ⟩
    exact ⟨_, _, _, A.ι.map_distinguished _ h, Z.property, hZ⟩

Goal state after: