α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
this : ∃ h, C x h
⊢ C x hx

case this
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ C x hx
suffices : ∃ h, C x h
case this
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
this : ∃ h, C x h
⊢ C x hx

case this
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
exact this.snd
case this.refine'_1
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : G
hx : x ∈ S i
⊢ (fun x => ∃ h, C x h) x

case this.refine'_2
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun x => ∃ h, C x h) 1

case this.refine'_3
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
⊢ (fun x => ∃ h, C x h) x → (fun x => ∃ h, C x h) y → (fun x => ∃ h, C x h) (x * y)
case this
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
refine' iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => _) _ fun x y => _
no goals
case this.refine'_1
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : G
hx : x ∈ S i
⊢ (fun x => ∃ h, C x h) x
exact ⟨_, hp i _ hx⟩
no goals
case this.refine'_2
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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 : G
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun x => ∃ h, C x h) 1
exact ⟨_, h1⟩
case this.refine'_3.intro.intro
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
w✝¹ : x ∈ ⨆ (i : ι), S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ h, C (x * y) h
case this.refine'_3
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
⊢ (fun x => ∃ h, C x h) x → (fun x => ∃ h, C x h) y → (fun x => ∃ h, C x h) (x * y)
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
no goals
case this.refine'_3.intro.intro
α : Type ?u.12999
G : Type u_2
A : Type ?u.13005
S✝ : Type ?u.13008
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : (x : G) → (x ∈ ⨆ (i : ι), S i) → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (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✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
w✝¹ : x ∈ ⨆ (i : ι), S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ h, C (x * y) h
refine' ⟨_, hmul _ _ _ _ Cx Cy⟩