mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
P : PrimeSpectrum A
hprodZ : ¬(P.asIdeal ::ₘ (Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
⊢ P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
Multiset.prod_cons,

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
P : PrimeSpectrum A
hprodZ : ¬P.asIdeal * ((Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
⊢ P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case neg
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) ↑I.den) * I ≤ I⁻¹ * I

Tactic:
gcongr

Goal state after:
case h₁
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) ↑I.den) ≤ I⁻¹
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ genWeightSpace L (-⇑↑α) ≤ LieSubmodule.restr I H

Tactic:
apply I.rootSpace_le_of_apply_coroot_ne_zero hα
        simp [Pi.neg_apply, root_apply_coroot (H.isNonZero_coe_root α)]

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

Goal state before:
pp: case a
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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * J ≤ I * (I * J / I)

Tactic:
gcongr

Goal state after:
case h₂
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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J ≤ I * J / I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K :=
    FractionalIdeal.mapEquiv (FractionRing.algEquiv A K)

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
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 = ⊥
⊢ genWeightSpace L ⇑β_lin ≤ I

Tactic:
let β : Weight K H L := ⟨β_lin, h_trivial⟩
      have hβ_nonzero : β.IsNonZero := Weight.coe_toLinear_ne_zero_iff.mp hβ_ne_zero
      refine le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)
      rw [sl2SubmoduleOfRoot_eq_sup]
      exact le_sup_of_le_left (le_sup_of_le_left le_rfl)

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
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ (↑M)⁻¹ * ↑P * ((↑P)⁻¹ * ↑M) ≤ ↑P * ((↑P)⁻¹ * ↑M)

Tactic:
gcongr

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
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (↑M)⁻¹ * ↑P
⊢ (↑M)⁻¹ * ↑P ≤ (↑M)⁻¹ * ↑M

Tactic:
gcongr

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ (↑I)⁻¹ * ↑J ≤ (↑I)⁻¹ * ↑I

Tactic:
gcongr

Goal state after:
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
⊢ 1 = ⊤

Tactic:
Ideal.one_eq_top

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
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) +
        spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) ⊓
        spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) ((I ⊓ J) * (I ⊔ J)) =
    (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) (I * J)

Tactic:
← mul_add,

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
        (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I + spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) ⊓
        spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) ((I ⊓ J) * (I ⊔ J)) =
    (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) (I * J)
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)
hs : Cardinal.mk ↑s = Module.rank K N
⊢ span K ↑f.range = ⊤

Tactic:
← Module.finrank_eq_rank,

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)
hs : Cardinal.mk ↑s = ↑(finrank K N)
⊢ span K ↑f.range = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
        (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I + spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) ⊓
        spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) ((I ⊓ J) * (I ⊔ J)) =
    (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) (I * J)

Tactic:
← mul_add,

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) ⊓
        spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) ((I ⊓ J) * (I ⊔ J)) =
    (fun a ↦ a * spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den))) (I * J)
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f g : V →ₗ[K] V₂
hf : IsNoetherian K ↥f.range
hg : IsNoetherian K ↥g.range
⊢ IsNoetherian K ↥(f + g).range

Tactic:
exact isNoetherian_of_le (range_add_le f g)

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
f_surj : Function.Surjective ⇑↑f
fsym_surj : Function.Surjective ⇑↑f.symm
⊢ (idealFactorsFunOfQuotHom fsym_surj).comp (idealFactorsFunOfQuotHom f_surj) = OrderHom.id

Tactic:
· simpa using! idealFactorsFunOfQuotHom_comp f_surj fsym_surj

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : I * I ∣ span {a}
⊢ IsUnit I

Tactic:
rw [← span_singleton_generator I, span_singleton_mul_span_singleton,
      span_singleton_dvd_span_singleton_iff_dvd] at hI
    exact isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)

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

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

Tactic:
exact (Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
    rw [← hτ, Submodule.span_le]
    intro x hxσ
    simp only [s₁]
    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
    convert! smul_zero _
    exact hs' ⟨x, hxσ⟩

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
this : π.ker ≤ (s₁ • linearCombination R i).ker
⊢ ∃ h s, f ∘ₗ h = s • g
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : 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
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ C a • D f = a • D f

Tactic:
have : C (σ := σ) a • D f = D (C a * f) := by simp
  rw [this, C_mul', D.map_smul]

Goal state after:
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 • f1.choose ∈ R ∙ z

Tactic:
← Quotient.mk_eq_zero,

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
⊢ Submodule.Quotient.mk (p ^ k • f1.choose) = 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
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
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
⊢ ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Tactic:
refine ⟨s₀ * s₁ * s₂, (s₀ * s₁ * s₂).2, fun t ht ↦ ?_⟩

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
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
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
⊢ Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial (m - single i 1 + single i 1)) (↑(m i) * r) = (monomial m) (↑(m i) * r)

Tactic:
sub_add_single_one_cancel h

Goal state after:
case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial m) (↑(m i) * r) = (monomial m) (↑(m i) * r)
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
inst✝ : Module.Finite R M
⊢ ∃ x, (toSpanSingleton R M x).ker = annihilator R M

Tactic:
have ⟨m, ι, _, p, irr, n, ⟨e⟩⟩ := equiv_free_prod_directSum (R := R) (M := M)

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
inst✝ : Module.Finite R M
m : ℕ
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
⊢ ∃ x, (toSpanSingleton R M x).ker = annihilator R M
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : x ∈ Ideal.span (Set.range ((⇑e ∘ ⇑↑TensorProduct.includeRight) ∘ P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
convert! H'

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : x ∈ Ideal.span (Set.range ((⇑e ∘ ⇑↑TensorProduct.includeRight) ∘ P.relation))
x✝ : σ
⊢ (MvPolynomial.map (algebraMap R T)) (P.relation x✝) = ((⇑e ∘ ⇑↑TensorProduct.includeRight) ∘ P.relation) x✝
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 α)
⊢ (invtSubmoduleToLieIdeal (↑q) hq).toInvtRootSubmodule = q

Tactic:
simp only [Subtype.ext_iff, LieIdeal.toInvtRootSubmodule, LieIdeal.rootSpan, LieIdeal.rootSet]
  conv_rhs => rw [RootPairing.invtRootSubmodule.eq_span_root q]
  congr 2; ext α
  exact mem_rootSet_invtSubmoduleToLieIdeal _ _

Goal state after: