-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem iSup_induction' {ι : Sort*} (S : ι → Submonoid M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
    (mem : ∀ (i), ∀ (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i hxS)) (one : C 1 (one_mem _))
    (mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, S i) : C x hx

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ C x hx

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

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (Hx : x ∈ ⨆ i, S i), C x Hx

Proof state:
case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) 1

Tactic:
exact ⟨_, one⟩

Result:
no goals

Proof state:
case refine_3.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
w✝¹ : x ∈ ⨆ i, S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : C y w✝
⊢ ∃ (hm : x * y ∈ ⨆ i, S i), C (x * y) hm

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

Result:
no goals

Proof state:
case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x →
    (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) y → (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) (x * y)

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

Result:
case refine_3.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
w✝¹ : x ∈ ⨆ i, S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : C y w✝
⊢ ∃ (hm : x * y ∈ ⨆ i, S i), C (x * y) hm

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (Hx : x ∈ ⨆ i, S i), C x Hx

Tactic:
refine @iSup_induction _ _ ι S (fun m => ∃ hm, C m hm) _ hx (fun i x hx => ?_) ?_ fun x y => ?_

Result:
case refine_1
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : M
hx : x ∈ S i
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x

case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) 1

case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x →
    (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) y → (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) (x * y)

Proof state:
case refine_1
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
one : C 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : M
hx : x ∈ S i
⊢ (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x

Tactic:
exact ⟨_, mem _ _ hx⟩

Result:
no goals