-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem closure_induction' {s : Set R} {p : closure s → Prop} (a : closure s)
    (mem : ∀ (x) (hx : x ∈ s), p ⟨x, subset_closure hx⟩) (zero : p 0)
    (add : ∀ x y, p x → p y → p (x + y)) (neg : ∀ x, p x → p (-x))
    (mul : ∀ x y, p x → p y → p (x * y)) : p a :=
  Subtype.recOn a fun b hb => by
    induction hb using closure_induction with
    | mem x hx => exact mem x hx
    | zero => exact zero
    | add x y hx hy h₁ h₂ => exact add _ _ h₁ h₂
    | neg x hx h => exact neg _ h
    | mul x y hx hy h₁ h₂ => exact mul _ _ h₁ h₂

Proof state:
case add
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b x y : R
hx : x ∈ closure s
hy : y ∈ closure s
h₁ : p ⟨x, hx⟩
h₂ : p ⟨y, hy⟩
⊢ p ⟨x + y, ⋯⟩

Tactic:
exact add _ _ h₁ h₂

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b : R
⊢ p ⟨0, ⋯⟩

Tactic:
exact zero

Result:
no goals

Proof state:
case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b x : R
hx : x ∈ s
⊢ p ⟨x, ⋯⟩

Tactic:
exact mem x hx

Result:
no goals

Proof state:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b x y : R
hx : x ∈ closure s
hy : y ∈ closure s
h₁ : p ⟨x, hx⟩
h₂ : p ⟨y, hy⟩
⊢ p ⟨x * y, ⋯⟩

Tactic:
exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ p ⟨b, hb⟩

Tactic:
induction hb using closure_induction with
| mem x hx => exact mem x hx
| zero => exact zero
| add x y hx hy h₁ h₂ => exact add _ _ h₁ h₂
| neg x hx h => exact neg _ h
| mul x y hx hy h₁ h₂ => exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : ↥(closure s) → Prop
a : ↥(closure s)
mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩
zero : p 0
add : ∀ (x y : ↥(closure s)), p x → p y → p (x + y)
neg : ∀ (x : ↥(closure s)), p x → p (-x)
mul : ∀ (x y : ↥(closure s)), p x → p y → p (x * y)
b x : R
hx : x ∈ closure s
h : p ⟨x, hx⟩
⊢ p ⟨-x, ⋯⟩

Tactic:
exact neg _ h

Result:
no goals