awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
f g : BoundedLatticeHom α β
h :
  Eq (α := (a : α) → β) ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) f) ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
  (map_inf' :
    ∀ (a b : α),
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
          { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b)
  (map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤)
  (map_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
      ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
      BoundedLatticeHom α β } =
    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 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
g : BoundedLatticeHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_inf' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b
map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
      BoundedLatticeHom α β } =
    g
have obtain : ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
  (map_inf'_1 :
    ∀ (a b : α),
      { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun (a ⊓ b) =
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun a ⊓
          { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun b)
  (map_top'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊤ = ⊤)
  (map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊥ = ⊥)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
      ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
          map_bot' := map_bot'_1 })),
  { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
      BoundedLatticeHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_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.BoundedLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
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 : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
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 : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
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]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass 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} (α := β) (sSup (image (α := α) (⇑f : (a : α) → β) {a, b}) : β)
  ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
Tactic: rw [← sSup_pair, map_sSup]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sSup ∅) : β) (⊥ : β)
Tactic: rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sSup ∅) : β) (⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) (sSup (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) ∅)) ⊥
Tactic: rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sSup ∅) : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (sSup (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) ∅)) ⊥
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₂ : Eq.{u_3 + 1} (α := β) (sSup ∅) ⊥
Tactic: rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : sSupHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sSup ∅) : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (sSup (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) ∅)) ⊥
rw₂ : Eq.{u_3 + 1} (α := β) (sSup ∅) ⊥
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ⊥ ⊥
Tactic: rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
f g : sSupHom α β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → β) (map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s))
  (h : { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun = g.toFun),
  { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
g : sSupHom α β
toFun : α → β
map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)
h : { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun = g.toFun
⊢ { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = g
have mk : ∀ (toFun_1 : α → β) (map_sSup'_1 : ∀ (s : Set α), toFun_1 (sSup s) = sSup (toFun_1 '' s))
  (h :
    { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β }.toFun =
      { toFun := toFun_1, map_sSup' := map_sSup'_1 : sSupHom α β }.toFun),
  { toFun := toFun, map_sSup' := map_sSup' : sSupHom α β } = { toFun := toFun_1, map_sSup' := map_sSup'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
s : Set α
⊢ id (sSup s) = sSup (id '' s)
have rw : sSup s = sSup (id '' s)
Tactic: rw [id, Set.image_id]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
s : Set α
rw : sSup s = sSup (id '' s)
⊢ id (sSup s) = sSup (id '' s)
have rw₁ : sSup s = sSup s
Tactic: rw [id, Set.image_id]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
inst_2 : SupSet β
inst_3 : SupSet γ
inst_4 : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) (sSup s))
    (sSup (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) '' s))
have rw : Eq.{u_4 + 1} (α := γ) (sSup ((fun (x : α) ↦ (f : (a : β) → γ) ((g : (a : α) → β) x : β)) '' s))
  (sSup (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) '' s))
Tactic: rw [comp_apply, map_sSup, map_sSup, Set.image_image]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
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.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
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.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SupSet α
inst_1 : SupSet β
inst_2 : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
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]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
s : Set α
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
have inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
s : Set α
inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
have inr : ∀ (hs : s.Nonempty), Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))
have inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ∅)
Tactic: rw [Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
inl : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ∅)
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) (sSup ((fun (x_1 : α) ↦ ⊥) '' ∅))
have inl₁ : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup ∅)) ⊥
Tactic: rw [Set.image_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
have inr : Eq (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup {⊥})
Tactic: rw [hs.image_const, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : SupSet α
x : CompleteLattice β
s : Set α
hs : s.Nonempty
inr : Eq (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup {⊥})
⊢ Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) (sSup ((fun (x_1 : α) ↦ ⊥) '' s))
have inr₁ : Eq.{u_3 + 1} (α := β) ((fun (x_1 : α) ↦ (⊥ : β)) (sSup s)) ⊥
Tactic: rw [hs.image_const, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
f g : FrameHom α β
h : Eq (α := (a : α) → β) ((fun (f : FrameHom α β) ↦ f.toFun) f) ((fun (f : FrameHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b)
  (map_top' : { toFun := toFun, map_inf' := map_inf' : InfHom α β }.toFun ⊤ = ⊤)
  (map_sSup' :
    ∀ (s : Set α),
      { toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun (sSup s) =
        sSup ({ toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun '' s))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : FrameHom α β) ↦ f.toFun)
        { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
      ((fun (f : FrameHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } = g
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
g : FrameHom α β
toFun : α → β
map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b
map_top' : { toFun := toFun, map_inf' := map_inf' : InfHom α β }.toFun ⊤ = ⊤
map_sSup' :
  ∀ (s : Set α),
    { toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun (sSup s) =
      sSup ({ toFun := toFun, map_inf' := map_inf', map_top' := map_top' : InfTopHom α β }.toFun '' s)
h :
  Eq (α := (a : α) → β)
    ((fun (f : FrameHom α β) ↦ f.toFun)
      { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
    ((fun (f : FrameHom α β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } = g
have obtain : ∀ (toFun_1 : α → β) (map_inf'_1 : ∀ (a b : α), toFun_1 (a ⊓ b) = toFun_1 a ⊓ toFun_1 b)
  (map_top'_1 : { toFun := toFun_1, map_inf' := map_inf'_1 : InfHom α β }.toFun ⊤ = ⊤)
  (map_sSup'_1 :
    ∀ (s : Set α),
      { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun (sSup s) =
        sSup ({ toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1 : InfTopHom α β }.toFun '' s))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : FrameHom α β) ↦ f.toFun)
        { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' })
      ((fun (f : FrameHom α β) ↦ f.toFun)
        { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 })),
  { toFun := toFun, map_inf' := map_inf', map_top' := map_top', map_sSup' := map_sSup' : FrameHom α β } =
    { toFun := toFun_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_sSup' := map_sSup'_1 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
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.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
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.CompleteLattice (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
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]
-- Lean 4 proof step from Mathlib.Order.Hom.CompleteLattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst : FunLike F α β
inst_1 : CompleteLattice α
inst_2 : CompleteLattice β
inst_3 : CompleteLattice γ
inst_4 : CompleteLattice δ
f g : CompleteLatticeHom α β
h :
  Eq (α := (a : α) → β) ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) f)
    ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s))
  (map_sSup' :
    ∀ (s : Set α),
      { toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun (sSup s) =
        sSup ({ toFun := toFun, map_sInf' := map_sInf' : sInfHom α β }.toFun '' s))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' })
      ((fun (f : CompleteLatticeHom α β) ↦ f.toFun) g)),
  { toFun := toFun, map_sInf' := map_sInf', map_sSup' := map_sSup' : CompleteLatticeHom α β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h