awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : LinearOrder β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u, v} (β := β) (fun (x : α) ↦ max (f x) (g x)) s

Tactic:
hf.sup hg

Premises used: AntitoneOn.sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
inst : SemilatticeInf α
inst_1 : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
rw : f (x ⊓ y) = f x
rw₁ rw₂ : f x = f x
⊢ f x ⊔ f y = f x

Tactic:
rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Premises used: Iff.mpr, inf_eq_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
inl : x ≤ y → f (max x y) = f x ⊓ f y
inr : y ≤ x → f (max x y) = f x ⊓ f y
⊢ f (max x y) = f x ⊓ f y

Tactic:
cases le_total x y

Premises used: le_total
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
inl : ∀ (this : f y ≤ f x), f (max x y) = f x ⊓ f y
inl₁ : x ∈ s
inl₂ : y ∈ s
⊢ f (max x y) = f x ⊓ f y

Tactic:
have := hf ?_ ?_ ‹_›
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
inr : ∀ (this : f x ≤ f y), f (max x y) = f x ⊓ f y
inr₁ : y ∈ s
inr₂ : x ∈ s
⊢ f (max x y) = f x ⊓ f y

Tactic:
have := hf ?_ ?_ ‹_›
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ y ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ y ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Premises used: inf_of_le_left, inf_of_le_right, sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Max β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Max β
p q : α × β
⊢ (p ⊔ q).fst = p.fst ⊔ q.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Max β
p q : α × β
⊢ (p ⊔ q).snd = p.snd ⊔ q.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Max β
p q : α × β
⊢ (p ⊔ q).swap = p.swap ⊔ q.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Max β
p q : α × β
⊢ p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
P : α → Prop
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
x y : Subtype P
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
P : α → Prop
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
x y : α
hx : P x
hy : P y
⊢ mk (p := P) x hx ⊔ mk (p := P) y hy = mk (p := P) (x ⊔ y) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
rw : f a ≤ f a ⊔ f b
⊢ a ≤ a ⊔ b

Tactic:
rw [← le, map_sup]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f a ⊔ f b

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f a ⊔ f b

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
rw : f b ≤ f a ⊔ f b
⊢ b ≤ a ⊔ b

Tactic:
rw [← le, map_sup]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f b ≤ f a ⊔ f b

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f b ≤ f a ⊔ f b

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : a ≤ c
hb : b ≤ c
rw : ∀ (ha : f a ≤ f c) (hb : f b ≤ f c), f (a ⊔ b) ≤ f c
⊢ a ⊔ b ≤ c

Tactic:
rw [← le] at *
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
rw : f a ⊔ f b ≤ f c
⊢ f (a ⊔ b) ≤ f c

Tactic:
rw [map_sup]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f a ⊔ f b ≤ f c

Tactic:
sup_le ha hb

Premises used: sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : LE α
inst_2 : LT α
inst_3 : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f a ⊔ f b ≤ f c

Tactic:
exact sup_le ha hb

Premises used: sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
rw : (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
rw [← le, map_inf, map_sup, map_sup, map_sup, map_inf]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c

Tactic:
le_sup_inf

Premises used: le_sup_inf
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c

Tactic:
exact le_sup_inf

Premises used: le_sup_inf
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Preorder β
le : LE α := e.le
lt : LT α := e.lt
le₁ : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt₁ : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ Preorder α

Tactic:
apply Function.Injective.preorder e

Premises used: Function.Injective.preorder, DFunLike.coe
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : PartialOrder β
preorder : Preorder α := e.preorder
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ PartialOrder α

Tactic:
apply e.injective.partialOrder

Premises used: Equiv.injective, Function.Injective.partialOrder
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : PartialOrder β
preorder : Preorder α := e.preorder
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : PartialOrder β
preorder : Preorder α := e.preorder
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
min₁ :
  ∀ (x y : α),
    Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊓ y) : β) (Min.min ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)
max₁ :
  ∀ (x y : α),
    Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊔ y) : β) (Max.max ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)
compare₁ : ∀ (x y : α), Ord.compare.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) = Ord.compare x y
⊢ LinearOrder α

Tactic:
apply e.injective.linearOrder

Premises used: Equiv.injective, Function.Injective.linearOrder
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊓ y) : β) (Min.min ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊓ y) : β) (Min.min ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊓ y) : β) (Min.min ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊔ y) : β) (Max.max ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊔ y) : β) (Max.max ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊔ y) : β) (Max.max ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Ord.compare.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) = Ord.compare x y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : LinearOrder β
inst_1 : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x y : α
⊢ Ord.compare.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) = Ord.compare x y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ SemilatticeSup α

Tactic:
apply e.injective.semilatticeSup

Premises used: Function.Injective.semilatticeSup, Equiv.injective
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y ≤ x
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y < x
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ SemilatticeInf α

Tactic:
apply e.injective.semilatticeInf

Premises used: Function.Injective.semilatticeInf, Equiv.injective
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y ≤ x

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y ≤ x

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y < x

Tactic:
rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y < x

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply