M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ Hx, C x Hx
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ C x hx
refine' Exists.elim (_ : ∃ Hx, C x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : C x hx) => hc
case refine'_1
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : M
hx : x ∈ S i
⊢ (fun m => ∃ hm, C m hm) x

case refine'_2
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun m => ∃ hm, C m hm) 1

case refine'_3
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), S i
x y : M
⊢ (fun m => ∃ hm, C m hm) x → (fun m => ∃ hm, C m hm) y → (fun m => ∃ hm, C m hm) (x * y)
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ Hx, C x Hx
refine' @iSup_induction _ _ ι S (fun m => ∃ hm, C m hm) _ hx (fun i x hx => _) _ fun x y => _
no goals
case refine'_1
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : M
hx : x ∈ S i
⊢ (fun m => ∃ hm, C m hm) x
exact ⟨_, hp _ _ hx⟩
no goals
case refine'_2
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun m => ∃ hm, C m hm) 1
exact ⟨_, h1⟩
case refine'_3.intro.intro
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
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, C (x * y) hm
case refine'_3
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), S i
x y : M
⊢ (fun m => ∃ hm, C m hm) x → (fun m => ∃ hm, C m hm) y → (fun m => ∃ hm, C m hm) (x * y)
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
no goals
case refine'_3.intro.intro
M : Type u_2
A : Type ?u.48124
B : Type ?u.48127
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
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, C (x * y) hm
refine' ⟨_, hmul _ _ _ _ Cx Cy⟩