α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x _hx, ¬IsUnit x
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x _hx, ¬IsUnit x
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x h, ¬∃ b, x * b = 1
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x _hx, ¬IsUnit x
simp_rw [isUnit_iff_exists_inv]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : Exists fun {a} => a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x h, ¬∃ b, x * b = 1
push_neg  at this⊢
case intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : Exists fun {a} => a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
obtain ⟨x, hx, not_unit⟩ := this
no goals
case intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
exact ⟨x, hx, not_unit⟩