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

Goal state before:
pp: case pos
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 ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1

pp: case neg
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 ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1

Tactic:
·

Goal state after:
case pos
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 ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
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 / J) = map (↑h) I / map (↑h) J

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₁
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 / J) = map (↑h) I / map (↑h) J

Tactic:
·

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) (I / J) = map (↑h) I / map (↑h) J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case pos
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
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1

pp: case neg
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
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1

Tactic:
·

Goal state after:
case pos
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
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1
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 / J) = map (↑h) I / map (↑h) J

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₁
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 / J) = map (↑h) I / map (↑h) J

Tactic:
· rw [H, div_zero, FractionalIdeal.map_zero, div_zero]

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₁
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 / J) = map (↑h) I / map (↑h) J
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₁
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 / J) = map (↑h) I / map (↑h) J

Tactic:
·

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₁
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 / J) = map (↑h) I / map (↑h) J
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:
·

Goal state after:
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
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I → ∃ x', (algebraMap K L) x' = x

pp: case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ (∃ x', (algebraMap K L) x' = x) → x ∈ I

Tactic:
·

Goal state after:
case mp
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I → ∃ x', (algebraMap K L) x' = x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ (∃ x', (algebraMap K L) x' = x) → x ∈ I

Tactic:
·

Goal state after:
case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ (∃ x', (algebraMap K L) x' = x) → x ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ x ∈ f '' ↑s, IsInteger R₁ (↑a' • x)

pp: case refine_2
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ (↑a' • 0)

pp: case refine_3
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

pp: case refine_4
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
·

Goal state after:
case refine_1
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ x ∈ f '' ↑s, IsInteger R₁ (↑a' • x)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ (↑a' • 0)

pp: case refine_3
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

pp: case refine_4
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
·

Goal state after:
case refine_2
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ (↑a' • 0)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_3
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

pp: case refine_4
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
·

Goal state after:
case refine_3
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J I : FractionalIdeal A⁰ K
⊢ I / 0 = I * 0⁻¹

pp: case inr
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹

Tactic:
·

Goal state after:
case inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J I : FractionalIdeal A⁰ K
⊢ I / 0 = I * 0⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J ≤ I * J⁻¹

pp: case inr.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I * J⁻¹ * J ≤ I

Tactic:
·

Goal state after:
case inr.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J ≤ I * J⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_4
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
·

Goal state after:
case refine_4
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
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I * J⁻¹ * J ≤ I

Tactic:
·

Goal state after:
case inr.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I * J⁻¹ * J ≤ I
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

pp: case neg
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:
·

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 I
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]; apply Submodule.fg_bot

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
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0

Tactic:
·

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)
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
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0

Tactic:
·

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
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
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) → ∃ z, z • (algebraMap R P) x = y

pp: case mpr
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
x : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y

Tactic:
·

Goal state after:
case mp
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
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) → ∃ z, z • (algebraMap R P) x = y
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0

pp: case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥

Tactic:
·

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥

Tactic:
·

Goal state after:
case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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
x : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y

Tactic:
·

Goal state after:
case mpr
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
x : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

pp: case mpr
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
·

Goal state after:
case mp
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)