case intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
cases' isMaximal_iff.1 hI with H₁ H₂
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
case intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
rcases mem_span_insert.1
    (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
      (subset_span (mem_insert _ _))) with
  ⟨y, z, hz, hy⟩
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
refine' ⟨y, z, _, hy.symm⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I
rwa [← span_eq I]