awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
⊢ CompletelyDistribLattice α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
⊢ CompletelyDistribLattice α
have map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompletelyDistribLattice α
have map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompletelyDistribLattice α
have map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ CompletelyDistribLattice α
have map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ CompletelyDistribLattice α
have map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ CompletelyDistribLattice α
have map_himp : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ CompletelyDistribLattice α
have map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
⊢ CompletelyDistribLattice α
have map_sdiff : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completelyDistribLattice
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
⊢ CompleteBooleanAlgebra α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ CompleteBooleanAlgebra α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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
⊢ CompleteBooleanAlgebra α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
⊢ CompleteBooleanAlgebra α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
⊢ CompleteBooleanAlgebra α
have map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteBooleanAlgebra α
have map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteBooleanAlgebra α
have map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ CompleteBooleanAlgebra α
have map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ CompleteBooleanAlgebra α
have map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ CompleteBooleanAlgebra α
have map_himp : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
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 : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ CompleteBooleanAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
⊢ CompleteAtomicBooleanAlgebra α
have le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ CompleteAtomicBooleanAlgebra α
have lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
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
⊢ CompleteAtomicBooleanAlgebra α
have map_sup : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
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 : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_inf : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra