mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ (∃ x_1 ∈ {b | b.toIdeal ≤ I}, x_1.toIdeal = x) → IsHomogeneous 𝒜 x ∧ x ≤ I

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Goal state after:
case e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : HomogeneousIdeal 𝒜
hx : x ∈ {b | b.toIdeal ≤ I}
⊢ IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case hf
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (r : R), ((algebraMap R (MvPolynomial ι R)) r).IsHomogeneous 0

Tactic:
exact fun r ↦ MvPolynomial.isHomogeneous_C _ _

Goal state after:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r = finrank K L
⊢ engel K y ≤ engel K x

Tactic:
suffices engel K x = ⊤ by simp_rw [this, le_top]

Goal state after:
case inr.inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r = finrank K L
⊢ engel K x = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x) ↔ l.Disjoint l'

Tactic:
List.Disjoint

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.range =
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker

Tactic:
by
        ext x
        constructor
        · intro hx
          obtain ⟨n, h⟩ := hx
          rw [← h]
          rfl
        · intro hx
          have : ((ofProd c).symm x).1 = 0 := hx
          simp only [LieHom.mem_range, LieHom.coe_mk]
          use ((ofProd c).symm x).2
          nth_rw 2 [← Equiv.apply_symm_apply (ofProd c) x]
          rw [← this]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ p.toList x = [] ↔ x ∉ p.support

Tactic:
simp [toList]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ (p.toList x).length = (p.cycleOf x).support.card

Tactic:
simp [toList]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
h : x ∈ p.support
⊢ (p.toList x)[0] = x

Tactic:
simp [toList]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ (p.toList ((p ^ k) x)).length = ((p.toList x).rotate k).length

pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (p.toList ((p ^ k) x)).length) (h₂ : i < ((p.toList x).rotate k).length),
    (p.toList ((p ^ k) x))[i] = ((p.toList x).rotate k)[i]

Tactic:
· simp only [length_toList, cycleOf_self_apply_pow, length_rotate]

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (p.toList ((p ^ k) x)).length) (h₂ : i < ((p.toList x).rotate k).length),
    (p.toList ((p ^ k) x))[i] = ((p.toList x).rotate k)[i]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ [].formPerm = 1

Tactic:
formPerm_nil

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ 1 = 1
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
x y : loopAlgebra R A L
⊢ { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (x + y)) (-a))) v, map_add' := ⋯,
      map_smul' := ⋯ } =
    { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v, map_add' := ⋯,
        map_smul' := ⋯ } +
      { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) y) (-a))) v, map_add' := ⋯,
        map_smul' := ⋯ }

Tactic:
by ext; simp [sum_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ C n i j ≤ 0

Tactic:
by
  simp only [C, Matrix.of_apply]; split_ifs <;> omega

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: 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)
⊢ Prime ↑(d ⟨p, ⋯⟩)

Tactic:
rw [← irreducible_iff_prime]
  refine (Associates.isAtom_iff <|
    ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨?_, fun b hb => ?_⟩
  · rw [Ne, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one,
      coe_factor_orderIso_map_eq_one_iff _ d]
    rintro rfl
    exact (prime_of_normalized_factor 1 hp).not_isUnit isUnit_one
  · have : b ≤ n := le_trans (le_of_lt hb) (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop
    obtain ⟨x, hx⟩ := d.surjective ⟨b, this⟩
    rw [← Subtype.coe_mk (p := (· ≤ n)) b this, ← hx] at hb
    let : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
    let : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
    suffices x = ⊥ by
      rw [this, OrderIso.map_bot d] at hx
      refine (Subtype.mk_eq_bot_iff ?_ _).mp hx.symm
      simp
    obtain ⟨a, ha⟩ := x
    rw [Subtype.mk_eq_bot_iff]
    · 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)
    simp

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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 : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y

Tactic:
rintro ⟨y', rfl⟩

Goal state after:
case mpr
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' : R
⊢ ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y' • (algebraMap R P) x
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ p ^ min 0 (Multiset.count p P) = ⊤

Tactic:
zero_min,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ p ^ 0 = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q ↦ span {q}) (factors p), Prime q
⊢ normalizedFactors (Multiset.map (fun x ↦ span {x}) (factors p)).prod = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
normalizedFactors_prod_of_prime this

Goal state after:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q ↦ span {q}) (factors p), Prime q
⊢ Multiset.map (fun q ↦ span {q}) (factors p) = Multiset.map (fun q ↦ span {q}) (factors p)
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ IsNoetherian K (V ⧸ u.eqLocus v)

Tactic:
rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
b : ↥S
hb : ∀ i ∈ Finset.univ, IsInteger f (↑b • g i)
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi : i ∈ {I | I ∈ normalizedFactors (span {r})}
⊢ ∃ a, (fun d ↦ ⟨span {↑d}, ⋯⟩) a = ⟨i, hi⟩

Tactic:
have : i.IsPrime := isPrime_of_prime (prime_of_normalized_factor i hi)

Goal state after:
case refine_2.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi : i ∈ {I | I ∈ normalizedFactors (span {r})}
this : i.IsPrime
⊢ ∃ a, (fun d ↦ ⟨span {↑d}, ⋯⟩) a = ⟨i, hi⟩
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Tactic:
obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
x : ↑{d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) x = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})
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 : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
h_minus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
h_neg_zero : ⁅x_χ, m_neg⁆ = 0
h_chi_coroot_zero : χ (coroot α) = 0
h_lie_eq_smul : ⁅↑y, x_χ⁆ = χ y • x_χ
⊢ ?m.1538 ∈ ?m.1533 ∙ ?m.1539

Tactic:
by
        rw [← coe_corootSpace_eq_span_singleton α, LieSubmodule.mem_toSubmodule]
        exact hy

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

Goal state before:
pp: case single.e_a.add
R : Type u
inst✝ : CommRing R
σ : Type u_1
b p✝ q✝ : MvPolynomial σ R
a✝¹ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) p✝) =
    (D R (MvPolynomial σ R)) p✝
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) q✝) =
    (D R (MvPolynomial σ R)) q✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) (p✝ + q✝)) =
    (D R (MvPolynomial σ R)) (p✝ + q✝)

pp: case single.e_a.mul_X
R : Type u
inst✝ : CommRing R
σ : Type u_1
b p✝ : MvPolynomial σ R
n✝ : σ
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) p✝) =
    (D R (MvPolynomial σ R)) p✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) (p✝ * MvPolynomial.X n✝)) =
    (D R (MvPolynomial σ R)) (p✝ * MvPolynomial.X n✝)

Tactic:
· simp only [map_add, *]

Goal state after:
case single.e_a.mul_X
R : Type u
inst✝ : CommRing R
σ : Type u_1
b p✝ : MvPolynomial σ R
n✝ : σ
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) p✝) =
    (D R (MvPolynomial σ R)) p✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) (p✝ * MvPolynomial.X n✝)) =
    (D R (MvPolynomial σ R)) (p✝ * MvPolynomial.X n✝)
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (D R R[X]) ((aeval X) P) = derivative ((aeval X) P) • (D R R[X]) X

Tactic:
(D R R[X]).map_aeval,

Goal state after:
R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (aeval X) (derivative P) • (D R R[X]) X = derivative ((aeval X) P) • (D R R[X]) X
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: 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'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
| ((algebraMap P'.Ring S') (f.toRingHom r) • of (P'.ker.toCotangent ⟨f.toAlgHom ↑x, ⋯⟩)).val

Tactic:
algebraMap_smul,

Goal state after:
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'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
| (f.toRingHom r • of (P'.ker.toCotangent ⟨f.toAlgHom ↑x, ⋯⟩)).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
inst✝¹ : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst✝ : Finite α
⊢ P.ker.FG

Tactic:
rw [Generators.ker_eq_ker_aeval_val]

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst✝ : Finite α
⊢ (RingHom.ker (aeval P.val)).FG
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Generators R S ι
r : R
inst✝ : IsLocalization.Away r S
s : S
⊢ s * (algebraMap R S) r ^ (IsLocalization.Away.sec r s).2 *
      IsLocalization.mk' S 1 ⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2 =
    s

Tactic:
rw [← IsLocalization.mk'_pow, one_pow, ← IsLocalization.mk'_one (M := Submonoid.powers r) S r]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Generators R S ι
r : R
inst✝ : IsLocalization.Away r S
s : S
⊢ s * IsLocalization.mk' S r 1 ^ (IsLocalization.Away.sec r s).2 *
      IsLocalization.mk' S 1 (⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2) =
    s
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Function.Surjective ⇑φ

Tactic:
rw [← LinearMap.range_eq_top] at h₁ ⊢

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ φ.range = ⊤
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
a : MvPolynomial ι T
ha : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
b : MvPolynomial ι T
hb : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) b = y
⊢ ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x + y

Tactic:
use (a + b)

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
a : MvPolynomial ι T
ha : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
b : MvPolynomial ι T
hb : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) b = y
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (a + b) = x + y
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
| (Ideal.Quotient.mkₐ R I) (s x)

Tactic:
aeval_unique (Ideal.Quotient.mkₐ _ I)

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
| (aeval (⇑(Ideal.Quotient.mkₐ R I) ∘ X)) (s x)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
⊢ algebraMap (ofAlgHom f h).toExtension.Ring S = f.toRingHom

Tactic:
exact MvPolynomial.ringHom_ext (by simp) (by simp [ofAlgHom])

Goal state after: