awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
inst : SemilatticeSup α
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
⊢ f x ⊔ f y = f y
have rw : f (x ⊔ y) = f y
Tactic: rw [← h _ hx _ hy, sup_eq_right.2 hxy]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
inst : SemilatticeSup α
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 y
⊢ f x ⊔ f y = f y
have rw₁ : f y = f y
Tactic: rw [← h _ hx _ hy, sup_eq_right.2 hxy]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (max x y) = f x ⊔ f y
have inl : x ≤ y → f (max x y) = f x ⊔ f y
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
inl : x ≤ y → f (max x y) = f x ⊔ f y
⊢ f (max x y) = f x ⊔ f y
have inr : y ≤ x → f (max x y) = f x ⊔ f y
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ f (max x y) = f x ⊔ f y
have inl : ∀ (this : f x ≤ f y), f (max x y) = f x ⊔ f y
Tactic: have := hf ?_ ?_ ‹_›
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ f (max x y) = f x ⊔ f y
have inr : ∀ (this : f y ≤ f x), f (max x y) = f x ⊔ f y
Tactic: have := hf ?_ ?_ ‹_›
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f x ⊔ f y = f x
have rw : f (x ⊓ y) = f x
Tactic: rw [← h _ hx _ hy, inf_eq_left.2 hxy]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f x ⊔ f y = f x
have rw₁ : f x = f x
Tactic: rw [← h _ hx _ hy, inf_eq_left.2 hxy]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f (max x y) = f x ⊓ f y
have inl : x ≤ y → f (max x y) = f x ⊓ f y
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f (max x y) = f x ⊓ f y
have inr : y ≤ x → f (max x y) = f x ⊓ f y
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f (max x y) = f x ⊓ f y
have inl : ∀ (this : f y ≤ f x), f (max x y) = f x ⊓ f y
Tactic: have := hf ?_ ?_ ‹_›
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ f (max x y) = f x ⊓ f y
have inr : ∀ (this : f x ≤ f y), f (max x y) = f x ⊓ f y
Tactic: have := hf ?_ ?_ ‹_›
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ a ≤ a ⊔ b
have rw : f a ≤ f a ⊔ f b
Tactic: rw [← le, map_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ b ≤ a ⊔ b
have rw : f b ≤ f a ⊔ f b
Tactic: rw [← le, map_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ a ⊔ b ≤ c
have rw : ∀ (ha : f a ≤ f c) (hb : f b ≤ f c), f (a ⊔ b) ≤ f c
Tactic: rw [← le] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 ⊔ b) ≤ f c
have rw : f a ⊔ f b ≤ f c
Tactic: rw [map_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw : (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c
Tactic: rw [← le, map_inf, map_sup, map_sup, map_sup, map_inf]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Preorder β
le : LE α := e.le
lt : LT α := e.lt
⊢ Preorder α
have le₁ : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply Function.Injective.preorder e
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ Preorder α
have lt₁ : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply Function.Injective.preorder e
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : PartialOrder β
preorder : Preorder α := e.preorder
⊢ PartialOrder α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.partialOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ PartialOrder α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.partialOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ LinearOrder α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.linearOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ LinearOrder α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.linearOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ LinearOrder α
have min₁ : ∀ (x y : α),
  Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊓ y) : β) (Min.min ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)
Tactic: apply e.injective.linearOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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) : β)
⊢ LinearOrder α
have max₁ : ∀ (x y : α),
  Eq.{v + 1} (α := β) ((e : (a : α) → β) (x ⊔ y) : β) (Max.max ((e : (a : α) → β) x) ((e : (a : α) → β) y) : β)
Tactic: apply e.injective.linearOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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) : β)
⊢ LinearOrder α
have compare₁ : ∀ (x y : α), Ord.compare.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) = Ord.compare x y
Tactic: apply e.injective.linearOrder
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeSup α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.semilatticeSup
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ SemilatticeSup α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.semilatticeSup
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ SemilatticeSup α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.semilatticeSup
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeInf α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y ≤ x
Tactic: apply e.injective.semilatticeInf
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ SemilatticeInf α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) y : β) ((e : (a : α) → β) x : β) ↔ y < x
Tactic: apply e.injective.semilatticeInf
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ SemilatticeInf α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.semilatticeInf
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
⊢ Lattice α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.lattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ Lattice α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.lattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ Lattice α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.lattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : β)
⊢ Lattice α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.lattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : DistribLattice β
lattice : Lattice α := e.lattice
⊢ DistribLattice α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.distribLattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ DistribLattice α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.distribLattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ DistribLattice α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.distribLattice
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : β)
⊢ DistribLattice α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.distribLattice
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
a : α
inst : Lattice α
inst_1 : OrderBot α
x y : (↑(Iic a) : Type u_1)
⊢ IsCompl x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
have rw : Disjoint x y ∧ Codisjoint x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
Tactic: rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ IsCompl x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
have rw₁ : Disjoint (↑x : α) (↑y : α) ∧ Codisjoint x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
Tactic: rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ IsCompl x y ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
have rw₂ : Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a ↔ Disjoint (↑x : α) (↑y : α) ∧ (↑x : α) ⊔ (↑y : α) = a
Tactic: rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
a : α
inst : Lattice α
inst_1 : OrderBot α
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
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
⊢ ComplementedLattice.{u_1} (↑(Iic a) : Type u_1) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
have 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
Tactic: simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]