mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
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
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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
β_lin : ↥H →ₗ[K] K
hβ_in_q : β_lin ∈ q
hβ_ne_zero : β_lin ≠ 0
h_trivial : ¬genWeightSpace L ⇑β_lin = ⊥
β : Weight K (↥H) L := { toFun := ⇑β_lin, genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
⊢ genWeightSpace L ⇑β_lin ≤ I

Tactic:
refine le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)

Goal state after:
case neg
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
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
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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
β_lin : ↥H →ₗ[K] K
hβ_in_q : β_lin ∈ q
hβ_ne_zero : β_lin ≠ 0
h_trivial : ¬genWeightSpace L ⇑β_lin = ⊥
β : Weight K (↥H) L := { toFun := ⇑β_lin, genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
⊢ genWeightSpace L ⇑β_lin ≤ sl2SubmoduleOfRoot ⋯
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J * J ≤ I

Tactic:
simp [FractionalIdeal.mul_le, mem_div_iff_of_ne_zero hJ]

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
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
h : Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank R ↥M + Module.rank R ↥N
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)

Tactic:
IsLattice.rank' K M,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
h : Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank R ↥N
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
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_eq : S.root i = -S.root j
⊢ Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0

Tactic:
by rw [← hi, ← hj, h_eq, neg_add_cancel]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
k : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : Module k M
inst✝² : Module k N
f : M →ₗ[k] N
inst✝¹ : FiniteDimensional k M
inst✝ : FiniteDimensional k N
⊢ f.index = ↑(finrank k M) - ↑(finrank k N)

Tactic:
rw [index_eq_finrank_sub]
  have h₁ := f.range.finrank_quotient_add_finrank
  have h₂ := f.quotKerEquivRange.finrank_eq
  have h₃ := f.ker.finrank_quotient_add_finrank
  lia

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
k : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : Module k M
inst✝² : Module k N
f : M →ₗ[k] N
inst✝¹ : FiniteDimensional k M
inst✝ : FiniteDimensional k N
⊢ f.index = ↑(finrank k M) - ↑(finrank k N)

Tactic:
by
  -- `0 → f.ker → M → N → f.coker → 0`
  rw [index_eq_finrank_sub]
  have h₁ := f.range.finrank_quotient_add_finrank
  have h₂ := f.quotKerEquivRange.finrank_eq
  have h₃ := f.ker.finrank_quotient_add_finrank
  lia

Goal state after:
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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → ↥s →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
this : ⇑(linearCombination R Subtype.val) '' σ '' ↑t = ↑t
⊢ (Submodule.comap (linearCombination R Subtype.val)
      (Submodule.map (linearCombination R Subtype.val) (Submodule.span R (σ '' ↑t)))).FG

Tactic:
Submodule.comap_map_eq,

Goal state after:
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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → ↥s →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
this : ⇑(linearCombination R Subtype.val) '' σ '' ↑t = ↑t
⊢ (Submodule.span R (σ '' ↑t) ⊔ (linearCombination R Subtype.val).ker).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ a = x ^ (n + 1) * q'

Tactic:
rw [hq, hq']

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ x ^ n * (x * q') = x ^ (n + 1) * q'
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:
rw [← coe_corootSpace_eq_span_singleton α, LieSubmodule.mem_toSubmodule]
        exact hy

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

Goal state before:
pp: case pos.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
⊢ torsionOf R M y = R ∙ p ^ (pOrder hM y - k) * p ^ k

Tactic:
convert! Ideal.torsionOf_eq_span_pow_pOrder hp hM y

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
⊢ p ^ (pOrder hM y - k) * p ^ k = p ^ pOrder hM y
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
cases q

Goal state after:
case mul_X.inl
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

case mul_X.inr
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1}
⊢ (auxInv S r) ((auxHom S r) x) = x

Tactic:
simpa using congrFun (congrArg DFunLike.coe <| auxInv_auxHom S r) x

Goal state after:
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}))
⊢ (Generators.localizationAway S r).ker = Ideal.span {C r * X () - 1}

Tactic:
rw [Generators.ker_eq_ker_aeval_val, this, ← RingHom.ker_coe_toRingHom, AlgHom.comp_toRingHom,
    ← RingHom.comap_ker]

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}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker ↑↑(mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}
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
⊢ (algebraMap R S) (IsLocalization.Away.sec r s).1 * IsLocalization.Away.invSelf r ^ (IsLocalization.Away.sec r s).2 = s

Tactic:
simp only [← IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf]

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 * (algebraMap R S) r ^ (IsLocalization.Away.sec r s).2 *
      IsLocalization.mk' S 1 ⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2 =
    s
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
m₁ m₂ : M
⊢ s.var m₁ + s.var m₂ = s.var (m₁ + m₂)

Tactic:
← sub_eq_zero

Goal state after:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
m₁ m₂ : M
⊢ s.var m₁ + s.var m₂ - s.var (m₁ + m₂) = 0
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
a : A
m : M
⊢ (RingHom.id A) a • s.var m = s.var (a • m)

Tactic:
← sub_eq_zero

Goal state after:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
a : A
m : M
⊢ (RingHom.id A) a • s.var m - s.var (a • m) = 0
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ ∀ (a : presB.G) (b : A) (f : presB.G →₀ A),
    a ∉ f.support →
      b ≠ 0 →
        Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r (presB.π (Finsupp.single a b + f)) ∈
            Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
intro g

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
g : presB.G
⊢ ∀ (b : A) (f : presB.G →₀ A),
    g ∉ f.support →
      b ≠ 0 →
        Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r (presB.π (Finsupp.single g b + f)) ∈
            Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
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 : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).toExtension.Ring S)

Tactic:
dsimp; ext; simp

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) → Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
rintro H x hx' f rfl

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
⊢ f ∈ ↑x.asIdeal
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
⊢ Ideal.map (algebraMap R Rₚ) I ≤ IsLocalRing.maximalIdeal Rₚ

Tactic:
← Localization.AtPrime.map_eq_maximalIdeal

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
⊢ Ideal.map (algebraMap R Rₚ) I ≤ Ideal.map (algebraMap R (Localization.AtPrime p.asIdeal)) p.asIdeal
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
⊢ ∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG

Tactic:
intro g

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ ∑ k, (-1) ^ ↑k • (f (v k)) (k.removeNth v) =
    (-1) ^ ↑i • (f (v i)) (i.removeNth v) + (-1) ^ ↑j • (f (v j)) (j.removeNth v)

Tactic:
refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
k : Fin (n + 1)
x✝ : k ≠ i ∧ k ≠ j
hki : k ≠ i
hkj : k ≠ j
⊢ (-1) ^ ↑k • (f (v k)) (k.removeNth v) = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
⊢ ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑a)) = 1

Tactic:
simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
⊢ (Matrix.of fun i j ↦ (f (a j)) (x (a i))).det = 1