awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r (b ⊓ c) d

Tactic:
simpa [sup_eq_right.mpr (le_inf hab hac), sup_eq_left.mpr (inf_le_of_left_le hbd)] using
    ((h₄ (le_trans hab hbd) had).2 : r (a ⊔ b ⊓ c) (d ⊔ b ⊓ c))

Premises used: Iff.mpr, inf_le_of_left_le, sup_eq_left, le_inf, And.right, sup_eq_right, le_trans
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ x

Tactic:
simp [inf_assoc, inf_le_left]

Premises used: inf_le_left, inf_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ≤ x ⊔ y ⊔ z

Tactic:
simp [sup_assoc, le_sup_left]

Premises used: le_sup_left, sup_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊔ z

Tactic:
simpa [inf_assoc] using inf_le_of_right_le inf_le_sup

Premises used: inf_le_of_right_le, inf_le_sup, inf_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ y ⊔ z ≤ x ⊔ y ⊔ z

Tactic:
simp [sup_assoc, le_sup_right]

Premises used: le_sup_right, sup_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊓ z

Tactic:
simpa [inf_assoc] using inf_le_right (b := y ⊓ z)

Premises used: inf_le_right, inf_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
rw : r (y ⊓ (x ⊓ z)) (y ⊓ z)
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)

Tactic:
rw [inf_comm x, inf_assoc]

Premises used: inf_comm, inf_assoc
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (y ⊓ (x ⊓ z)) (y ⊓ z)

Tactic:
simpa [inf_comm x, ← inf_inf_distrib_left] using this

Premises used: inf_inf_distrib_left, inf_comm
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
suffices : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)

Tactic:
suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))

Tactic:
(h₄ inf_le_sup (h₂.mp hxy)).1

Premises used: inf_le_sup, And.left, Iff.mp
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))

Tactic:
exact (h₄ inf_le_sup (h₂.mp hxy)).1

Premises used: inf_le_sup, And.left, Iff.mp
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (y ⊔ z) (x ⊔ y ⊔ z)

Tactic:
simpa [sup_comm y x, sup_sup_distrib_left y x z, sup_assoc] using
          ((h₄ inf_le_sup (h₂.mp hxy)).2 : r (x ⊓ y ⊔ (y ⊔ z)) (x ⊔ y ⊔ (y ⊔ z)))

Premises used: inf_le_sup, sup_assoc, sup_sup_distrib_left, sup_comm, And.right, Iff.mp
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r x z

Tactic:
exact closed_interval h₂ h₄ (x ⊓ y ⊓ z) _ _ (x ⊔ y ⊔ z) (by simp [inf_assoc, inf_le_left])
    (by simp [sup_assoc, le_sup_left]) inf_le_right le_sup_right
    (h₃ (by simpa [inf_assoc] using inf_le_of_right_le inf_le_sup)
    (by simp [sup_assoc, le_sup_right]) (h₃
    (by simpa [inf_assoc] using inf_le_right (b := y ⊓ z)) inf_le_sup (by
      suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this
      exact (h₄ inf_le_sup (h₂.mp hxy)).1) (h₂.mp hyz)) (by
        simpa [sup_comm y x, sup_sup_distrib_left y x z, sup_assoc] using
          ((h₄ inf_le_sup (h₂.mp hxy)).2 : r (x ⊓ y ⊔ (y ⊔ z)) (x ⊔ y ⊔ (y ⊔ z)))))

Premises used: inf_le_right, inf_le_sup, le_sup_right, Max.max, Iff.mp, _private.0.LatticeCon.closed_interval, Min.min
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y : α
h : r x y
⊢ r y x

Tactic:
simpa [h₂, inf_comm, sup_comm, ← h₂] using h

Premises used: inf_comm, sup_comm
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w : α
_ : ∀ {x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)
⊢ ∀ {x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
_
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y : α
_ : ∀ {z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)
⊢ ∀ {z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
_
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
have : ∀ (compatible_left_inf : ∀ {x y t : α} (hh : r x y), r (x ⊓ t) (y ⊓ t)), r (w ⊓ y) (x ⊓ z)
⊢ r (w ⊓ y) (x ⊓ z)

Tactic:
have compatible_left_inf {x y t : α} (hh : r x y) : r (x ⊓ t) (y ⊓ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊓ t) _ _ ((x ⊔ y) ⊓ t)
            (inf_le_inf_right _ inf_le_left) (inf_le_inf_right _ le_sup_left)
            (inf_le_inf_right _ inf_le_right) (inf_le_inf_right _ le_sup_right)
            (h₄ inf_le_sup (h₂.mp hh)).1
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
compatible_left_inf : ∀ {x y t : α} (hh : r x y), r (x ⊓ t) (y ⊓ t)
⊢ r (w ⊓ y) (w ⊓ z)

Tactic:
simpa [inf_comm w] using compatible_left_inf h2

Premises used: inf_comm
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
compatible_left_inf : ∀ {x y t : α} (hh : r x y), r (x ⊓ t) (y ⊓ t)
⊢ r (w ⊓ y) (x ⊓ z)

Tactic:
exact transitive h₂ h₃ h₄ (by
          simpa [inf_comm w] using compatible_left_inf h2) (compatible_left_inf h1)

Premises used: _private.0.LatticeCon.transitive
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w : α
_ : ∀ {x y z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)
⊢ ∀ {x y z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)

Tactic:
_
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y : α
_ : ∀ {z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)
⊢ ∀ {z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)

Tactic:
_
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
have : ∀ (compatible_left_sup : ∀ {x y t : α} (hh : r x y), r (x ⊔ t) (y ⊔ t)), r (w ⊔ y) (x ⊔ z)
⊢ r (w ⊔ y) (x ⊔ z)

Tactic:
have compatible_left_sup {x y t : α} (hh : r x y) : r (x ⊔ t) (y ⊔ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊔ t) _ _ ((x ⊔ y) ⊔ t)
        (sup_le_sup_right inf_le_left _) (sup_le_sup_right le_sup_left _)
        (sup_le_sup_right inf_le_right _) (sup_le_sup_right le_sup_right _)
        (h₄ inf_le_sup (h₂.mp hh)).2
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
compatible_left_sup : ∀ {x y t : α} (hh : r x y), r (x ⊔ t) (y ⊔ t)
⊢ r (w ⊔ y) (w ⊔ z)

Tactic:
simpa [sup_comm w] using compatible_left_sup h2

Premises used: sup_comm
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
compatible_left_sup : ∀ {x y t : α} (hh : r x y), r (x ⊔ t) (y ⊔ t)
⊢ r (w ⊔ y) (x ⊔ z)

Tactic:
exact transitive h₂ h₃ h₄ (by
      simpa [sup_comm w] using compatible_left_sup h2)
      (compatible_left_sup h1)

Premises used: _private.0.LatticeCon.transitive
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : LatticeHomClass F α β
f : F
w x y z : α
h : (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) w x
h_1 : (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) y z
⊢ (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) (w ⊓ y) (x ⊓ z)

Tactic:
simp_all +instances only [Setoid.ker, onFun, map_inf]

Premises used: Function.onFun, Setoid.ker, InfHomClass.map_inf
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : LatticeHomClass F α β
f : F
w x y z : α
h : (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) w x
h_1 : (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) y z
⊢ (Setoid.ker (⇑f : (a : α) → β) : α → α → Prop) (w ⊔ y) (x ⊔ z)

Tactic:
simp_all +instances only [Setoid.ker, onFun, map_sup]

Premises used: Function.onFun, Setoid.ker, SupHomClass.map_sup
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
rw : a ⊔ (b ⊔ c) = b ⊔ c
rw₁ : a ⊔ b ⊔ c = b ⊔ c
rw₂ rw₃ : b ⊔ c = b ⊔ c
⊢ a ⊔ c = c

Tactic:
rw [← hbc, ← sup_assoc, hab]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ⊔ b = b
hba : b ⊔ a = a
rwa : b ⊔ a = b
rwa₁ rwa₂ rwa₃ rwa₄ : a ⊔ b = b
⊢ a = b

Tactic:
rwa [← hba, sup_comm]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
rw : a ⊔ a ⊔ b = a ⊔ b
rw₁ rw₂ : a ⊔ b = a ⊔ b
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
rw [← sup_assoc, sup_idem]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
rw : a ⊔ b ⊔ b = a ⊔ b
rw₁ : a ⊔ (b ⊔ b) = a ⊔ b
rw₂ rw₃ : a ⊔ b = a ⊔ b
⊢ b ⊔ (a ⊔ b) = a ⊔ b

Tactic:
rw [sup_comm, sup_assoc, sup_idem]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
rwa : a ⊔ (b ⊔ c) = c
rwa₁ rwa₂ rwa₃ rwa₄ : a ⊔ c = c
⊢ a ⊔ b ⊔ c = c

Tactic:
rwa [sup_assoc, hbc]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
rw : a ⊓ (b ⊓ c) = b ⊓ c
rw₁ : a ⊓ b ⊓ c = b ⊓ c
rw₂ rw₃ : b ⊓ c = b ⊓ c
⊢ a ⊓ c = c

Tactic:
rw [← hbc, ← inf_assoc, hab]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
hba : b ⊓ a = a
hab : a ⊓ b = b
rwa : b ⊓ a = b
rwa₁ rwa₂ rwa₃ rwa₄ : a ⊓ b = b
⊢ a = b

Tactic:
rwa [← hba, inf_comm]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
rw : a ⊓ a ⊓ b = a ⊓ b
rw₁ rw₂ : a ⊓ b = a ⊓ b
⊢ a ⊓ (a ⊓ b) = a ⊓ b

Tactic:
rw [← inf_assoc, inf_idem]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
rw : a ⊓ b ⊓ b = a ⊓ b
rw₁ : a ⊓ (b ⊓ b) = a ⊓ b
rw₂ rw₃ : a ⊓ b = a ⊓ b
⊢ b ⊓ (a ⊓ b) = a ⊓ b

Tactic:
rw [inf_comm, inf_assoc, inf_idem]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b c : α
hac : b ⊓ a = a
hbc : c ⊓ a = a
rwa : b ⊓ (c ⊓ a) = a
rwa₁ rwa₂ rwa₃ rwa₄ : b ⊓ a = a
⊢ b ⊓ c ⊓ a = a

Tactic:
rwa [inf_assoc, hbc]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ≤ a ⊔ b

Tactic:
SemilatticeSup.le_sup_left a b

Premises used: SemilatticeSup.le_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ b ≤ a ⊔ b

Tactic:
SemilatticeSup.le_sup_right a b

Premises used: SemilatticeSup.le_sup_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
SemilatticeSup.sup_le a b c

Premises used: SemilatticeSup.sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
h : c ≤ a
⊢ c ≤ a ⊔ b

Tactic:
le_trans h le_sup_left

Premises used: le_sup_left, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
h : c ≤ b
⊢ c ≤ a ⊔ b

Tactic:
le_trans h le_sup_right

Premises used: le_sup_right, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
h : c < a
⊢ c < a ⊔ b

Tactic:
h.trans_le le_sup_left

Premises used: le_sup_left, LT.lt.trans_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
h : c < b
⊢ c < a ⊔ b

Tactic:
h.trans_le le_sup_right

Premises used: le_sup_right, LT.lt.trans_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c

Tactic:
⟨fun h : a ⊔ b ≤ c => ⟨le_trans le_sup_left h, le_trans le_sup_right h⟩,
   fun ⟨h₁, h₂⟩ => sup_le h₁ h₂⟩

Premises used: le_sup_left, le_sup_right, LE.le, _private.0.sup_le_iff.match_1, Max.max, And.intro, Iff.intro, sup_le, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ a ∧ a ≤ a ⊔ b ↔ b ≤ a

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ∧ b ≤ a ⊔ b ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a = a ⊔ b ↔ b ≤ a

Tactic:
eq_comm.trans sup_eq_left

Premises used: sup_eq_left, eq_comm, Iff.trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ b = a ⊔ b ↔ a ≤ b

Tactic:
eq_comm.trans sup_eq_right

Premises used: eq_comm, sup_eq_right, Iff.trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a < a ⊔ b ↔ ¬b ≤ a

Tactic:
le_sup_left.lt_iff_ne.trans <| not_congr left_eq_sup

Premises used: le_sup_left, LE.le.lt_iff_ne, Iff.trans, left_eq_sup, not_congr
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ b < a ⊔ b ↔ ¬a ≤ b

Tactic:
le_sup_right.lt_iff_ne.trans <| not_congr right_eq_sup

Premises used: right_eq_sup, le_sup_right, LE.le.lt_iff_ne, Iff.trans, not_congr
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
h : a ≠ b
⊢ a < a ⊔ b ∨ b < a ⊔ b

Tactic:
h.not_le_or_not_ge.symm.imp left_lt_sup.2 right_lt_sup.2

Premises used: Iff.mpr, right_lt_sup, left_lt_sup, Ne.not_le_or_not_ge, Or.symm, Or.imp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
mp : a ≤ b → ∃ (c : α), b = a ⊔ c
mpr : (∃ (c : α), b = a ⊔ c) → a ≤ b
⊢ a ≤ b ↔ ∃ (c : α), b = a ⊔ c

Tactic:
constructor
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
h : a ≤ b
⊢ ∃ (c : α), b = a ⊔ c

Tactic:
⟨b, (sup_eq_right.mpr h).symm⟩

Premises used: Iff.mpr, sup_eq_right, Exists.intro, Eq.symm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
h : a ≤ b
⊢ ∃ (c : α), b = a ⊔ c

Tactic:
exact ⟨b, (sup_eq_right.mpr h).symm⟩
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a ⊔ c ≤ b ⊔ d

Tactic:
sup_le (le_sup_of_le_left h₁) (le_sup_of_le_right h₂)

Premises used: le_sup_of_le_left, le_sup_of_le_right, sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
h₁ : a ≤ b
c : α
⊢ c ⊔ a ≤ c ⊔ b

Tactic:
sup_le_sup le_rfl h₁

Premises used: sup_le_sup, le_rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
h₁ : a ≤ b
c : α
⊢ a ⊔ c ≤ b ⊔ c

Tactic:
sup_le_sup h₁ le_rfl

Premises used: sup_le_sup, le_rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a : α
⊢ a ⊔ a = a

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
a b c d : α
⊢ Std.IdempotentOp fun (x1 x2 : α) ↦ x1 ⊔ x2

Tactic:
⟨sup_idem⟩

Premises used: sup_idem, Std.IdempotentOp.mk
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
a₁ : a ⊔ b ≤ b ⊔ a
a₂ : b ⊔ a ≤ a ⊔ b
⊢ a ⊔ b = b ⊔ a

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ⊔ a

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ b ⊔ a ≤ a ⊔ b

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
a b c d : α
⊢ Std.Commutative fun (x1 x2 : α) ↦ x1 ⊔ x2

Tactic:
⟨sup_comm⟩

Premises used: sup_comm, Std.Commutative.mk
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c x : α
simp : (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x

Tactic:
simp only [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c x : α
rw rw₁ : a ≤ x ∧ b ≤ x ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x

Tactic:
rw [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
a b c d : α
⊢ Std.Associative fun (x1 x2 : α) ↦ x1 ⊔ x2

Tactic:
⟨sup_assoc⟩

Premises used: sup_assoc, Std.Associative.mk
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : c ⊔ (a ⊔ b) = c ⊔ b ⊔ a
rw₁ : c ⊔ (b ⊔ a) = c ⊔ b ⊔ a
rw₂ rw₃ : c ⊔ (b ⊔ a) = c ⊔ (b ⊔ a)
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a

Tactic:
rw [sup_comm, sup_comm a, sup_assoc]

Premises used: sup_assoc, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ b ⊔ b = a ⊔ b

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ b ⊔ c = b ⊔ (a ⊔ c)
rw₁ : a ⊔ b ⊔ c = b ⊔ a ⊔ c
rw₂ rw₃ : b ⊔ a ⊔ c = b ⊔ a ⊔ c
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Tactic:
rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]

Premises used: sup_assoc, sup_comm