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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
⊢ (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)

Tactic:
by
  obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁; rw [heq₁]; clear heq₁
  obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂; rw [heq₂]; clear heq₂
  exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q

Tactic:
cases Q

Goal state after:
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p ↥toSubgroup✝¹
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : Nat.card α ≠ 1
⊢ Nat.Prime (Nat.card α)

Tactic:
rw [← orderOf_eq_card_of_forall_mem_zpowers hg] at hα ⊢

Goal state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
⊢ Nat.Prime (orderOf g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑n = ((zmultiplesHom G) g).ker

Tactic:
by
    rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]

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)⁻¹ * (↑n * g) ∈ normalizer ↑(map N.subtype ↑P) ⊔ N

Tactic:
sup_comm

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 : n • MulAut.conjNormal g • P = P
⊢ (↑n)⁻¹ * (↑n * g) ∈ N ⊔ normalizer ↑(map N.subtype ↑P)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ Nat.card ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d

Tactic:
MonoidHom.map_zpowers,

Goal state after:
G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ Nat.card ↥(Subgroup.zpowers ((powMonoidHom d) g)) = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ x ^ 0 = ↑⟨y, ⋯⟩

Tactic:
rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ ⟨y, ⋯⟩ ∈ H.subgroupOf (normalizer ↑H)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y

Tactic:
sup_comm

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (y ⊔ x)
hyz : IsMaximal y (y ⊔ x)
⊢ IsMaximal (y ⊓ x) y
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
M✝ : Type u_4
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
m : Submodule R M✝
N : Type u_5
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type u_7
inst✝³ : Finite ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R ((i : ι) → M i)

Tactic:
by
  classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single _ _ ·))
    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : (eraseLast s).last = x
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

pp: case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
· use s.eraseLast
      simp [← hetx, hn, Equivalent.refl]

Goal state after:
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ LinearMap.range f = Ideal.span {f 1}

Tactic:
LinearMap.range_eq_map,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Submodule.map f ⊤ = Ideal.span {f 1}
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0

Tactic:
· rw [contra, torsionOf_zero] at h
    exact bot_ne_top.symm h

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)

Tactic:
simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : ∃ y_1 ∈ I, y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s

Tactic:
rcases hy with ⟨c, hci, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ((s • m).coeff.sum fun i m ↦ r ^ i • m) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m

Tactic:
refine (Finsupp.sum_smul_index' ?_).trans ?_
    · exact fun i => smul_zero _
    · simp_rw [RingHom.id_apply, Finsupp.smul_sum]
      congr
      ext i c
      rw [smul_comm]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
⊢ (l.sum fun a₁ b ↦ (b • ↑a₁).coeff (n + 1)) ∈ I • F.N n

Tactic:
apply Submodule.sum_mem _ _

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
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
⊢ ∀ c ∈ l.support, (fun a₁ b ↦ (b • ↑a₁).coeff (n + 1)) c (l c) ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
rcases Submodule.mem_sup.mp hx with ⟨y, hy, z, hz, hyz⟩

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
⊢ j✝ = j'✝

Tactic:
obtain ⟨k', w₁', w₂'⟩ := w'

Goal state after:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
k' : ι
w₁' : c₁.Rel i✝ k'
w₂' : c₂.Rel k' j'✝
⊢ j✝ = j'✝
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
⊢ i✝ = i'✝

Tactic:
obtain ⟨k', w₁', w₂'⟩ := w'

Goal state after:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
k' : ι
w₁' : c₁.Rel i'✝ k'
w₂' : c₂.Rel k' j✝
⊢ i✝ = i'✝
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' φ') β
⊢ α = β

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

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

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : ¬i = j
⊢ 0 ≫ K.d i k = 0

Tactic:
apply (isZero_single_obj_X c j A i hi).eq_of_src

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
⊢ m = { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ }

Tactic:
by
    ext i
    apply (hs i).uniq ((eval C c i).mapCone t)
    intro j
    dsimp
    simp only [← comp_f, hm]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ j + i = k

Tactic:
add_comm j i,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ i + j = k
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
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (F ⋙ shiftFunctor D m₃).map ((add hF s i m₁ m₂).hom.app X) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))

Tactic:
rw [Functor.comp_map, map_add_hom_app,
          Functor.map_comp, Functor.map_comp, Iso.inv_hom_id_app_assoc,
          ← Functor.map_comp_assoc _ ((i (m₁ + m₂)).inv.app X), Iso.inv_hom_id_app,
          Functor.map_id, Category.id_comp, reassoc_of% h,
          dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃)]

Goal state after:
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
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (eqToHom ⋯ ≫ (i (m₁ + (m₂ + m₃))).hom.app X ≫ eqToHom ⋯) ≫
      (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
        (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
          (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))
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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
a b : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Finsupp.smul_single_one _ (1 * _ : S)

Goal state after:
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
a b : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
hk : k ≫ K.d i j = 0
⊢ K.liftCycles k j hj hk ≫ K.iCycles i = k

Tactic:
dsimp [liftCycles, iCycles]

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
hk : k ≫ K.d i j = 0
⊢ (K.sc i).liftCycles k ⋯ ≫ (K.sc i).iCycles = k
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_cases h : c.Rel i i'

Goal state after:
case pos
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
h : c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

case neg
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
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0
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
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
⊢ (map R S A B).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.restrictScalars A (kerTotal S B)))

Tactic:
← Submodule.map_comap_eq_of_surjective (linearCombination_surjective R A) (LinearMap.ker _)

Goal state after:
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
⊢ Submodule.map (linearCombination A ⇑(D R A)) (Submodule.comap (linearCombination A ⇑(D R A)) (map R S A B).ker) =
    Submodule.map (linearCombination A ⇑(D R A))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.restrictScalars A (kerTotal S B)))
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inl ≫ (K.biprodXIso L i).inv = biprod.inl.f i

Tactic:
simp [biprodXIso]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr ≫ (K.biprodXIso L i).inv = biprod.inr.f i

Tactic:
simp [biprodXIso]

Goal state after: