mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ n.succ < n + 1 + 1

Tactic:
·

Goal state after:
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ n.succ < n + 1 + 1
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ P (map (Quotient.mk (I ^ 2)) I)

Tactic:
·

Goal state after:
case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ P (map (Quotient.mk (I ^ 2)) I)
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

pp: case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
·

Goal state after:
case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) x ∈ I

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) x ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
·

Goal state after:
case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z) →
    ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) →
    ∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z) →
    ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) →
    ∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) →
    ∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
h : ((IsLocalizedModule.map p f f') g) x = 0
⊢ ∃ m, g m = 0 ∧ ∃ s, mk' f m s = x

pp: case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ (∃ m, g m = 0 ∧ ∃ s, mk' f m s = x) → ((IsLocalizedModule.map p f f') g) x = 0

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
h : ((IsLocalizedModule.map p f f') g) x = 0
⊢ ∃ m, g m = 0 ∧ ∃ s, mk' f m s = x
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

pp: case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)

Tactic:
·

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)

Tactic:
·

Goal state after:
case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case pos
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit ((mk (I ^ n)) x)

pp: case neg
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n ≠ 0
⊢ IsUnit ((mk (I ^ n)) x)

Tactic:
·

Goal state after:
case pos
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit ((mk (I ^ n)) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ (∃ m, g m = 0 ∧ ∃ s, mk' f m s = x) → ((IsLocalizedModule.map p f f') g) x = 0

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ (∃ m, g m = 0 ∧ ∃ s, mk' f m s = x) → ((IsLocalizedModule.map p f f') g) x = 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂ → J₁ ≤ J₂

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂ → J₁ ≤ J₂
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ Ideal.under R J ≠ ⊤

pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ Ideal.under R J ≠ ⊤
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime

Tactic:
· refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
    · refine fun hJ => h.ne_top ?_
      rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
      exact le_of_eq hJ.symm
    · intro x y hxy
      rw [Ideal.mem_comap, map_mul] at hxy
      exact h.mem_or_mem hxy

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.under R J

pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
·

Goal state after:
case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.under R J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
·

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ J = ⊤ → ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ J = ⊤ → ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' →
    I ≤ I'

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I I' : { p // p.IsPrime }
⊢ I ≤ I' →
    { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I'

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' →
    I ≤ I'
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I ≤ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)

pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I ≤ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A) 0) = 0

pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A) 0) = 0
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y