awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ GeneralizedCoheytingAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedCoheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ GeneralizedCoheytingAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedCoheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ GeneralizedCoheytingAlgebra α
have map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.generalizedCoheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ GeneralizedCoheytingAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedCoheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ HeytingAlgebra α
have le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ HeytingAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ HeytingAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ HeytingAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ HeytingAlgebra α
have map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ HeytingAlgebra α
have map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ HeytingAlgebra α
have map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ HeytingAlgebra α
have map_himp : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.heytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ CoheytingAlgebra α
have le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ CoheytingAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ CoheytingAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ CoheytingAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ CoheytingAlgebra α
have map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ CoheytingAlgebra α
have map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ CoheytingAlgebra α
have map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
⊢ CoheytingAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.coheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ BiheytingAlgebra α
have le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ BiheytingAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ BiheytingAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ BiheytingAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ BiheytingAlgebra α
have map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ BiheytingAlgebra α
have map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ BiheytingAlgebra α
have map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ BiheytingAlgebra α
have map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
⊢ BiheytingAlgebra α
have map_himp : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.biheytingAlgebra