-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {C : ∀ x, (x ∈ ⨆ i, p i) → Prop}
    (mem : ∀ (i) (x) (hx : x ∈ p i), C x (mem_iSup_of_mem i hx)) (zero : C 0 (zero_mem _))
    (add : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, p i) : C x hx

Proof state:
case refine_3.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
w✝¹ : x ∈ ⨆ i, p i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, p i
Cy : C y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, p i), C (x + y) hx

Tactic:
exact ⟨_, add _ _ _ _ Cx Cy⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ ∃ (x_1 : x ∈ ⨆ i, p i), C x x_1

Tactic:
refine iSup_induction p (C := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), C x hx) hx
  (fun i x hx => ?_) ?_ fun x y => ?_

Result:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, p i
i : ι
x : M
hx : x ∈ p i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) 0

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x →
    (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) (x + y)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ C x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : C x hx) => hc

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ ∃ (x_1 : x ∈ ⨆ i, p i), C x x_1

Proof state:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, p i
i : ι
x : M
hx : x ∈ p i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x

Tactic:
exact ⟨_, mem _ _ hx⟩

Result:
no goals

Proof state:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x →
    (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) (x + y)

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩

Result:
case refine_3.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
w✝¹ : x ∈ ⨆ i, p i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, p i
Cy : C y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, p i), C (x + y) hx

Proof state:
case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯
zero : C 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) 0

Tactic:
exact ⟨_, zero⟩

Result:
no goals