Theorem: inf_le_inf_left' (FM2023Exrcise/section06_orderings_and_lattices/sheet2.lean)

State before:
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a ⊓ c
Tactic:
apply le_inf
State after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a

case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c

State before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a

case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
. apply inf_le_left
State after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c

State before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
. have h' : a ⊓ b ≤ b :=
    by
    apply inf_le_right
  apply le_trans h' h
State after:
no goals

State before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a
Tactic:
apply inf_le_left
State after:
no goals

State before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
have h' : a ⊓ b ≤ b :=
  by
  apply inf_le_right
State after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
h' : a ⊓ b ≤ b
⊢ a ⊓ b ≤ c

State before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
h' : a ⊓ b ≤ b
⊢ a ⊓ b ≤ c
Tactic:
apply le_trans h' h
State after:
no goals

State before:
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ b
Tactic:
apply inf_le_right
State after:
no goals