-- Mathlib/Algebra/Lie/Submodule.lean
theorem iSup_induction' {ι} (N : ι → LieSubmodule R L M) {C : (x : M) → (x ∈ ⨆ i, N i) → Prop}
    (hN : ∀ (i) (x) (hx : x ∈ N i), C x (mem_iSup_of_mem i hx)) (h0 : C 0 (zero_mem _))
    (hadd : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, N i) : C x hx

Proof state:
case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x →
    (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) (x + y)

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

Result:
case refine_3.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
w✝¹ : x ∈ ⨆ i, N i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, N i
Cy : C y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, N i), C (x + y) hx

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ C x hx

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

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (x_1 : x ∈ ⨆ i, N i), C x x_1

Proof state:
case refine_3.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
w✝¹ : x ∈ ⨆ i, N i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, N i
Cy : C y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, N i), C (x + y) hx

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

Result:
no goals

Proof state:
case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) 0

Tactic:
exact ⟨_, h0⟩

Result:
no goals

Proof state:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, N i
i : ι
x : M
hx : x ∈ N i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x

Tactic:
exact ⟨_, hN _ _ hx⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (x_1 : x ∈ ⨆ i, N i), C x x_1

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

Result:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, N i
i : ι
x : M
hx : x ∈ N i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x

case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) 0

case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : (x : M) → x ∈ ⨆ i, N i → Prop
hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯
h0 : C 0 ⋯
hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
⊢ (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x →
    (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) (x + y)