awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ ⊤) ⊤
Tactic: rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ ⊤) ⊤
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
Tactic: rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ ⊤) ⊤
Tactic: rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ ⊤) ⊤
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
Tactic: rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : Preorder δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
f g : BoundedOrderHom α β
h : Eq (α := (a : α) → β) ((fun (f : BoundedOrderHom α β) ↦ f.toFun) f) ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (monotone' : Monotone toFun)
  (map_top' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊤ = ⊤)
  (map_bot' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
        { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
      ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)),
  { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : Preorder δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
g : BoundedOrderHom α β
toFun : α → β
monotone' : Monotone toFun
map_top' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } = g
have obtain : ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
  (map_top'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊤ = ⊤)
  (map_bot'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
        { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
      ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
        { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 })),
  { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } =
    { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : BotHomClass F α β
inst_6 : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β) (⊥ : β)
Tactic: rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : BotHomClass F α β
inst_6 : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β) (⊥ : β)
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) (⊥ : β)
Tactic: rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : BotHomClass F α β
inst_6 : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) (⊥ : β)
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : BotHomClass F α β
inst_6 : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) (⊥ : β)
rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ⊥ ⊥
Tactic: rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β)
  ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β)
    ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
  ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
Tactic: rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
  ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
Tactic: rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) ⊔ (f : (a : α) → β) (b \ a) : β)
  ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
Tactic: rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) ⊔ (f : (a : α) → β) (b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) (b \ a) : β)
  ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
Tactic: rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) ⊔ (f : (a : α) → β) (b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) (b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have rw₄ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
  ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
Tactic: rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : Max β
inst_4 : Bot β
inst_5 : Max γ
inst_6 : Bot γ
inst_7 : Max δ
inst_8 : Bot δ
f g : SupBotHom α β
h : Eq (α := (a : α) → β) ((fun (f : SupBotHom α β) ↦ f.toFun) f) ((fun (f : SupBotHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
  (map_bot' : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
      ((fun (f : SupBotHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : Max β
inst_4 : Bot β
inst_5 : Max γ
inst_6 : Bot γ
inst_7 : Max δ
inst_8 : Bot δ
g : SupBotHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_bot' : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
    ((fun (f : SupBotHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } = g
have obtain : ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
  (map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
      ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 })),
  { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.BoundedLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]