awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
f₁ :
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂)) =
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
⊢ (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
have f₂ : (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] a₂ ⊔ a₁) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)
Tactic: calc
      f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) :=
        Function.iterate_add_apply f n₁ n₂ _
      _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
      _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
      _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
      _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _
-- Lean 4 proof step from Mathlib.Order.Hom.PowersetCard (goal)
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
⊢ (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I))
      ((fun (f : Fin n ↪o I) ↦
          ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
        f) =
    f
have symm : f =
  (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin sorry : Fin n ↪o I))
    ((fun (f : Fin n ↪o I) ↦
        ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
      f)
Tactic: symm
-- Lean 4 proof step from Mathlib.Order.Hom.PowersetCard (goal)
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
⊢ f =
    (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I))
      ((fun (f : Fin n ↪o I) ↦
          ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
        f)
have hfs : ∀ (x : Fin n),
  Membership.mem (α := I) (γ := Finset I)
    (↑((fun (f : Fin n ↪o I) ↦
            ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
          f) :
      Finset I)
    ((f : (a : Fin n) → I) x : I)
Tactic: apply Finset.orderEmbOfFin_unique'
-- Lean 4 proof step from Mathlib.Order.Hom.PowersetCard (goal)
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
s : (↑(powersetCard I n) : Type u_1)
⊢ (fun (f : Fin n ↪o I) ↦
        ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
      ((fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I)) s) =
    s
have a : ∀ (a : I),
  Membership.mem (γ := Finset I)
      (↑((fun (f : Fin n ↪o I) ↦
              ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
            ((fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin sorry : Fin n ↪o I)) s)) :
        Finset I)
      a ↔
    a ∈ (↑s : Finset I)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ↪o β
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g
have rw : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f = g
Tactic: rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ↪o β
rw : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f = g
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g
have rw₁ : f = g ↔ f = g
Tactic: rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
⊢ Subsingleton (α ≃o β)
have refine : ∀ (f g : α ≃o β), f = g
Tactic: refine ⟨fun f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
⊢ f = g
have rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g
have rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g
have rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
⊢ f = g
have rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
⊢ f = g
have rw₄ : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
  (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
rw₄ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
⊢ f = g
have rw₅ : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
  (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
rw₄ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₅ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
⊢ f = g
have rw₆ : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
  (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
rw₄ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₅ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₆ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
⊢ f = g
have rw₇ : Eq.{u_2 + 1} (α := Set β) univ (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
rw₄ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₅ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₆ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
rw₇ : Eq.{u_2 + 1} (α := Set β) univ (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
⊢ f = g
have rw₈ : Eq.{u_2 + 1} (α := Set β) univ univ
Tactic: rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
⊢ Subsingleton (α ≃o β)
have refine : ∀ (f g : α ≃o β), f = g
Tactic: refine ⟨fun f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
f g : α ≃o β
⊢ f = g
have change : f.symm.symm = g.symm.symm
Tactic: change f.symm.symm = g.symm.symm
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
f g : α ≃o β
⊢ f.symm.symm = g.symm.symm
have rw : g.symm.symm = g.symm.symm
Tactic: rw [Subsingleton.elim f.symm]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
f g : α ≃o β
rw : g.symm.symm = g.symm.symm
⊢ f.symm.symm = g.symm.symm
have rw₁ : β ≃o α
Tactic: rw [Subsingleton.elim f.symm]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
⊢ Subsingleton (α ≃o β)
have refine : ∀ (f g : α ≃o β), f = g
Tactic: refine ⟨fun f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
f g : α ≃o β
⊢ f = g
have change : f.dual.dual = g.dual.dual
Tactic: change f.dual.dual = g.dual.dual
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual
have rw : g.dual.dual = g.dual.dual
Tactic: rw [Subsingleton.elim f.dual]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
f g : α ≃o β
rw : g.dual.dual = g.dual.dual
⊢ f.dual.dual = g.dual.dual
have rw₁ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
Tactic: rw [Subsingleton.elim f.dual]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
⊢ Subsingleton (α ≃o β)
have refine : ∀ (f g : α ≃o β), f = g
Tactic: refine ⟨fun f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
f g : α ≃o β
⊢ f = g
have change : f.dual.dual = g.dual.dual
Tactic: change f.dual.dual = g.dual.dual
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual
have rw : g.dual.dual = g.dual.dual
Tactic: rw [Subsingleton.elim f.dual]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
f g : α ≃o β
rw : g.dual.dual = g.dual.dual
⊢ f.dual.dual = g.dual.dual
have rw₁ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
Tactic: rw [Subsingleton.elim f.dual]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc x y) : Type u_1)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    ((e : (a : α) → β) (↑z : α) : β)
have simp : x ≤ (↑z : α) ∧ (↑z : α) ≤ y
Tactic: simp only [mem_Icc, map_le_map_iff]
-- Lean 4 proof step from Mathlib.Order.Hom.Set (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)
⊢ Membership.mem (α := α) (Icc x y) ((e.symm : (a : β) → α) (↑z : β) : α)
have simp : (e : (a : α) → β) x ≤ (↑z : β) ∧ (↑z : β) ≤ (e : (a : α) → β) y
Tactic: simp only [mem_Icc, e.le_symm_apply, e.symm_apply_le]
-- Lean 4 proof step from Mathlib.Order.Hom.WithTopBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
⊢ untopD ⊤
      (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
        (if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }))) =
    a
have pos : a = ⊤ → untopD ⊤ (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) ⊤) = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Hom.WithTopBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
pos : a = ⊤ → untopD ⊤ (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) ⊤) = a
⊢ untopD ⊤
      (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
        (if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }))) =
    a
have neg : ∀ (h : ¬a = ⊤),
  untopD ⊤
      (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
        (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })) =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Hom.WithTopBot (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ Eq (α := WithTop { a : α // a ≠ ⊤ })
    ((OrderIso.symm subtypeOrderIso : (a : α) → WithTop { a : α // a ≠ ⊤ }) a : WithTop { a : α // a ≠ ⊤ })
    ((↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }) : WithTop { a : α // a ≠ ⊤ })
have rw : a =
  (subtypeOrderIso : (a : WithTop { a : α // a ≠ ⊤ }) → α)
    (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })
Tactic: rw [OrderIso.symm_apply_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.WithTopBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot
have h : ∀ (a : WithTop (WithBot α)),
  Eq.{u_3 + 1} (α := WithTop (WithBot γ))
    (((f.comp g).withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a : WithTop (WithBot γ))
    ((f.withTopWithBot.comp g.withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a : WithTop (WithBot γ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
s t : Ideal P
h : s.toLowerSet = t.toLowerSet
⊢ s = t
have mk : ∀ (toLowerSet : LowerSet P) (nonempty' : toLowerSet.carrier.Nonempty)
  (directed' : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet.carrier),
  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet = t.toLowerSet →
    { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
t : Ideal P
toLowerSet : LowerSet P
nonempty' : toLowerSet.carrier.Nonempty
directed' : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet.carrier
h : { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } = t
have mk : ∀ (toLowerSet_1 : LowerSet P) (nonempty'_1 : toLowerSet_1.carrier.Nonempty)
  (directed'_1 : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet_1.carrier),
  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet =
      { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }.toLowerSet →
    { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } =
      { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.Ideal (hypothesis)
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
⊢ False
have this : Membership.mem (γ := Set P) univ p
Tactic: have := mem_univ p
-- Lean 4 proof step from Mathlib.Order.Ideal (hypothesis)
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
this : Membership.mem (γ := Set P) univ p
⊢ False
have this₁ : p ∈ (↑I : Set P)
Tactic: rw [← hp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
have obtain : ∀ (a : P) (ha : a ∈ (↑I : Set P)), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
Tactic: obtain ⟨a, ha⟩ := I.nonempty
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
have obtain : ∀ (b : P) (hb : b ∈ (↑J : Set P)), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
Tactic: obtain ⟨b, hb⟩ := J.nonempty
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
b : P
hb : b ∈ (↑J : Set P)
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
have obtain : ∀ (c : P) (hac : c ≤ a) (hbc : c ≤ b), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
Tactic: obtain ⟨c, hac, hbc⟩ := exists_le_le a b
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
⊢ I.IsProper ↔ ⊤ ∉ I
have rw : I ≠ ⊤ ↔ ⊤ ∉ I
Tactic: rw [isProper_iff_ne_top, ne_eq, top_mem_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
rw : I ≠ ⊤ ↔ ⊤ ∉ I
⊢ I.IsProper ↔ ⊤ ∉ I
have rw₁ : ¬I = ⊤ ↔ ⊤ ∉ I
Tactic: rw [isProper_iff_ne_top, ne_eq, top_mem_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
rw : I ≠ ⊤ ↔ ⊤ ∉ I
rw₁ : ¬I = ⊤ ↔ ⊤ ∉ I
⊢ I.IsProper ↔ ⊤ ∉ I
have rw₂ : ¬I = ⊤ ↔ ¬I = ⊤
Tactic: rw [isProper_iff_ne_top, ne_eq, top_mem_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
a : P
⊢ IsProper (principal a) ↔ a ≠ ⊤
have rw : ⊤ ∉ principal a ↔ a ≠ ⊤
Tactic: rw [isProper_iff_top_notMem, mem_principal, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
a : P
rw : ⊤ ∉ principal a ↔ a ≠ ⊤
⊢ IsProper (principal a) ↔ a ≠ ⊤
have rw₁ : ¬⊤ ≤ a ↔ a ≠ ⊤
Tactic: rw [isProper_iff_top_notMem, mem_principal, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
a : P
rw : ⊤ ∉ principal a ↔ a ≠ ⊤
rw₁ : ¬⊤ ≤ a ↔ a ≠ ⊤
⊢ IsProper (principal a) ↔ a ≠ ⊤
have rw₂ : ¬a = ⊤ ↔ a ≠ ⊤
Tactic: rw [isProper_iff_top_notMem, mem_principal, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
have empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((insert a s).sup f ∈ t ↔ ∀ i ∈ insert a s, f i ∈ t)
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s