no goals
α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x
induction x using FreeCommRing.induction_on with
| hn1 =>
  use -1
  rfl
| hb b =>
  exact ⟨FreeRing.of b, rfl⟩
| ha _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
| hm _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
case hn1
α : Type u
⊢ ↑(-1) = -1
case hn1
α : Type u
⊢ ∃ a, ↑a = -1
use -1
no goals
case hn1
α : Type u
⊢ ↑(-1) = -1
rfl
no goals
case hb
α : Type u
b : α
⊢ ∃ a, ↑a = FreeCommRing.of b
exact ⟨FreeRing.of b, rfl⟩
case ha.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝
case ha
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝
rcases hx with ⟨x, rfl⟩
case ha.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y
case ha.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝
rcases hy with ⟨y, rfl⟩
no goals
case ha.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
case hm.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝
case hm
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝
rcases hx with ⟨x, rfl⟩
case hm.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x * ↑y
case hm.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝
rcases hy with ⟨y, rfl⟩
no goals
case hm.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x * ↑y
exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩