mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s} = minimalPrimes R

Tactic:
minimalPrimes_eq_minimals,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s} = {x | Minimal Ideal.IsPrime x}
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ≠ d
⊢ m ∈ c.divisors.erase d

Tactic:
exact mem_erase_of_ne_of_mem hm₂ hm₁

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)

Tactic:
by
  constructor
  · rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]
    exact Set.mem_image_of_mem _
  · rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]
    exact Set.mem_image_of_mem _

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ #{a | orderOf a = d} = φ d

Tactic:
by
  classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ 1 < orderOf g

Tactic:
refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩
    contrapose! h
    exact ⟨37, by simp [h]⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : n • MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
smul_def,

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : MulAut.conj n • MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

Tactic:
by
  refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
  · cases (finite_or_infinite M).symm
    · cases subsingleton_or_nontrivial N; · simp
      exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim
    cases (finite_or_infinite N).symm
    · cases subsingleton_or_nontrivial M; · simp
      rw [(MulEquiv.prodComm ..).isCyclic] at h
      exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim
    apply coprime_card_of_isCyclic_prod
  · let f := MonoidHom.snd M N
    let e : f.ker ≃* M := by
      rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv
    let _ := hM.commGroup; let _ := hN.commGroup
    rw [← e.isCyclic] at hM
    rw [← Nat.card_congr e.toEquiv] at h
    exact isCyclic_of_coprime_card_ker f h Prod.snd_surjective

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
refine exists_subgroup_card_pow_prime _ ?_

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ Nat.card G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P

Tactic:
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
  rw [← (P.subtype _).coe_coe, coe_subtype,
    normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer),
    ← subgroupOf_normalizer_eq (le_normalizer.trans le_normalizer)] at this
  exact le_antisymm (this normal_in_normalizer) le_normalizer

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r = 0

Tactic:
rw [← Submodule.mem_bot R, ← h_ne_zero i]

Goal state after:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBy R M a ↔ torsionBy R M a = ⊤

Tactic:
← torsionBySet_singleton_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBy R M a ↔ torsionBySet R M {a} = ⊤
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ x ∈ ⨆ i ∈ S, torsionBySet R M ↑(p i)

Tactic:
mem_iSup_finset_iff_exists_sum

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ∃ μ, ∑ i ∈ S, ↑(μ i) = x
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ N' = N

Tactic:
sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ ⊥ • N' = N
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ a • (mk (R ∙ a * b)) x = 0

Tactic:
obtain ⟨c, h⟩ := h
    rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i)) = F.submodule.toAddSubmonoid

Tactic:
apply le_antisymm
  · rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]
    rintro i _ ⟨m, hm, rfl⟩ j
    rw [coeff_single, Finsupp.single_apply]
    split_ifs with h
    · rwa [← h]
    · exact (F.N j).zero_mem
  · intro f hf
    rw [← f.ofCoeff_coeff, ← f.coeff.sum_single, ofCoeff_finsuppSum]
    apply AddSubmonoid.sum_mem _ _
    rintro c -
    exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ ∀ (i : ℕ), I ≤ I ^ i

Tactic:
rintro (_ | n)

Goal state after:
case neg.zero
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ I ^ 0

case neg.succ
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
n : ℕ
⊢ I ≤ I ^ (n + 1)
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
⊢ Derivation.postcomp (derivation' φ') { app := fun X ↦ (d'.app X).desc, naturality := ⋯ } = d'

Tactic:
by
      ext X b
      apply ModuleCat.Derivation.desc_d

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(Submodule.restrictScalars S (ideal R S))

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
⊢ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
have : x - TensorProduct.lmul' (S := S) R x ⊗ₜ[R] (1 : S) = x := by
      rw [hx, TensorProduct.zero_tmul, sub_zero]

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
this : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 = x
⊢ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(ideal R S)

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

Tactic:
change _ - _ ∈ I

Goal state after:
case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
⊢ 1 ⊗ₜ[R] x - x ⊗ₜ[R] 1 ∈ I
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝ x : S
hx : x ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ∀ (x y : S),
    x ∈ adjoin R ↑(EssFiniteType.finset R S) →
      y ∈ adjoin R ↑(EssFiniteType.finset R S) →
        (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x + y) ∈ Submodule.span S ↑s

pp: case refine_4
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝ x : S
hx : x ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ∀ (x y : S),
    x ∈ adjoin R ↑(EssFiniteType.finset R S) →
      y ∈ adjoin R ↑(EssFiniteType.finset R S) →
        (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x * y) ∈ Submodule.span S ↑s

Tactic:
· exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy

Goal state after:
case refine_4
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝ x : S
hx : x ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ∀ (x y : S),
    x ∈ adjoin R ↑(EssFiniteType.finset R S) →
      y ∈ adjoin R ↑(EssFiniteType.finset R S) →
        (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x * y) ∈ Submodule.span S ↑s
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_3
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
⊢ (map R A B B).ker = Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

Tactic:
rw [KaehlerDifferential.ker_map]
      congr 1
      convert! Submodule.comap_id _
      · ext; simp

Goal state after:
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)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : ↥({i ∈ x.support | (algebraMap A B) i = c})
⊢ x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c ↔ ↑i ∈ {i ∈ x.support | (algebraMap A B) i = c}

Tactic:
simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]

Goal state after:
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)
⊢ (kerCotangentToTensor R A B).range = Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
by
  classical
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]
  · intro hx
    obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
    obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
    replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
    rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
    obtain ⟨x, hx, rfl⟩ := hx
    simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]
    rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
    simp only [map_sum (s := x.support.image (algebraMap A B)),
      TensorProduct.tmul_sum]
    apply sum_mem
    intro c _
    simp only [LinearMap.mem_range]
    simp only [map_sum, Finsupp.linearCombination_single]
    have : ∑ i ∈ x.support with algebraMap A B i = c, x i ∈ RingHom.ker (algebraMap A B) := by
      simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finsetSum_apply, RingHom.mem_ker,
        Finsupp.single_apply, ← Finset.sum_filter] using DFunLike.congr_fun hx c
    obtain ⟨a, ha⟩ := h c
    use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
    · simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
      simp_rw [← TensorProduct.tmul_smul]
      -- TODO: was `simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum,
        ← Finset.sum_smul, Finset.sum_attach, sub_eq_self,
        Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]
      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
    · have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
· apply ext_to_X _ _ _ hj
      · simp [d_fstX φ _ _ _ hij]
      · simp [d_sndX φ _ _ hij]

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j
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 : ℤ
α β : Cochain F G n
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
by_cases h : n + 1 = m

Goal state after:
case pos
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 : ℤ
α β : Cochain F G n
h : n + 1 = m
⊢ δ n m (α + β) = δ n m α + δ n m β

case neg
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 : ℤ
α β : Cochain F G n
h : ¬n + 1 = m
⊢ δ n m (α + β) = δ n m α + δ n m β
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 : ℤ
r : R
a : Cochain F G n
⊢ δ n m (r • a) = (RingHom.id R) r • δ n m a

Tactic:
by_cases h : n + 1 = m

Goal state after:
case pos
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 : ℤ
r : R
a : Cochain F G n
h : n + 1 = m
⊢ δ n m (r • a) = (RingHom.id R) r • δ n m a

case neg
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 : ℤ
r : R
a : Cochain F G n
h : ¬n + 1 = m
⊢ δ n m (r • a) = (RingHom.id R) r • δ n m a
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 : Cocycle F G n
m : ℤ
⊢ δ n m ↑z = 0

Tactic:
by_cases h : n + 1 = m

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ δ n m ↑z = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i ≫ sndX φ i = 𝟙 (X φ i) ≫ sndX φ i

Tactic:
by simp [mapArrowHom, desc_f' _ _ _ _ hi]

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 : 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 φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (mapArrowHom φ φ'' H (α ≫ β)).f i ≫ sndX φ'' i =
    ((mapArrowHom φ φ' H α).f i ≫ (mapArrowHom φ' φ'' H β).f i) ≫ sndX φ'' i

Tactic:
by simp [mapArrowHom, desc_f' _ _ _ _ hi]

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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ (lift φ α β eq).f p ≫ (↑(fst φ)).v p q hpq = (↑α).v p q hpq

Tactic:
simp [lift]

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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
q : ℤ
hpq : q + 0 = q
⊢ (lift φ α β eq).f q ≫ (snd φ).v q q hpq = β.v q q hpq

Tactic:
simp [lift]

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 : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Quotient r ⥤ D
hΦ : functor r ⋙ Φ = F
⊢ Φ = lift r F H

Tactic:
subst_vars

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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ Φ = lift r (functor r ⋙ Φ) H