mathlib-initiative/mathlib-tactics huggingface dataset:
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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ I * J

Tactic:
mul_comm

Goal state after:
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
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ J * 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
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
⊢ J = 1 / I

Tactic:
by
  have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h
  suffices h' : I * (1 / I) = 1 from
    congr_arg Units.inv <| @Units.ext _ _ (Units.mkOfMulEqOne _ _ h) (Units.mkOfMulEqOne _ _ h') rfl
  apply le_antisymm
  · apply mul_le.mpr _
    intro x hx y hy
    rw [mul_comm]
    exact (mem_div_iff_of_ne_zero hI).mp hy x hx
  rw [← h]
  gcongr
  apply (le_div_iff_of_ne_zero hI).mpr _
  intro y hy x hx
  rw [mul_comm]
  exact mul_mem_mul hy hx

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

Goal state before:
pp: case pos
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₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) (I / 0) = map (↑h) I / map (↑h) 0

Tactic:
div_zero,

Goal state after:
case pos
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₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) 0 = map (↑h) I / map (↑h) 0
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✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
this : x ∈ integralClosure A K
⊢ x ∈ 1

Tactic:
rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
      ← mem_one_iff] at this

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
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
x : R
H : x ∈ ↑⊤.annihilator
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x ∈ ⊤.annihilator, x ≠ 0

Tactic:
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩

Goal state after:
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
hI : I ≠ 0
hJ : J ≠ 0
⊢ I * J ≤ 1 ↔ J * I ≤ 1

Tactic:
mul_comm

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
hI : I ≠ 0
hJ : J ≠ 0
⊢ J * I ≤ 1 ↔ J * I ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

Tactic:
rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
      exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩

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

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
this : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
⊢ Module A (⨁ (i : ιM), ↥(𝓜 i))

Tactic:
infer_instance

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

Goal state before:
pp: case inl
K : Type u_3
inst✝ : Field K
⊢ factors (span {0}) = Multiset.map (fun q ↦ span {q}) (factors 0)

Tactic:
simpa [Set.singleton_zero] using! normalizedFactors_zero

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsTorsionFree R K
M : Submodule R V
inst✝ : IsLattice K M
this : IsTorsionFree R V
⊢ Free R ↥M

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
this : IsNoetherian R ↥(M ⊓ N)
⊢ Module.Finite R ↥(M ⊓ N)

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V₂
inst✝² : Module K V₂
inst✝¹ : AddCommMonoid V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
h : IsNoetherian K ↥u.range
v : V₂ →ₗ[K] V₃
⊢ IsNoetherian K ↥(map v u.range)

Tactic:
infer_instance

Goal state after:
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₂
inst✝ : IsNoetherianRing K
u : V →ₗ[K] V₂
h : u.HasFiniteRange
this : Module.Finite K ↥u.range
⊢ IsNoetherian K ↥u.range

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u : V →ₗ[K] V₂
⊢ u ≈ 0 ↔ u.HasFiniteRange

Tactic:
by
  simp [equiv_iff_hasFiniteRange]

Goal state after:
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 : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
mul_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
⊢ a ∈ I ^ n ∨ b ∈ I
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 ↥(comap f g.ker)

Tactic:
infer_instance

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
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₄
this : FiniteDimensional k ↥(g ∘ₗ f).ker
⊢ FiniteDimensional k (P ⧸ map g f.range)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ IsLocalizedModule.Away (r * ↑u) f

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ IsLocalizedModule.Away (↑u * r) f
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'
⊢ J * K ∣ K * I'

Tactic:
mul_comm

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'
⊢ K * J ∣ K * I'
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬P.IsPrime
hJ : I ≤ J
hK : I ≤ K
⊢ I ≤ J * K

Tactic:
simp only [← dvd_iff_le] at coprime hJ hK ⊢
  by_cases hJ0 : J = 0
  · simpa only [hJ0, zero_mul] using hJ
  obtain ⟨I', rfl⟩ := hK
  rw [mul_comm]
  refine mul_dvd_mul_left K
    (UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors (b := K) hJ0 ?_ hJ)
  exact fun hPJ hPK => mt isPrime_of_prime (coprime _ hPJ hPK)

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

Goal state before:
pp: case hs2
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
⊢ Module.Finite R ↥l.ker

Tactic:
infer_instance

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

Goal state before:
pp: case refine_3
R : Type u_3
M✝ : Type ?u.7
N : Type ?u.12
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι✝ : Sort ?u.18
inst✝⁴ : Finite ι✝
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), FinitePresentation R (M i)
inst✝ : Finite ι
⊢ FinitePresentation R PUnit.{u_2 + 1}

Tactic:
infer_instance

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

Goal state before:
pp: case refine_4
R : Type u_3
M✝ : Type ?u.7
N✝ : Type ?u.12
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R N✝
ι✝ : Sort ?u.18
inst✝⁸ : Finite ι✝
ι : Type u_1
M : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommGroup (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : ∀ (i : ι), FinitePresentation R (M i)
inst✝⁴ : Finite ι
N : Type u_2
N' : Type (max u_2 u_1)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N
inst✝ : Module R N'
hN : FinitePresentation R N
hN' : FinitePresentation R N'
⊢ FinitePresentation R (N × N')

Tactic:
infer_instance

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

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = (p ^ k * a) • y

Tactic:
mul_comm

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = (a * p ^ k) • y
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
x✝ : M
⊢ Decidable (x✝ = 0)

Tactic:
infer_instance

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

Goal state before:
pp: case pos.hx
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
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
hx_χ_in_sl2 : x_χ ∈ sl2SubalgebraOfRoot hα₀
⊢ x_χ ∈ sl2SubalgebraOfRoot ⋯

Tactic:
exact hx_χ_in_sl2

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

Goal state before:
pp: case pos.hx
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
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
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
hx_χ_in_sl2 : x_χ ∈ sl2SubalgebraOfRoot hα₀
⊢ x_χ ∈ sl2SubalgebraOfRoot ⋯

Tactic:
exact hx_χ_in_sl2

Goal state after:
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.map (↑e.toRingEquiv) (Ideal.map (↑TensorProduct.includeRight) (Ideal.span (Set.range P.relation)))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
Ideal.map_map,

Goal state after:
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.map ((↑e.toRingEquiv).comp ↑TensorProduct.includeRight) (Ideal.span (Set.range P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.RingTheory.Extension.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
x : P.Ring
hx : x ∈ P.ker
⊢ ⟨x, hx⟩ ∈ mk.ker ↔ ⟨x, hx⟩ ∈ P.ker • ⊤

Tactic:
simp [LinearMap.mem_ker, mk_eq_zero_iff, Submodule.mem_smul_top_iff, sq]

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
y : P.Ring
y_in : y ∈ P.ker ^ 2
z : P.Ring
z_in : z ∈ RingHom.ker f.toRingHom
hyz : z = ↑x - y
⊢ z ∈ P.ker

Tactic:
exact hyz ▸ Ideal.sub_mem _ x.prop (Ideal.pow_le_self (show 2 ≠ 0 by lia) y_in)

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M → ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
intro

Goal state after:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 1}

Tactic:
infer_instance

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
ι' : 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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ C ((algebraMap R S) a) * ((v₁.prod fun x x2 ↦ X x ^ x2) * C (v₂.prod fun a ↦ HPow.hPow (P.val a))) =
    C ((algebraMap R S) a) * (C (v₂.prod fun i k ↦ P.val i ^ k) * v₁.prod fun n e ↦ X n ^ e)

Tactic:
mul_comm

Goal state after:
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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ C ((algebraMap R S) a) * (C (v₂.prod fun a ↦ HPow.hPow (P.val a)) * v₁.prod fun x x2 ↦ X x ^ x2) =
    C ((algebraMap R S) a) * (C (v₂.prod fun i k ↦ P.val i ^ k) * v₁.prod fun n e ↦ X n ^ e)
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
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
⊢ RingHom.ker (algebraMap P S) ≤ RingHom.ker ((algebraMap S A).comp (algebraMap P S))

Tactic:
intro

Goal state after:
R : Type u
S : Type v
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P✝ : Extension R S
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
x✝ : P
⊢ x✝ ∈ RingHom.ker (algebraMap P S) → x✝ ∈ RingHom.ker ((algebraMap S A).comp (algebraMap P S))
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst✝ : Fintype κ
e : κ ≃ ι
⊢ VanishesTrivially R (f ∘ ⇑e) (x ∘ ⇑e) ↔ VanishesTrivially R f x

Tactic:
e.vanishesTrivially_comp

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

Goal state before:
pp: case refine_1
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'
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''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝³ : Algebra P.Ring S' := ⋯
this✝² : IsScalarTower P.Ring S S'
this✝¹ : Algebra P.Ring P'.Ring := ⋯
this✝ : IsScalarTower P.Ring P'.Ring S'
this : IsScalarTower R P.Ring S'
⊢ ((↑R Cotangent.mk ∘ₗ f.subToKer g) 1).val = Cotangent.val 0

Tactic:
simp [Ideal.toCotangent_eq_zero]

Goal state after: