[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
this : x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
[PROOFSTEP]
refine' fun hx => closure_induction hx (fun y hy => mem_iUnion.mp hy) _
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
[PROOFSTEP]
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
[GOAL]
case intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
rcases hS i j with ⟨k, hki, hkj⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subsemigroup M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directed_on hS]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
have : S ≤ S ⊔ T := le_sup_left
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
have : T ≤ S ⊔ T := le_sup_right
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
[PROOFSTEP]
have : S i ≤ iSup S := le_iSup _ _
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
have : s ≤ sSup S := le_sSup hs
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₁
[PROOFSTEP]
rw [iSup_eq_closure] at hx₁ 
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₁
[PROOFSTEP]
refine' closure_induction hx₁ (fun x₂ hx₂ => _) hmul
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₂
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
[GOAL]
case intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₂
[PROOFSTEP]
exact hp _ _ hi
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₁
[PROOFSTEP]
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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
[PROOFSTEP]
refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁ (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
[GOAL]
case refine_1
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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₂
[PROOFSTEP]
exact ⟨_, hp _ _ hx₂⟩
[GOAL]
case refine_2
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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)
[PROOFSTEP]
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
[GOAL]
case refine_2.intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
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''
[PROOFSTEP]
exact ⟨_, hmul _ _ _ _ Cx Cy⟩
