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

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (integralClosure (↥S) A).toSubring ≤ T ↔ ofClass S ≤ T

Tactic:
rw [integralClosure_le_iff, Subtype.forall, SetLike.le_def]

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ∀ ⦃x : A⦄, x ∈ ofClass S → x ∈ T
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x

Tactic:
exact isIntegral_iff.mp hx

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ eval₂ (algebraMap R K) y (X ^ n - C x) = 0

Tactic:
simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ (algebraMap R K) b ^ n / (algebraMap R K) a ^ n - (algebraMap R K) x = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
⊢ #ℍ[R,c₁,c₂,c₃] = #R ^ 4

Tactic:
by
  rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]
  simp only [mk_prod, lift_id]
  ring

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

Goal state before:
pp: case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ shiftₗ M G h - 1 = shiftₗ M G h + -1

Tactic:
simp only [sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ Δ_[1]^[n] (j.choose i • fun r ↦ r ^ i) = 0

Tactic:
rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi),

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • 0) x = 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(s / t) ≤ #↑s * #↑t

Tactic:
rw [← image2_div]; exact Cardinal.mk_image2_le

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x✝ x : M
h : x ∈ Set.range f
⊢ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x✝ x : M
h : x ∈ Set.range f
⊢ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
⊢ ∃ y, x * y ∈ s

Tactic:
induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Finset β
ht : t.Nonempty
⊢ 0 ⊆ 0 • t

Tactic:
simpa [mem_smul] using! ht

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
⊢ ∀ (a : ↥(MonoidHom.mrange f)), a ≠ 0 → a * ⟨(↑a)⁻¹, ⋯⟩ = 1

Tactic:
rintro ⟨a, ha⟩ h
    simp only [ne_eq, Subtype.ext_iff] at h
    simpa using mul_inv_cancel₀ h

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkHom
        {
          toFun := fun x ↦
            match x with
            | 0 => i.castSucc
            | 1 => i.succ,
          monotone' := ⋯ } ≫
      mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun x ↦
          match x with
          | 0 => ⟨j + ↑i, ⋯⟩.castSucc
          | 1 => ⟨j + ↑i, ⋯⟩.succ,
        monotone' := ⋯ }

Tactic:
ext (i : Fin 2)

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ mkHom
        {
          toFun := fun x ↦
            match x with
            | 0 => 0
            | 1 => Fin.last l,
          monotone' := ⋯ } ≫
      mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun x ↦
          match x with
          | 0 => ⟨j, ⋯⟩
          | 1 => ⟨j + l, ⋯⟩,
        monotone' := ⋯ }

Tactic:
ext (i : Fin 2)

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

pp: case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

pp: case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

pp: case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
any_goals simp

Goal state after:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False
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 ⋯ ≫ δ 0

Tactic:
dsimp% δ_comp_σ_of_le (i := 0) (j := j) (by simp),

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 ⋯ ≫ σ j ≫ δ 0 = σ j' ≫ δ₀Iter i ⋯ ≫ δ 0
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
⊢ {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u} ⊆
    ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u}

Tactic:
rintro _ ⟨f, rfl⟩
    exact ⟨f ≫ g, by simp⟩

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

Goal state before:
pp: case neg
X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
this : ∀ (i : Fin d), Finite ↑(X.nonDegenerate ↑i)
x : X.N
hj : ¬x.dim < d
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

Tactic:
have := x.nonDegenerate
      simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d x.dim (by simpa using hj)] at this

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

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex = (N.mk ↑z ⋯).subcomplex

Tactic:
exact subcomplex_eq_of_epi _ _ f rfl

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ StrictMono s.obj

Tactic:
obtain _ | n := n

Goal state after:
case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ s ∈ (nerve X).nonDegenerate 0 ↔ StrictMono s.obj

case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ (Hom.toOrderHom (objEquiv x)) i₁ ≤ (Hom.toOrderHom (objEquiv x)) i₂

Tactic:
exact OrderHom.monotone _ h

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

Goal state before:
pp: case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
⊢ Hom.toOrderHom f₁ = Hom.toOrderHom f₂

Tactic:
rw [← OrderHom.range_eq_iff h₁ h₂]

Goal state after:
case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
⊢ Set.range ⇑(Hom.toOrderHom f₁) = Set.range ⇑(Hom.toOrderHom f₂)
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ ρ₁₂.q (i₁₂, i₃) = j

Tactic:
by rw [← h₁₂, ← h, ← ρ₁₂.hpq]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j =
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
dsimp [mapBifunctorComp₁₂MapObjIso]
  apply CofanMapObjFun.ιMapObj_iso_inv

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

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

Tactic:
op_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (f.f (-n)).op =
    (((dNext (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
          (prevD (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op +
      (g.f (-n)).op
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

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

Tactic:
op_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (f.f (-n)).op =
    ((dNext (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op +
        ((prevD (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op +
      (g.f (-n)).op
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ c₁.π c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j

Tactic:
rw [← h, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃)
Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKInjective
inst✝ : L.IsKInjective
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
  rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
  obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
  refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
  · simp [hg]
  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
hi : ¬c.Rel i (c.next i)
hi' : c'.Rel (e.f i) (c'.next (e.f i))
⊢ (dNext (e.f i)) h.hom = (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
hi : ¬c.Rel i (c.next i)
hi' : ¬c'.Rel (e.f i) (c'.next (e.f i))
⊢ (dNext (e.f i)) h.hom = (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv

Tactic:
· simp [dNext_eq _ hi', extend_d_from_eq_zero _ _ _ _ _ rfl hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
hi : ¬c.Rel i (c.next i)
hi' : ¬c'.Rel (e.f i) (c'.next (e.f i))
⊢ (dNext (e.f i)) h.hom = (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv