awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : a ≤ c_1
hbc : b ≤ c_1
⊢ sup a b ≤ c_1

Tactic:
simp [eq_sup, hac, hbc]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
⊢ le (inf a b) a

Tactic:
simp [eq_le, eq_inf]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
⊢ le (inf a b) b

Tactic:
simp [eq_le, eq_inf]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a : α
_ : ∀ (b c : α), le a b → le a c → le a (inf b c)
⊢ ∀ (b c : α), le a b → le a c → le a (inf b c)

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
_ : ∀ (c : α), le a b → le a c → le a (inf b c)
⊢ ∀ (c : α), le a b → le a c → le a (inf b c)

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : le a b
hbc : le a c_1
simp_rw : ∀ (hac : a ≤ b) (hbc : a ≤ c_1), a ≤ inf b c_1
⊢ le a (inf b c_1)

Tactic:
simp_rw [eq_le] at hac hbc ⊢
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : a ≤ b
hbc : a ≤ c_1
⊢ a ≤ inf b c_1

Tactic:
simp [eq_inf, hac, hbc]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : DistribLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
simp +instances [eq_le, eq_sup, eq_inf, le_sup_inf]

Premises used: le_sup_inf
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
rw : ∀ (x y : α), x ≤ y ↔ le x y
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
fun _ _ ↦ .rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
exact fun _ _ ↦ .rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
x x_1 x_2 : α
⊢ x ≤ himp x_1 x_2 ↔ x ⊓ x_1 ≤ x_2

Tactic:
simp +instances [eq_le, eq_himp, eq_inf]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
rw : ∀ (x y : α), x ≤ y ↔ le x y
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
fun _ _ ↦ .rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
exact fun _ _ ↦ .rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (a b c_1 : α), sdiff a b ≤ c_1 ↔ a ≤ b ⊔ c_1

Tactic:
simp +instances [eq_le, eq_sdiff, eq_sup]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
rw : ∀ (x y : α), x ≤ y ↔ le x y
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
fun _ _ ↦ .rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
exact fun _ _ ↦ .rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (a : α), a ⇨ ⊥ = compl a

Tactic:
simp +instances [eq_le, eq_himp, eq_bot, eq_compl]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
rw : ∀ (x y : α), x ≤ y ↔ le x y
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
fun _ _ ↦ .rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
exact fun _ _ ↦ .rfl
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (a : α), ⊤ \ a = hnot a

Tactic:
simp +instances [eq_le, eq_sdiff, eq_top, eq_hnot]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
x : Set α
⊢ IsLUB x (sSup x)

Tactic:
simp +instances only [eq_le, eq_sSup, isLUB_sSup]

Premises used: CompleteLattice.isLUB_sSup
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
x : Set α
⊢ IsGLB x (sInf x)

Tactic:
simp +instances only [eq_le, eq_sInf, isGLB_sInf]

Premises used: CompleteLattice.isGLB_sInf
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a : α
⊢ a ≤ top

Tactic:
simp +instances [eq_le, eq_top]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a : α
⊢ bot ≤ a

Tactic:
simp +instances [eq_le, eq_bot]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
⊢ HImp α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
sSup : Set α → α
⊢ SupSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
infer_instance