Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ a ≤ bᶜ ⊔ c
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c → a ≤ bᶜ ⊔ c

case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜ ⊔ c → a ⊓ b ≤ c

State before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c → a ≤ bᶜ ⊔ c
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
⊢ a ≤ bᶜ ⊔ c

State before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
have : bᶜ ⊔ (a ⊓ b) ≤ bᶜ ⊔ c := sup_le_sup_left h bᶜ
State after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : bᶜ ⊔ a ⊓ b ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c

State before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : bᶜ ⊔ a ⊓ b ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
replace := le_trans le_sup_inf this
State after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c

State before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
simp only [compl_sup_eq_top, ge_iff_le, le_top, inf_of_le_left, sup_le_iff, le_sup_left,
  true_and] at this
State after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : a ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c

State before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : a ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
exact this
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜ ⊔ c → a ⊓ b ≤ c
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ bᶜ ⊔ c
⊢ a ⊓ b ≤ c

State before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ bᶜ ⊔ c
⊢ a ⊓ b ≤ c
Tactic:
rw [sup_comm] at h
State after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
⊢ a ⊓ b ≤ c

State before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
⊢ a ⊓ b ≤ c
Tactic:
have : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b := inf_le_inf_right b h
State after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c

State before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c
Tactic:
simp [inf_sup_right] at this
State after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ c
⊢ a ⊓ b ≤ c

State before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
exact this
State after:
no goals