mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : ¬g = 1
⊢ orderOf g ∣ p

Tactic:
rw [h g hg]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G

Tactic:
exact order_dvd_exponent g

Goal state after:
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
⊢ 0 < #{a | orderOf a = Nat.card α}

Tactic:
rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
⊢ 0 < Fintype.card α
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
hmem : g ^ ngn ∈ f.ker
⊢ IsOfFinOrder g

Tactic:
lift g ^ ngn to N using hN.symm ▸ hmem with gn h

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
⊢ IsOfFinOrder g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
x y : Multiplicative ℤ
hxy : x < y
⊢ g ^ Multiplicative.toAdd y < g ^ Multiplicative.toAdd x

Tactic:
exact zpow_right_strictAnti hg1 hxy

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
⊢ j ≠ i → ↑(μ i) ∈ I j

Tactic:
ij

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ ↑(μ i) ∈ I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ (Exists.choose h)) + ↑⟨↑(μ (Exists.choose h)), ⋯⟩ =
    Pi.single (Exists.choose h) (↑(μ a)) (Exists.choose h) + ↑(μ (Exists.choose h))

Tactic:
Pi.single_eq_same,

Goal state after:
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑⟨↑(μ a), ⋯⟩ + ↑⟨↑(μ (Exists.choose h)), ⋯⟩ =
    Pi.single (Exists.choose h) (↑(μ a)) (Exists.choose h) + ↑(μ (Exists.choose h))
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑⟨↑(μ a), ⋯⟩ + ↑⟨↑(μ (Exists.choose h)), ⋯⟩ =
    Pi.single (Exists.choose h) (↑(μ a)) (Exists.choose h) + ↑(μ (Exists.choose h))

Tactic:
Pi.single_eq_same,

Goal state after:
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑⟨↑(μ a), ⋯⟩ + ↑⟨↑(μ (Exists.choose h)), ⋯⟩ = ↑(μ a) + ↑(μ (Exists.choose h))
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

Tactic:
rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ eraseLast s ↔ x ≠ last s ∧ x ∈ s

Tactic:
simp only [RelSeries.mem_def, eraseLast]
  constructor
  · rintro ⟨i, rfl⟩
    have hi : (i : ℕ) < s.length := by lia
    simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
  · intro h
    exact mem_eraseLast_of_ne_of_mem h.1 h.2

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
i : Fin s₂.length
⊢ Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ)
    (s₂.toFun i.castSucc, s₂.toFun i.succ)

Tactic:
by simpa using h.choose_spec (h.choose.symm i)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
⊢ j ≠ i → v ∈ I j

Tactic:
ij

Goal state after:
case refine_2.mpr.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ v ∈ I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
⊢ j ≠ i → u * ↑(μ i) ∈ I j

Tactic:
ij

Goal state after:
case refine_2.mpr.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ u * ↑(μ i) ∈ I j
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case pos
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 : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j

Tactic:
ij

Goal state after:
case pos
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 : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r ∘ₗ comp p) (single R i m) = (eval (Polynomial.eval r p)) (single R i m)

Tactic:
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    module

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.succ
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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ I • F.N (n₀ + n✝) = I ^ (n✝ + 1) • F.N n₀

pp: case h.succ.a
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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ n₀ + n✝ ≥ n₀

Tactic:
ih,

Goal state after:
case h.succ
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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ I • I ^ n✝ • F.N n₀ = I ^ (n✝ + 1) • F.N n₀

case h.succ.a
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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ n₀ + n✝ ≥ n₀
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
⊢ Submodule.span ↥(reesAlgebra I) ↑F.submodule.toAddSubmonoid = F.submodule

Tactic:
Submodule.coe_toAddSubmonoid

Goal state after:
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
⊢ Submodule.span ↥(reesAlgebra I) ↑F.submodule = F.submodule
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Function.Injective fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩

Tactic:
rintro x y e

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : I.Cotangent
e : (fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) x = (fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) y
⊢ x = y
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)
α β : relativeDifferentials' φ' ⟶ M
h : Derivation.postcomp (derivation' φ') α = Derivation.postcomp (derivation' φ') β
X : Dᵒᵖ
⊢ α.app X = β.app X

Tactic:
exact CommRingCat.KaehlerDifferential.ext (Derivation.congr_d h)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ▷ n)).app X

Tactic:
← tensorHom_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ⊗ₘ 𝟙 n)).app X
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst

Tactic:
dsimp [mkHom, mkHomAux]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst

Tactic:
dsimp [mkHom, mkHomAux]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ Submodule.Quotient.mk (single x z + single y z - single (x + y) z) = 0

Tactic:
Submodule.Quotient.mk_eq_zero

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ Submodule.Quotient.mk (single y (z * x) + single x (z * y) - single (x * y) z) = 0

Tactic:
Submodule.Quotient.mk_eq_zero

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map ((add hF s i n 0).hom.app X) = F.map (eqToHom ⋯ ≫ (zero hF s i).inv.app ((s n).obj X))

Tactic:
by
        have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n)
        simp [this, ← NatTrans.naturality_assoc, eqToHom_map,
          shiftFunctorAdd_add_zero_hom_app]

Goal state after:
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 L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ (α ≫ k) ≫ K.d i j = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ α ≫ k ≫ K.d i j = 0
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 L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ (x ≫ K.d i' i) ≫ K.d i j = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ x ≫ K.d i' i ≫ K.d i j = 0
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
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ (x ≫ K.d i' i) ≫ K.d i j = 0

Tactic:
assoc,

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
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ x ≫ K.d i' i ≫ K.d i j = 0
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
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
by
  by_cases h : c.Rel i i'
  · obtain rfl := c.next_eq' h
    exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx
  · have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
      rw [K.shape _ _ h, zero_comp] at hx
      rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
    rw [this, comp_zero]

Goal state after:
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 L M : HomologicalComplex C c
φ✝ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ (k ≫ φ.f i) ≫ L.d i j = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ✝ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ k ≫ φ.f i ≫ L.d i j = 0
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 L M : HomologicalComplex C c
φ✝ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ (k ≫ φ.f i) ≫ L.d i j = 0

Tactic:
by rw [assoc, φ.comm, reassoc_of% hk, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ (desc φ α hα).f j = hα.hom (c.next j) j

Tactic:
dsimp [desc]

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 ≫
      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
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
i : ι
⊢ inrX φ i ≫ (desc φ α hα).f i = α.f i

Tactic:
dsimp [desc]

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
i : ι
⊢ (inrX φ i ≫
      if hj : c.Rel i (c.next i) then fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i
      else sndX φ i ≫ α.f i) =
    α.f i
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 K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ ι₁ K ≫ desc φ₀ φ₁ h = φ₁

Tactic:
simp [ι₁, desc]

Goal state after: