awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
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 : SemilatticeInf β
min : Min α := e.min
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 : SemilatticeInf β
min : Min α := e.min
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ Lattice α

Tactic:
apply e.injective.lattice

Premises used: Equiv.injective, Function.Injective.lattice
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ DistribLattice α

Tactic:
apply e.injective.distribLattice

Premises used: Function.Injective.distribLattice, Equiv.injective
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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 : DistribLattice β
lattice : Lattice α := e.lattice
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
inst : LinearOrder α
p : α → α → Prop
hp : Symmetric p
⊢ Pairwise p ↔ ∀ ⦃a b : α⦄, a < b → p a b

Tactic:
simpa [Pairwise, ← lt_or_lt_iff_ne, or_imp, forall_and] using fun h a b hab ↦ hp <| h _ _ hab

Premises used: or_imp, Pairwise, lt_or_lt_iff_ne, forall_and
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
p : α → α → Prop
hp : Symmetric p
⊢ Pairwise p ↔ ∀ ⦃a b : α⦄, b < a → p a b

Tactic:
simpa [Pairwise, ← lt_or_lt_iff_ne, or_imp, forall_and] using fun h a b hab ↦ hp <| h _ _ hab

Premises used: or_imp, Pairwise, lt_or_lt_iff_ne, forall_and
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
x y : (↑(Ico a b) : Type u_1)
⊢ (↑(x ⊓ y) : α) = (↑x : α) ⊓ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
inst_1 : Fact (a < b)
⊢ (↑⊥ : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
inst_1 : Fact (a < b)
x y : (↑(Ico a b) : Type u_1)
⊢ Disjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Premises used: disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeInf α
a : α
x y : (↑(Iio a) : Type u_1)
⊢ (↑(x ⊓ y) : α) = (↑x : α) ⊓ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
x y : (↑(Ioc a b) : Type u_1)
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
inst_1 : Fact (a < b)
⊢ (↑⊤ : α) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
inst_1 : Fact (a < b)
x y : (↑(Ioc a b) : Type u_1)
⊢ Codisjoint x y ↔ (↑x : α) ⊔ (↑y : α) = b

Tactic:
simp [_root_.codisjoint_iff, Subtype.ext_iff]

Premises used: codisjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeSup α
a : α
x y : (↑(Ioi a) : Type u_1)
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : SemilatticeInf α
x y : (↑(Iic a) : Type u_1)
⊢ (↑(x ⊓ y) : α) = (↑x : α) ⊓ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : SemilatticeSup α
x y : (↑(Iic a) : Type u_1)
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑⊤ : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : Preorder α
x : (↑(Iic a) : Type u_1)
⊢ x = ⊤ ↔ (↑x : α) = a

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
a : α
⊢ Eq.{u_1 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : SemilatticeInf α
inst_1 : OrderBot α
x y : (↑(Iic a) : Type u_1)
⊢ Disjoint x y ↔ Disjoint (↑x : α) (↑y : α)

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Premises used: disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : SemilatticeSup α
x y : (↑(Iic a) : Type u_1)
⊢ Codisjoint x y ↔ (↑x : α) ⊔ (↑y : α) = a

Tactic:
simpa only [_root_.codisjoint_iff] using Iic.eq_top_iff

Premises used: codisjoint_iff, Set.Iic.eq_top_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : Lattice α
inst_1 : OrderBot α
x y : (↑(Iic a) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
rw₁ : Disjoint (↑x : α) (↑y : α) ∧ Codisjoint x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
rw₂ rw₃ : Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
⊢ IsCompl x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a

Tactic:
rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]

Premises used: isCompl_iff, Set.Iic.disjoint_iff, Set.Iic.codisjoint_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a : α
inst : Lattice α
inst_1 : OrderBot α
simp_rw :
  (∀ (a_1 : (↑(Iic a) : Type u_1)), ∃ (b : (↑(Iic a) : Type u_1)), IsCompl a_1 b) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
simp_rw₁ :
  (∀ (a_1 : (↑(Iic a) : Type u_1)),
      ∃ (b : (↑(Iic a) : Type u_1)), Disjoint (↑a_1 : α) (↑b : α) ∧ (↑a_1 : α) ⊔ (↑b : α) = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
simp_rw₂ :
  (∀ (a_1 : α) (b : a_1 ∈ Iic a), ∃ (b : (↑(Iic a) : Type u_1)), Disjoint a_1 (↑b : α) ∧ a_1 ⊔ (↑b : α) = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
simp_rw₃ :
  (∀ (a_1 : α) (b : a_1 ∈ Iic a), ∃ (a_2 : α) (_ : a_2 ∈ Iic a), Disjoint a_1 a_2 ∧ a_1 ⊔ a_2 = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
simp_rw₄ :
  (∀ (a_1 : α) (b : a_1 ∈ Iic a), ∃ (a_2 : α) (_ : a_2 ∈ Iic a), a_1 ⊓ a_2 = ⊥ ∧ a_1 ⊔ a_2 = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
simp_rw₅ :
  (∀ (a_1 : α) (b : a_1 ∈ Iic a), ∃ a_2 ∈ Iic a, a_1 ⊓ a_2 = ⊥ ∧ a_1 ⊔ a_2 = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]

Premises used: complementedLattice_iff, disjoint_iff, Subtype.exists, Subtype.forall, exists_prop, Set.mem_Iic, Set.Iic.isCompl_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeInf α
a : α
x y : (↑(Ici a) : Type u_1)
⊢ (↑(x ⊓ y) : α) = (↑x : α) ⊓ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeSup α
a : α
x y : (↑(Ici a) : Type u_1)
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑⊥ : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ Eq.{u_1 + 1} (α := α) (↑⊤ : α) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeInf α
a : α
x y : (↑(Ici a) : Type u_1)
⊢ Disjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Premises used: disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderTop α
a : α
x y : (↑(Ici a) : Type u_1)
⊢ Codisjoint x y ↔ Codisjoint (↑x : α) (↑y : α)

Tactic:
simp [_root_.codisjoint_iff, Subtype.ext_iff]

Premises used: codisjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderTop α
a : α
x y : (↑(Ici a) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
rw₂ rw₃ :
  (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α) ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)

Tactic:
rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]

Premises used: isCompl_iff, Set.Ici.disjoint_iff, Set.Ici.codisjoint_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a b : α
inst : SemilatticeInf α
x y : (↑(Icc a b) : Type u_1)
⊢ (↑(x ⊓ y) : α) = (↑x : α) ⊓ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a b : α
inst : SemilatticeSup α
x y : (↑(Icc a b) : Type u_1)
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : Fact (a ≤ b)
⊢ (↑⊥ : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : Fact (a ≤ b)
⊢ (↑⊤ : α) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a b : α
inst : SemilatticeInf α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
⊢ Disjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Premises used: disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a b : α
inst : SemilatticeSup α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
⊢ Codisjoint x y ↔ (↑x : α) ⊔ (↑y : α) = b

Tactic:
simp [_root_.codisjoint_iff, Subtype.ext_iff]

Premises used: codisjoint_iff, Subtype.ext_iff
-- Module: Mathlib.Order.LatticeIntervals
Goal:
α : Type u_1
a b : α
inst : Lattice α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
rw₂ rw₃ : (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b

Tactic:
rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]

Premises used: Set.Icc.disjoint_iff, Set.Icc.codisjoint_iff, isCompl_iff
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Lex α ≃ α) (Equiv.symm toLex) ofLex

Tactic:
rfl

Premises used: Lex, Equiv.symm, ofLex, Equiv.refl, rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ Lex α) (Equiv.symm ofLex) toLex

Tactic:
rfl

Premises used: Lex, Equiv.symm, Equiv.refl, rfl, toLex
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a : Lex α
⊢ (toLex : (a : α) → Lex α) ((ofLex : (a : Lex α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a : α
⊢ (ofLex : (a : Lex α) → α) ((toLex : (a : α) → Lex α) a : Lex α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ((toLex : (a : α) → Lex α) b : Lex α) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a b : Lex α
⊢ Eq (α := α) ((ofLex : (a : Lex α) → α) a : α) ((ofLex : (a : Lex α) → α) b : α) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
inst : BEq α
h : LawfulBEq α
⊢ LawfulBEq.{u_2} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
h : Nonempty α
⊢ Nonempty.{u_2 + 1} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
h : Nontrivial α
⊢ Nontrivial.{u_2} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
p : Lex α → Prop
⊢ (∀ (a : Lex α), p a) ↔ ∀ (a : α), p ((toLex : (a : α) → Lex α) a)

Tactic:
Iff.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
p : Lex α → Prop
⊢ (∃ (a : Lex α), p a) ↔ ∃ (a : α), p ((toLex : (a : α) → Lex α) a)

Tactic:
Iff.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Colex α ≃ α) (Equiv.symm toColex) ofColex

Tactic:
rfl

Premises used: Colex, ofColex, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ Colex α) (Equiv.symm ofColex) toColex

Tactic:
rfl

Premises used: Colex, toColex, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a : Colex α
⊢ (toColex : (a : α) → Colex α) ((ofColex : (a : Colex α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a : α
⊢ (ofColex : (a : Colex α) → α) ((toColex : (a : α) → Colex α) a : Colex α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) ((toColex : (a : α) → Colex α) b : Colex α) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
a b : Colex α
⊢ Eq (α := α) ((ofColex : (a : Colex α) → α) a : α) ((ofColex : (a : Colex α) → α) b : α) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
inst : BEq α
h : LawfulBEq α
⊢ LawfulBEq.{u_2} (Colex α)

Tactic:
h

Premises used: Colex
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
h : Nonempty α
⊢ Nonempty.{u_2 + 1} (Colex α)

Tactic:
h

Premises used: Colex
-- Module: Mathlib.Order.Lex
Goal:
α_1 : Type u_1
α : Type u_2
h : Nontrivial α
⊢ Nontrivial.{u_2} (Colex α)

Tactic:
h

Premises used: Colex
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
p : Colex α → Prop
⊢ (∀ (a : Colex α), p a) ↔ ∀ (a : α), p ((toColex : (a : α) → Colex α) a)

Tactic:
Iff.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Order.Lex
Goal:
α : Type u_1
p : Colex α → Prop
⊢ (∃ (a : Colex α), p a) ↔ ∃ (a : α), p ((toColex : (a : α) → Colex α) a)

Tactic:
Iff.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ limsup u f = sInf {a : α | ∀ᶠ (n : β) in f, u n ≤ a}

Tactic:
rfl

Premises used: Filter.limsSup, Set.Mem, Filter.Eventually, setOf, Filter.limsup, Set.preimage, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ liminf u f = sSup {a : α | ∀ᶠ (n : β) in f, a ≤ u n}

Tactic:
rfl

Premises used: Filter.limsInf, Filter.liminf, Set.Mem, Filter.Eventually, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}

Tactic:
rfl

Premises used: Filter.blimsup, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ bliminf u f p = sSup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}

Tactic:
rfl

Premises used: Filter.bliminf, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
u : β → α
v : γ → β
f : Filter γ
⊢ liminf (u ∘ v) f = liminf u (map v f)

Tactic:
rfl

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
u : β → α
v : γ → β
f : Filter γ
⊢ limsup (u ∘ v) f = limsup u (map v f)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Filter.limsup, Set.preimage, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun (x : β) ↦ True) = limsup u f

Tactic:
simp [blimsup_eq, limsup_eq]

Premises used: Filter.blimsup_eq, Filter.limsup_eq