mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)

Tactic:
split_ifs with h h'

Goal state after:
case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : b.factorization q ≤ a.factorization q
⊢ Coprime 1 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t

Tactic:
convert! ← zeroLocus_anti_mono_ideal h

Goal state after:
case e'_3
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal s) = closure s

case e'_4
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal t) = closure t
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, {x * y} ⊆ ↑I → {x} ⊆ ↑I ∨ {y} ⊆ ↑I

Tactic:
← Ideal.span_le,

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R}, Ideal.span {x * y} ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ } S

Tactic:
by
      rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm

Tactic:
· simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ g ^ (k % ↑(Nat.find hex)) * g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
rw [← zpow_add, Int.emod_add_mul_ediv, hk]; exact hx

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, x_1 ≤ y → x_1 = x → y = x) ↔ IsMax x

Tactic:
@forall_comm _ (_ = _),

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 : PrimeSpectrum R⦄, x_1 = x → ∀ (a : PrimeSpectrum R), x_1 ≤ a → a = x) ↔ IsMax x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 y : PrimeSpectrum R⦄, y ≤ x_1 → x_1 = x → y = x) ↔ IsMin x

Tactic:
@forall_comm _ (_ = _),

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃x_1 : PrimeSpectrum R⦄, x_1 = x → ∀ a ≤ x_1, a = x) ↔ IsMin x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
this : ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal
⊢ comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p}) ∩ zeroLocus ↑(Ideal.span {X}) = ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem]

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
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ d / (d / m) = m

Tactic:
Nat.div_div_self hm.1 hd0

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ m = m
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ eval₂ (algebraMap R S) r (b.reverse * X ^ (1 + c.natDegree)) = 0

Tactic:
· have : p.natDegree ≤ 1 := by simpa using! natDegree_linear_le (a := r) (b := -1)
    rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow,
      map_X, ← revAt_zero (1 + _), ← reflect_monomial,
      ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc,
      ← add_assoc, reflect_mul _ _ (this.trans (by simp)) le_rfl,
      eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
    simp [← pow_succ']

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.gcd (orderOf g) = 1

Tactic:
have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
hgn : g ∈ Subgroup.zpowers (g ^ n)
⊢ n.gcd (orderOf g) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : 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)
⊢ Nat.Prime (orderOf g)

Tactic:
apply Nat.prime_of_coprime

Goal state after:
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

case h
α : 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)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ Nat.card ↥K' = p ^ m

Tactic:
by rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]

Goal state after:
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
h : (↑P).Normal
Q : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = default

Tactic:
obtain ⟨x, h2⟩ := exists_smul_eq G P default

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
x✝ : G
h1 : x✝ • P = Q
x : G
h2 : x • P = default
⊢ Q = default
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso (s.toFun i.castSucc, s.toFun i.succ) (s.toFun i.castSucc, (snoc s x₂ hsat₂).toFun i.succ.castSucc)

Tactic:
snoc_castSucc

Goal state after:
case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso (s.toFun i.castSucc, s.toFun i.succ) (s.toFun i.castSucc, s.toFun i.succ)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case empty
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
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R ∅) ∧ ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
rcases H with ⟨r, hr1, hrn, _⟩

Goal state after:
case empty
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
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ (a✝ + b✝).coeff i ∈ I ^ i

Tactic:
coeff_add

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ a✝.coeff i + b✝.coeff i ∈ I ^ i
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ (C ((algebraMap R R) r)).coeff i ∈ I ^ i

Tactic:
coeff_C

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ (if i = 0 then (algebraMap R R) r else 0) ∈ I ^ 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
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'
f : M →ₗ[R] M'
p : R[X]
i : ℕ
m : M
⊢ (map R' f) (p • single R i m) = Polynomial.map (algebraMap R R') p • (map R' f) (single R i m)

Tactic:
| single i m =>

Goal state after:
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) (p • single R i m) = Polynomial.eval r p • (eval r) (single R i m)

Tactic:
| single i m =>

Goal state after:
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
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'
f : M →ₗ[R] M'
r : R
i : ℕ
m : M
⊢ (eval ((algebraMap R R') r)) ((map R' f) (single R i m)) = f ((eval r) (single R i m))

Tactic:
| single i m =>

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

Goal state before:
pp: case single
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
i : ℕ
m : S
⊢ (aeval x) (equivPolynomial (single S i m)) = (eval x) ((map R (Algebra.linearMap S R)) (single S i m))

Tactic:
| single i m =>

Goal state after:
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:
| single i m =>

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case 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
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I • I ^ n✝ • F.N j ≤ F.N (n✝ + (j + 1))

Tactic:
← add_assoc

Goal state after:
case 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
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I • I ^ n✝ • F.N j ≤ F.N (n✝ + j + 1)
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 F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N

Tactic:
by rw [add_comm, pow_add, mul_smul, pow_one]

Goal state after:
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ ↥I₁ →ₗ[R] ↥I₂

Tactic:
exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h

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

Goal state before:
pp: 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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x y : ↥I
⊢ (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) (x * y) = 0

Tactic:
by
    simp [toCotangent_eq_zero, ← hIJ, sq, mul_mem_mul]

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

Goal state before:
pp: case refine_2.refine_2
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
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
intro x y

Goal state after:
case refine_2.refine_2
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
D : Derivation R S M
x✝ y✝ : S ⊗[R] S
x₁ x₂ x y : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
Module: Mathlib.RingTheory.Kaehler.Basic

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

Tactic:
intro x y

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: 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
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (mkHomToSingle φ hφ).f j = φ ≫ (singleObjXSelf c j A).inv

Tactic:
dsimp [mkHomToSingle]

Goal state after:
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
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ (singleObjXIsoOfEq c j A j hi).inv else 0) = φ ≫ (singleObjXSelf c j A).inv
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: 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
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (mkHomToSingle φ hφ).f j = φ ≫ (singleObjXSelf c j A).inv

Tactic:
by
  dsimp [mkHomToSingle]
  rw [dif_pos rfl, id_comp]
  rfl

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

Goal state before:
pp: case pos
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
⊢ ((singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k = 0

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:
· subst hi
      simp only [XIsoOfEq_rfl, Iso.refl_inv, comp_id, assoc, hφ k hik, comp_zero]

Goal state after:
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
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 : S ⊗[R] S
hx : x ∈ ideal R S
⊢ (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ (fromIdeal R S) ⟨x, hx✝⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case w
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})
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)

Tactic:
have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]

Goal state after:
case w
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})
this : x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)