mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case mpr
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
inst✝ : (↑I).IsPrincipal
⊢ generator ↑I ≠ 0 → I * I⁻¹ = 1

Tactic:
intro hg

Goal state after:
case mpr
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
inst✝ : (↑I).IsPrincipal
hg : generator ↑I ≠ 0
⊢ I * I⁻¹ = 1
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
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
⊢ ∃ Z, (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
have := Multiset.map_erase asIdeal (fun _ _ => PrimeSpectrum.ext) P Z
    obtain ⟨hP0, hZP0⟩ : P.asIdeal ≠ ⊥ ∧ ((Z.erase P).map asIdeal).prod ≠ ⊥ := by
      rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
        this] at hprodZ
    -- By maximality of `P` and `M`, we have that `P ≤ M` implies `P = M`.
    have hPM' := (P.isPrime.isMaximal hP0).eq_of_le hM.ne_top hPM
    subst hPM'
    -- By minimality of `Z`, erasing `P` from `Z` is exactly what we need.
    refine ⟨Z.erase P, ?_, ?_⟩
    · convert! hZI
      rw [this, Multiset.cons_erase hPZ']
    · refine fun h => h_eraseZ (Z.erase P) ⟨h, ?_⟩ (Multiset.erase_lt.mpr hPZ)
      exact hZP0

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
⊢ ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I

Tactic:
obtain ⟨y : K, y_mem, y_notMem⟩ :=
    SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr hI)
  have y_ne_zero : y ≠ 0 := by simpa using y_notMem
  obtain ⟨z, ⟨x, hx⟩⟩ := exists_integer_multiple R⁰ y
  refine ⟨x, ?_, ?_⟩
  · rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]
    exact mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero
  · rw [hx]
    exact smul_mem _ _ y_mem

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 * (1 / I) ≤ 1

Tactic:
apply mul_le.mpr _
    intro x hx y hy
    rw [mul_comm]
    exact (mem_div_iff_of_ne_zero hI).mp hy x hx

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_1
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
i : ι
hi : i ∈ ↑s
⊢ a * f i ∈ ↑J

Tactic:
exact hpI i hi

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

Goal state before:
pp: 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
⊢ (ringEquivOfRingEquiv K L f).symm = ringEquivOfRingEquiv L K f.symm

Tactic:
exact (RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm
          (ringEquivOfRingEquiv L K f.symm)).mpr rfl

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

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

Tactic:
factors_eq_normalizedFactors,

Goal state after:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q ↦ span {q}) (factors p), Prime q
⊢ normalizedFactors (Multiset.map (fun x ↦ span {x}) (factors p)).prod = Multiset.map (fun q ↦ span {q}) (factors p)
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 K V + Module.rank K V
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)

Tactic:
IsLattice.rank'

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 K V + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank K V
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
or_comm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n
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)
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
have aux : f.range ≤ comap g (g ∘ₗ f).range := by rw [← map_le_iff_le_comap, range_comp]
  let f₀ : f.ker →ₗ[k] (g ∘ₗ f).ker := inclusion <| ker_le_ker_comp f g
  let f₁ : (g ∘ₗ f).ker →ₗ[k] g.ker := f.restrict <| by simp
  let f₂ : g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
  let f₃ : (N ⧸ f.range) →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
  let f₄ : (P ⧸ (g ∘ₗ f).range) →ₗ[k] P ⧸ g.range := factor <| range_comp_le_range f g
  have h₀ : Injective f₀ := inclusion_injective _
  have h₁ : Exact f₀ f₁ := by rw [exact_iff]; simp [f₀, f₁, ker_restrict, range_inclusion]
  have h₂ : Exact f₁ f₂ := by rw [exact_iff]; simp [f₁, f₂, ker_comp, map_comap_eq]
  have h₃ : Exact f₂ f₃ := by rw [exact_iff]; simp [f₂, f₃, range_comp, ker_mapQ, comap_map_eq]
  have h₄ : Exact f₃ f₄ := by rw [exact_iff]; simp [f₃, f₄, factor, ker_mapQ, range_mapQ]
  have h₅ : Surjective f₄ := factor_surjective _
  have : FiniteDimensional k (g ∘ₗ f).ker := by rw [ker_comp]; infer_instance
  have : FiniteDimensional k (P ⧸ (g ∘ₗ f).range) := by rw [range_comp]; infer_instance
  grind [index, sum_neg_one_pow_finrank_eq_zero_of_exact_six f₀ f₁ f₂ f₃ f₄ h₀ h₁ h₂ h₃ h₄ h₅]

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✝² : Field k
inst✝¹ : Module k M
inst✝ : Module k N
f : M →ₗ[k] N
t : k
ht : t ≠ 0
⊢ ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ (t • f).range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))

Tactic:
range_smul _ _ ht

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
k : Type u_3
inst✝² : Field k
inst✝¹ : Module k M
inst✝ : Module k N
f : M →ₗ[k] N
t : k
ht : t ≠ 0
⊢ ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ K * J ∣ K * I'

Tactic:
refine mul_dvd_mul_left K
    (UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors (b := K) hJ0 ?_ hJ)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ ∀ {d : Ideal R}, d ∣ J → d ∣ K → ¬Prime d
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ f ((∏ j ∈ s.erase i, (sec j).2) • (sec i).1) = ↑(∏ i ∈ s, (sec i).2) • g i

Tactic:
simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finsetProd]

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ (∏ j ∈ s.erase i, (sec j).2) • f (sec i).1 = (∏ i ∈ s, ↑(sec i).2) • g i
Module: Mathlib.Algebra.Module.LocalizedModule.Int

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

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples S f Finset.univ g

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Tactic:
simp only [normalize_apply, this]

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
⊢ π.ker ≤ (s₁ • linearCombination R i).ker

Tactic:
rw [← hτ, Submodule.span_le]

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
⊢ ↑τ ⊆ ↑(s₁ • linearCombination R i).ker
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
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p ↦ torsionBy R M (IsPrincipal.generator ↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
by
  convert! isInternal_prime_power_torsion hM
  rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mem
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
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
χ : Weight K (↥H) L
x_χ : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
⊢ ⁅x_χ, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
| mem χ x_χ hx_χ =>

Goal state after:
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:
by
    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.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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
⊢ invtSubmoduleToLieIdeal I.rootSpan hI = I

Tactic:
set J := invtSubmoduleToLieIdeal I.rootSpan
    ((rootSystem H).mem_invtRootSubmodule_iff.mp I.rootSpan_mem_invtRootSubmodule)

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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
⊢ J = I
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case e_g
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      ((aeval (⇑C ∘ P.val)) (P.σ s) *
        ((algebraMap R (MvPolynomial ι' S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (AddMonoidAlgebra.ofCoeff (Finsupp.single u s))

Tactic:
simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom, map_one, one_mul, AddMonoidAlgebra.ofCoeff_single,
    single_eq_monomial]

Goal state after:
case e_g
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 ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      (eval₂ (algebraMap R (MvPolynomial ι' S)) (⇑C ∘ P.val) (P.σ s) *
        (Finsupp.mapDomain Sum.inl u).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k) =
    coeff m ((monomial u) s)
Module: Mathlib.RingTheory.Extension.Generators

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

Tactic:
let X := P.σ b
    use a • MvPolynomial.map (algebraMap R T) X
    simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
    have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]
    rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ ∃ a, (aeval (Sum.elim P.val b)) a = s

Tactic:
by
    use rename Sum.inl (P.σ s)
    simp [aeval_rename]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
v : ι' ⊕ ι →₀ ℕ
a : R
⊢ (∑ i_1 ∈ Finset.map (↑e).toEmbedding ((monomial v) a).support,
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) ((monomial v) a))) else 0) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial v) a))

Tactic:
← Finset.sum_filter

Goal state after:
case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
v : ι' ⊕ ι →₀ ℕ
a : R
⊢ ∑ a_1 ∈ Finset.map (↑e).toEmbedding ((monomial v) a).support with a_1.1 = i,
      (aeval P.val) ((monomial a_1.2) (coeff (e.symm a_1) ((monomial v) a))) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial v) a))
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hmn : VanishesTrivially R m n
⊢ ∑ i, m i ⊗ₜ[R] n i = 0

Tactic:
by
  obtain ⟨k, a, y, h₁, h₂⟩ := hmn
  simp_rw [h₁, tmul_sum, tmul_smul]
  rw [Finset.sum_comm]
  simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]

Goal state after: