α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
⊢ ∀ (c : α), (∀ (b : α), b ∈ t → c ≤ b) → ∀ (b : α), b ∈ s → c ≤ b
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
⊢ ∀ (c : α), c ≤ sInf t → c ≤ sInf s
simp only [le_sInf_iff]
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
⊢ c ≤ b
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
⊢ ∀ (c : α), (∀ (b : α), b ∈ t → c ≤ b) → ∀ (b : α), b ∈ s → c ≤ b
introv h₀ h₁
case intro.intro
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
y : α
hy : y ∈ t
hy' : y ≤ b
⊢ c ≤ b
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
⊢ c ≤ b
rcases h _ h₁ with ⟨y, hy, hy'⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.39374
β₂ : Type ?u.39377
γ : Type ?u.39380
ι : Sort ?u.39383
ι' : Sort ?u.39386
κ : ι → Sort ?u.39391
κ' : ι' → Sort ?u.39396
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
y : α
hy : y ∈ t
hy' : y ≤ b
⊢ c ≤ b
solve_by_elim [le_trans _ hy']