ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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, C x₁ x
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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 ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
case refine_1
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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 x' => ∃ hx'', C x' hx'') x₂

case refine_2
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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 x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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, C x₁ x
refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
    (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
no goals
case refine_1
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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 x' => ∃ hx'', C x' hx'') x₂
exact ⟨_, hp _ _ hx₂⟩
case refine_2.intro.intro
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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✝
⊢ ∃ hx'', C (x₃ * y) hx''
case refine_2
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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 x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
no goals
case refine_2.intro.intro
ι : Sort u_2
M : Type u_1
A : Type ?u.9929
B : Type ?u.9932
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (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✝
⊢ ∃ hx'', C (x₃ * y) hx''
exact ⟨_, hmul _ _ _ _ Cx Cy⟩