ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
rw [iSup_eq_closure] at hx₁
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ (i : ι), ↑(S i)
⊢ C x₂
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
refine' closure_induction hx₁ (fun x₂ hx₂ => _) hmul
case intro
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
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₂
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
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
ι : Sort u_2
M : Type u_1
A : Type ?u.9348
B : Type ?u.9351
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
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