M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
rw [iSup_eq_closure] at hx
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
refine closure_induction hx (fun x hx => ?_) h1 hmul
case intro
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
no goals
case intro
M : Type u_2
A : Type ?u.46357
B : Type ?u.46360
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
exact hp _ _ hi