Theorem: infi₂_le_iff (Sion/ForMathlib/Misc.lean)

State before:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ⨅ x ∈ s, f x ≤ b ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
rw [iInf_le_iff]
State after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ (∀ (b_1 : β), (∀ (i : α), b_1 ≤ ⨅ (_ : i ∈ s), f i) → b_1 ≤ b) ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b

State before:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ (∀ (b_1 : β), (∀ (i : α), b_1 ≤ ⨅ (_ : i ∈ s), f i) → b_1 ≤ b) ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
apply forall_congr'
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ∀ (a : β), (∀ (i : α), a ≤ ⨅ (_ : i ∈ s), f i) → a ≤ b ↔ (∀ x ∈ s, a ≤ f x) → a ≤ b

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ∀ (a : β), (∀ (i : α), a ≤ ⨅ (_ : i ∈ s), f i) → a ≤ b ↔ (∀ x ∈ s, a ≤ f x) → a ≤ b
Tactic:
intro b'
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b b' : β
⊢ (∀ (i : α), b' ≤ ⨅ (_ : i ∈ s), f i) → b' ≤ b ↔ (∀ x ∈ s, b' ≤ f x) → b' ≤ b

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b b' : β
⊢ (∀ (i : α), b' ≤ ⨅ (_ : i ∈ s), f i) → b' ≤ b ↔ (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
simp_rw [le_iInf_iff]
State after:
no goals