mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
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✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpolyAux b (Free.chooseBasis R M) =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)

Tactic:
φ.polyCharpolyAux_basisIndep b (Module.Free.chooseBasis R M) bₘ,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
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✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpolyAux b bₘ = Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A

Tactic:
by
      rw [J_inv]
      simp

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite n → A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ Infinite ?m.33

Tactic:
simpa using hfin

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite m → A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ Infinite ?m.33

Tactic:
simpa using hfin

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ LinearIndependent R (col 1)

Tactic:
convert! Pi.linearIndependent_single_one m R

Goal state after:
m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
x✝ : m
⊢ col 1 x✝ = Pi.single x✝ 1
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
a b : R[M]
ha : a ∈ {a | ∀ m ∈ a.coeff.support, f m = i}
hb : b ∈ {a | ∀ m ∈ a.coeff.support, f m = i}
m : M
h : m ∈ (a + b).coeff.support
⊢ f m = i

Tactic:
exact (Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ (coeAlgHom (gradeBy R ⇑f)).comp (decomposeAux f) = AlgHom.id R R[M]

Tactic:
ext; simp [decomposeAux_single]

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case refine_1
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
aux : radical k L = center k L
x : L
hx : x ∈ center k L
⊢ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
rw [← aux] at hx

Goal state after:
case refine_1
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
aux : radical k L = center k L
x : L
hx : x ∈ radical k L
⊢ (toEnd k L M) x ∈ k ∙ LinearMap.id
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ l.formPerm.IsCycle

Tactic:
rcases l with - | ⟨x, l⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
hn : 2 ≤ [].length
⊢ [].formPerm.IsCycle

case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
⊢ (x :: l).formPerm.IsCycle
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
u' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hu' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) u' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆
v' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hv' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) v' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆
⊢ (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) (u' + v') =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ +
      ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆

Tactic:
simp [← hu', ← hv']

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf → f x ≠ x

Tactic:
have ⟨l, hl⟩ := exists_toCycle_toList f hf
    simp only [hl, Cycle.mem_coe_iff, ne_eq]
    intro h
    have ⟨h1, h2⟩ := mem_toList_iff.mp h
    exact ((isCycle_iff_sameCycle (mem_support.mp h2)).mp (y := x) hf).mp h1

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ c i = c 1

Tactic:
refine congr_arg c (eq_of_le_of_not_lt' ?_ fun hi => ?_)

Goal state after:
case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ 1 ≤ i

case succ.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
hi : 1 < i
⊢ False
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
⊢ b ∈ Weight.ker

Tactic:
have hμ_root : μ ∈ H.root := by simpa [LieSubalgebra.root] using hμ

Goal state after:
case pos
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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
hμ_root : μ ∈ LieSubalgebra.root
⊢ b ∈ Weight.ker
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * (1 / I) = 1

Tactic:
by rwa [← eq_one_div_of_mul_eq_one_right I J hJ]

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

Goal state before:
pp: case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG I

Tactic:
rw [hI]

Goal state after:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG ⊥
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)
χ : 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
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
have h_h_containment : ⁅x_χ, (y : L)⁆ ∈ genWeightSpace L χ := by
    have h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L (0 : H → K) := by
      apply toLieSubmodule_le_rootSpace_zero
      exact y.property
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx_χ h_zero_weight
    ext h; simp
  have h_bracket_decomp : ⁅x_χ, m_α⁆ ∈
      genWeightSpace L (χ.toLinear + α.toLinear) ⊔
      genWeightSpace L (χ.toLinear - α.toLinear) ⊔ genWeightSpace L χ := by
    rw [h_bracket_sum]
    exact add_mem (add_mem
      (Submodule.mem_sup_left (Submodule.mem_sup_left h_pos_containment))
      (Submodule.mem_sup_left (Submodule.mem_sup_right h_neg_containment)))
      (Submodule.mem_sup_right h_h_containment)
  let I := ⨆ β : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot β.2.2
  have genWeightSpace_le_I (β_lin : H →ₗ[K] K) (hβ_in_q : β_lin ∈ q)
      (hβ_ne_zero : β_lin ≠ 0) : genWeightSpace L β_lin ≤ I := by
    by_cases h_trivial : genWeightSpace L β_lin = ⊥
    · simp [h_trivial]
    · 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)
  have h_plus_contain : genWeightSpace L (χ.toLinear + α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (q.add_mem h_chi_in_q hαq) w_plus
  have h_minus_contain : genWeightSpace L (χ.toLinear - α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (by
      have : -α.toLinear = (-1 : K) • α.toLinear := by simp
      rw [sub_eq_add_neg, this]
      exact q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)) w_minus
  have h_chi_contain : genWeightSpace L χ.toLinear ≤ I :=
    genWeightSpace_le_I _ h_chi_in_q (fun h_eq => (w_chi h_eq).elim)
  exact sup_le (sup_le h_plus_contain h_minus_contain) h_chi_contain h_bracket_decomp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ↑I.num ≤ I

Tactic:
rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]

Goal state after:
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
I : FractionalIdeal S P
⊢ ∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG

Tactic:
rw [hI]

Goal state after:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : ¬x = 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)

Tactic:
have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx

Goal state after:
case neg
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₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_2
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ a * 0 ∈ ↑J

pp: case refine_2.refine_3
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x y : K),
    x ∈ Submodule.span A (f '' ↑s) → y ∈ Submodule.span A (f '' ↑s) → a * x ∈ ↑J → a * y ∈ ↑J → a * (x + y) ∈ ↑J

pp: case refine_2.refine_4
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (a_1 : A), ∀ x ∈ Submodule.span A (f '' ↑s), a * x ∈ ↑J → a * a_1 • x ∈ ↑J

Tactic:
· rw [mul_zero]; exact Submodule.zero_mem _

Goal state after:
case refine_2.refine_3
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x y : K),
    x ∈ Submodule.span A (f '' ↑s) → y ∈ Submodule.span A (f '' ↑s) → a * x ∈ ↑J → a * y ∈ ↑J → a * (x + y) ∈ ↑J

case refine_2.refine_4
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (a_1 : A), ∀ x ∈ Submodule.span A (f '' ↑s), a * x ∈ ↑J → a * a_1 • x ∈ ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal R⁰ K
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (↑I * ↑J) =
    Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J

Tactic:
apply le_antisymm <;> simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]

Goal state after:
case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal R⁰ K
⊢ ∀ m ∈ I,
    ∀ n ∈ J,
      (IsFractionRing.ringEquivOfRingEquiv f) m * (IsFractionRing.ringEquivOfRingEquiv f) n ∈
        Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J

case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal R⁰ K
⊢ ∀ (m : L),
    (IsFractionRing.ringEquivOfRingEquiv f).symm m ∈ I →
      ∀ (n : L),
        (IsFractionRing.ringEquivOfRingEquiv f).symm n ∈ J →
          (IsFractionRing.ringEquivOfRingEquiv f).symm m * (IsFractionRing.ringEquivOfRingEquiv f).symm n ∈ ↑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)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
hsubset : (Set.range fun x ↦ f ↑x) ⊆ ↑f.range
⊢ span K ↑f.range = ⊤

Tactic:
rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Semiring K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
⊢ HasNoetherianRange 0

Tactic:
simp [HasNoetherianRange, isNoetherian_submodule, Submodule.fg_bot]

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
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
⊢ l.ker.FG

Tactic:
have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])

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
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
⊢ l.ker.FG