-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem closure_induction {p : (x : M) → x ∈ span R s → Prop}
    (zero : p 0 (Submodule.zero_mem _))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
    (smul_mem : ∀ (r x) (h : x ∈ s), p (r • x) (Submodule.smul_mem _ _ <| subset_span h)) {x}
    (hx : x ∈ span R s) : p x hx

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
v : M
⊢ v ∈ span R s ↔ v ∈ closure (univ • s)

Tactic:
simp [← span_eq_closure]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x y : M) (hx : x ∈ closure (univ • s)) (hy : y ∈ closure (univ • s)),
    (fun x hx => p x ⋯) x hx → (fun x hx => p x ⋯) y hy → (fun x hx => p x ⋯) (x + y) ⋯

Tactic:
simpa only [key] using add

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x✝ : M
hx✝ : x✝ ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
r : R
left✝ : r ∈ univ
x : M
hx : x ∈ s
⊢ p ((fun x1 x2 => x1 • x2) r x) ⋯

Tactic:
exact smul_mem r x hx

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ p x hx

Tactic:
refine AddSubmonoid.closure_induction (p := fun x hx ↦ p x (key.mpr hx))
  ?_ zero (by simpa only [key] using add) (key.mp hx)

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x : M) (h : x ∈ univ • s), (fun x hx => p x ⋯) x ⋯

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ p x hx

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x : M) (h : x ∈ univ • s), (fun x hx => p x ⋯) x ⋯

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x✝ : M
hx✝ : x✝ ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
r : R
left✝ : r ∈ univ
x : M
hx : x ∈ s
⊢ p ((fun x1 x2 => x1 • x2) r x) ⋯