mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
h₄ : Exact ⇑f₃ ⇑f₄
h₅ : Surjective ⇑f₄
⊢ FiniteDimensional k ↥(g ∘ₗ f).ker

Tactic:
ker_comp

Goal state after:
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
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
h₄ : Exact ⇑f₃ ⇑f₄
h₅ : Surjective ⇑f₄
⊢ FiniteDimensional k ↥(comap f g.ker)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ Irreducible (span {x})

pp: case hnorm
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ normalize (span {x}) = span {x}

pp: case hle
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ^ n ∣ span {a₀}

pp: case hlt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬span {x} ^ (n + 1) ∣ span {a₀}

pp: case hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {a₀} ≠ 0

pp: case hJ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ (span {x}).IsPrime

pp: case hJ₀
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ≠ ⊥

Tactic:
· exact (prime_span_singleton_iff.mpr hx).irreducible

Goal state after:
case hnorm
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ normalize (span {x}) = span {x}

case hle
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ^ n ∣ span {a₀}

case hlt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬span {x} ^ (n + 1) ∣ span {a₀}

case hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {a₀} ≠ 0

case hJ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ (span {x}).IsPrime

case hJ₀
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ≠ ⊥
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: case inr
A : Type u
inst✝⁶ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module A M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module A M₂
inst✝¹ : AddCommGroup M₃
inst✝ : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
i : ι
⊢ f.range.mkQ ((Finsupp.linearCombination A pres₂.var) ((pres₂.cokernelRelations data).relation (Sum.inr i))) = 0

Tactic:
erw [data.π_lift]

Goal state after:
case inr
A : Type u
inst✝⁶ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module A M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module A M₂
inst✝¹ : AddCommGroup M₃
inst✝ : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
i : ι
⊢ f.range.mkQ (f (g₁ i)) = 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : FinitePresentation R M
S : Submonoid R
Mₚ : Type u_1
inst✝⁵ : AddCommGroup Mₚ
inst✝⁴ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝³ : IsLocalizedModule S f
Nₚ : Type u_2
inst✝² : AddCommGroup Nₚ
inst✝¹ : Module R Nₚ
g : N →ₗ[R] Nₚ
inst✝ : IsLocalizedModule S g
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
φ : M →ₗ[R] N
s : ↥S
hφ : g ∘ₗ φ = s • ϕ ∘ₗ f
hmap : (IsLocalizedModule.map S f g) φ = s • ϕ
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)

Tactic:
refine ⟨φ, s, hmap, ?_⟩

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : FinitePresentation R M
S : Submonoid R
Mₚ : Type u_1
inst✝⁵ : AddCommGroup Mₚ
inst✝⁴ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝³ : IsLocalizedModule S f
Nₚ : Type u_2
inst✝² : AddCommGroup Nₚ
inst✝¹ : Module R Nₚ
g : N →ₗ[R] Nₚ
inst✝ : IsLocalizedModule S g
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
φ : M →ₗ[R] N
s : ↥S
hφ : g ∘ₗ φ = s • ϕ ∘ₗ f
hmap : (IsLocalizedModule.map S f g) φ = s • ϕ
⊢ Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)
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
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
⊢ m_α = m_pos + m_neg + m_h

Tactic:
← hm_eq,

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 : 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
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
⊢ m_αneg + m_h = m_pos + m_neg + m_h
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • f 1 = 0

Tactic:
← f.map_smul

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ f (p ^ k • 1) = 0
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: 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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • Submodule.Quotient.mk 1 = 0

Tactic:
rw [← mk_smul, Quotient.mk_eq_zero, smul_eq_mul, mul_one]

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)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k ∈ R ∙ p ^ k
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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ ∃ b, (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * b = 1

Tactic:
use (Ideal.Quotient.mk _ <| X ())

Goal state after:
case h
σ : 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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := ⋯
⊢ (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (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 : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
⊢ ∀ {x m : L}, m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier → ⁅x, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
intro x m hm
    have hx : x ∈ ⨆ χ : Weight K H L, genWeightSpace L χ := by
      simp [LieModule.iSup_genWeightSpace_eq_top']
    induction hx using LieSubmodule.iSup_induction' with
    | mem χ x_χ hx_χ =>
      induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂
    | zero =>
      simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]
    | add x₁ x₂ _ _ ih₁ ih₂ =>
      simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
      exact add_mem ih₁ ih₂

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case hf
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
⊢ Function.Bijective ⇑↑(sumAlgEquiv R ι' ι)

Tactic:
simpa using AlgEquiv.bijective (sumAlgEquiv R ι' ι)

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
pres : Presentation A M
inst✝¹ : Finite pres.G
inst✝ : Finite pres.R
⊢ pres.π.ker.FG

Tactic:
rw [pres.ker_π]
    exact Submodule.fg_span (Set.finite_range _)

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
relations : Relations A
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module A M
inst✝² : IsEmpty relations.R
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (relations.G →₀ A) →ₗ[A] N✝
h : relations.solutionFinsupp.postcomp f✝ = relations.solutionFinsupp.postcomp f'✝
a✝ : relations.G
⊢ (f✝ ∘ₗ Finsupp.lsingle a✝) 1 = (f'✝ ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
apply Solution.congr_var h

Goal state after:
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
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
p q : MvPolynomial ι' S
hp : ∃ a, (Q.ofComp P).toAlgHom a = p
hq : ∃ a, (Q.ofComp P).toAlgHom a = q
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p + q

Tactic:
obtain ⟨p, rfl⟩ := hp

Goal state after:
case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
q : MvPolynomial ι' S
hq : ∃ a, (Q.ofComp P).toAlgHom a = q
p : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + q
Module: Mathlib.RingTheory.Extension.Cotangent.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'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker ^ 2

Tactic:
rw [pow_two]

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'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker * P'.ker
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
ι : Type u_2
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : ι → Ideal R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) =
    ↑(piLeft R M fun i ↦ R ⧸ I i).symm ∘ₗ
      (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)

Tactic:
by
  ext; simp [LinearMap.pi, LinearEquiv.piCongrRight]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
by
  let g : S →ₐ[R] S' :=
    AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one]
  have g_apply : ∀ x, g x = algebraMap S S' x := fun _ => rfl
  -- We first obtain the `y' ∈ M` such that `s' = y' • s` is falls in the image of `S` in `S'`.
  let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S)) s
  have hx₁ : (y : S) • (s : Set S') = g '' _ :=
    (IsLocalization.finsetIntegerMultiple_image _ s).symm
  obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop
  have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by
    simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
  rw [← e, this] at hx₁
  replace hx₁ := congr_arg (Submodule.span R) hx₁
  rw [Submodule.span_smul] at hx₁
  replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx
  rw [hx₁, ← g_apply, ← map_smul g, g_apply, ← Algebra.linearMap_apply, ← AlgHom.coe_toLinearMap,
    ← Submodule.map_span] at hx
  -- Since `x` falls in the span of `s` in `S'`, `y' • x : S` falls in the span of `s'` in `S'`.
  -- That is, there exists some `x' : S` in the span of `s'` in `S` and `x' = y' • x` in `S'`.
  -- Thus `a • (y' • x) = a • x' ∈ span s'` in `S` for some `a ∈ M`.
  obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx
  obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ :=
    (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx''
  use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M)
  convert!
    (Submodule.span R
          (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s :
            Set S)).smul_mem
      a hx' using 1
  convert! ha₂.symm using 1
  · rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul]
    exact Algebra.smul_def _ _
  · exact Algebra.smul_def _ _

Goal state after:
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
⊢ (ker f).FG

Tactic:
by
  apply Ideal.fg_of_localizationSpan t ht
  intro g
  rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)]
  exact H g

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := ⋯
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := ⋯
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := ⋯
i : (κ × ι →₀ R) →ₗ[R] S := ⋯
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
h : Function.Injective ⇑i
x : κ × ι
⊢ (i ∘ₗ Finsupp.lsingle x) 1 = ((Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)) ∘ₗ Finsupp.lsingle x) 1

Tactic:
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ p ∈ x.lifts ↔ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x

Tactic:
simp only [lifts, Set.mem_ofPred_eq, FreeAddMonoid.toPiTensorProduct]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := ⋯
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := ⋯
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := ⋯
i : (κ × ι →₀ R) →ₗ[R] S := ⋯
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
h : Function.Injective ⇑i
x : κ × ι
⊢ (i ∘ₗ Finsupp.lsingle x) 1 = ((Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)) ∘ₗ Finsupp.lsingle x) 1

Tactic:
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ x ∈ s, f x • v x + f n✝ • v n✝ = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ i ∈ s, f i • (v + fun x ↦ c x • v ↑n) i = 0

Tactic:
hfn

Goal state after:
case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ i ∈ s, f i • (v + fun x ↦ c x • v ↑n) i = 0