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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ a = ⊥

pp: case refine_2.hbot
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⊥ ∈ Set.Iic m

Tactic:
· exact
        ((Associates.isAtom_iff <| Prime.ne_zero <| prime_of_normalized_factor p hp).mpr <|
              irreducible_of_normalized_factor p hp).right
          a (Subtype.mk_lt_mk.mp <| d.lt_iff_lt.mp hb)

Goal state after:
case refine_2.hbot
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⊥ ∈ Set.Iic m
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ Aᵀ.IsSimplyLaced ↔ A.IsSimplyLaced

Tactic:
IsSimplyLaced,

Goal state after:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (Pairwise fun i j ↦ Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ A.IsSimplyLaced
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ (Pairwise fun i j ↦ Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ A.IsSimplyLaced

Tactic:
IsSimplyLaced,

Goal state after:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (Pairwise fun i j ↦ Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ Pairwise fun i j ↦ A i j = 0 ∨ A i j = -1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ I / 1 = I

Tactic:
div_of_ne_zero (one_ne_zero' (FractionalIdeal R₁⁰ K))

Goal state after:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ ⟨↑I / ↑1, ⋯⟩ = I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsNoetherianRing A

Tactic:
by
  let := h.commGroupWithZero (FractionRing A)
  refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩
  by_cases hI : I = ⊥
  · rw [hI]; apply Submodule.fg_bot
  have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
  exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ y, (algebraMap A (FractionRing A)) y = x

Tactic:
rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)

Tactic:
apply coeToSubmodule_injective
  simp only [coe_mul, coe_spanSingleton, span_mul_span, singleton_mul_singleton]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ I * J ≤ P → I ≤ P ∨ J ≤ P

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → I ≤ P ∨ J ≤ P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → I ≤ P ∨ J ≤ P

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ J ≤ P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I ^ e < I

Tactic:
convert! I.pow_right_strictAnti hI0 hI1 he
  dsimp only
  rw [pow_one]

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom ((∑ i ∈ DFinsupp.support ((decompose 𝓐) x), ↑(((decompose 𝓐) x) i)) • y) =
    (∑ x_1 ∈ DFinsupp.support ((decompose 𝓐) x), (RingHom.id A) ↑(((decompose 𝓐) x) x_1)) •
      (decomposeAddEquiv 𝓜).toAddHom y

Tactic:
Finset.sum_smul,

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom (∑ i ∈ DFinsupp.support ((decompose 𝓐) x), ↑(((decompose 𝓐) x) i) • y) =
    (∑ x_1 ∈ DFinsupp.support ((decompose 𝓐) x), (RingHom.id A) ↑(((decompose 𝓐) x) x_1)) •
      (decomposeAddEquiv 𝓜).toAddHom y
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
⊢ (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • y) = ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) y

Tactic:
← DirectSum.sum_support_decompose 𝓜 y,

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
⊢ (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ∑ i ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓜) y) i)) =
    ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) (∑ i ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓜) y) i))
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom.toFun (x • y) = (RingHom.id A) x • (decomposeAddEquiv 𝓜).toAddHom.toFun y

Tactic:
classical
  rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
  refine Finset.sum_congr rfl (fun i _hi => ?_)
  rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]
  refine Finset.sum_congr rfl (fun j _hj => ?_)
  rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
  simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
  convert! DirectSum.decompose_coe 𝓜 _
  rfl

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := ↑s) K (⇑f ∘ Subtype.val)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
hsubset : (Set.range fun x ↦ f ↑x) ⊆ ↑f.range
⊢ ⊤ ≤ span K ↑f.range

Tactic:
← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := ↑s) K (⇑f ∘ Subtype.val)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
hsubset : (Set.range fun x ↦ f ↑x) ⊆ ↑f.range
⊢ span K (Set.range (⇑f ∘ Subtype.val)) ≤ span K ↑f.range
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
x✝ : ↥⋯.toFinset
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, π a = ⟨x, hx⟩

Tactic:
obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
    exact ⟨y, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case hs1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : (↥s →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ (Submodule.map f.range.mkQ l.ker).FG

Tactic:
rw [this]
    exact Module.Finite.fg_top

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p q : MvPolynomial σ R
i : σ
hq : D (p * q) = p • D q + q • D p
⊢ D (p * (q * X i)) = p • D (q * X i) + (q * X i) • D p

Tactic:
| mul_X q i hq =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
⊢ Function.RightInverse
    (⇑(Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x)))
    (MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun

Tactic:
by
    intro x
    induction x using Finsupp.induction_linear with
    | zero => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero]
    | add => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *; simp only [*]
    | single a b => simp [-map_smul]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
rw [← this]

Goal state after:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i =
    ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) x
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
i : σ
⊢ (aeval P.val) (P.relation i) = 0

Tactic:
← RingHom.mem_ker,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
i : σ
⊢ P.relation i ∈ RingHom.ker (aeval P.val)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker ↑((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) =
    Ideal.span {C r * X () - 1}

Tactic:
AlgHom.comp_toRingHom,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker ((↑↑(mvPolynomialQuotientEquiv S r)).comp ↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) =
    Ideal.span {C r * X () - 1}
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
| ↑q

Tactic:
RootPairing.invtRootSubmodule.eq_span_root q

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
| Submodule.span K (⇑(rootSystem H).root '' {i | (rootSystem H).root i ∈ ↑q})
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
t : (i : ι) → (relations i).Solution N
x✝ : (directSum relations).R
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun x ↦
        match x with
        | ⟨i, g⟩ => (t i).var g)
      ((directSum relations).relation ⟨i, r⟩) =
    0

Tactic:
rw [← (t i).linearCombination_var_relation r]

Goal state after:
A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
t : (i : ι) → (relations i).Solution N
x✝ : (directSum relations).R
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun x ↦
        match x with
        | ⟨i, g⟩ => (t i).var g)
      ((directSum relations).relation ⟨i, r⟩) =
    (Finsupp.linearCombination A (t i).var) ((relations i).relation r)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case e'_2
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' : 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0
hb' : 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0
⊢ 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ + 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩

Tactic:
rw [← tmul_add]

Goal state after:
case e'_2
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' : 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0
hb' : 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0
⊢ 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 1 ⊗ₜ[P.Ring] (⟨a, ⋯⟩ + ⟨b, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
x : ↥G.ker × N
a✝ : x ∈ ma
h'x : ↑x.1 i = 0
⊢ ↑x.1 i • x.2 = 0

Tactic:
h'x,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
x : ↥G.ker × N
a✝ : x ∈ ma
h'x : ↑x.1 i = 0
⊢ 0 • x.2 = 0