awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ False
have hne₁ : x ≠ y ∧ y ≠ z ∧ x ≠ z
Tactic: simp only [not_or, ← Ne.eq_def] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False
have inl : ∀ (h₁ : x < y), False
Tactic: rcases hne.1.lt_or_gt with h₁ | h₁
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
inl : ∀ (h₁ : x < y), False
⊢ False
have inr : ∀ (h₁ : y < x), False
Tactic: rcases hne.1.lt_or_gt with h₁ | h₁
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False
have inl : ∀ (h₂ : y < z), False
Tactic: rcases hne.2.1.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
inl : ∀ (h₂ : y < z), False
⊢ False
have inl₁ : ∀ (h₂ : z < y), False
Tactic: rcases hne.2.1.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False
have inr : ∀ (h₂ : y < z), False
Tactic: rcases hne.2.1.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
inr : ∀ (h₂ : y < z), False
⊢ False
have inr₁ : ∀ (h₂ : z < y), False
Tactic: rcases hne.2.1.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False
have inl : ∀ (h₃ : x < z), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
inl : ∀ (h₃ : x < z), False
⊢ False
have inl₁ : ∀ (h₃ : z < x), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False
have inl : ∀ (h₃ : x < z), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
inl : ∀ (h₃ : x < z), False
⊢ False
have inl₁ : ∀ (h₃ : z < x), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False
have inr : ∀ (h₃ : x < z), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
inr : ∀ (h₃ : x < z), False
⊢ False
have inr₁ : ∀ (h₃ : z < x), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
have inr : ∀ (h₃ : x < z), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
inr : ∀ (h₃ : x < z), False
⊢ False
have inr₁ : ∀ (h₃ : z < x), False
Tactic: rcases hne.2.2.lt_or_gt with h₃ | h₃
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ InfIrred (α := UpperSet α) (Ici a)
have refine : ∀ (s t : UpperSet α) (hst : s ⊓ t = Ici a), s = Ici a ∨ t = Ici a
Tactic: refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
⊢ s = Ici a ∨ t = Ici a
have this : Membership.mem (γ := UpperSet α) (Ici a) a
Tactic: have := mem_Ici_iff.2 (le_refl a)
-- Lean 4 proof step from Mathlib.Order.Birkhoff (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : Membership.mem (γ := UpperSet α) (Ici a) a
⊢ s = Ici a ∨ t = Ici a
have this₁ : a ∈ s ⊓ t
Tactic: rw [← hst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
⊢ InfIrred s ↔ ∃ (a : α), Ici a = s
have refine_1 : ∀ (hs : InfIrred s), ∃ (a : α), Ici a = s
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
refine_1 : ∀ (hs : InfIrred s), ∃ (a : α), Ici a = s
⊢ InfIrred s ↔ ∃ (a : α), Ici a = s
have refine_2 : (∃ (a : α), Ici a = s) → InfIrred s
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
hs : InfIrred s
⊢ ∃ (a : α), Ici a = s
have refine_1 : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → y ≤ a → a ≤ y),
  ∃ (a : α), Ici a = s
Tactic: obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal (coe_nonempty.2 hs.ne_top)
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ SupIrred (α := LowerSet α) (Iic a)
have refine : ∀ (s t : LowerSet α) (hst : s ⊔ t = Iic a), s = Iic a ∨ t = Iic a
Tactic: refine ⟨fun h ↦ Iic_ne_bot h.eq_bot, fun s t hst ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
⊢ s = Iic a ∨ t = Iic a
have this : Membership.mem (γ := LowerSet α) (Iic a) a
Tactic: have := mem_Iic_iff.2 (le_refl a)
-- Lean 4 proof step from Mathlib.Order.Birkhoff (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : Membership.mem (γ := LowerSet α) (Iic a) a
⊢ s = Iic a ∨ t = Iic a
have this₁ : a ∈ s ⊔ t
Tactic: rw [← hst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
⊢ SupIrred s ↔ ∃ (a : α), Iic a = s
have refine_1 : ∀ (hs : SupIrred s), ∃ (a : α), Iic a = s
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
refine_1 : ∀ (hs : SupIrred s), ∃ (a : α), Iic a = s
⊢ SupIrred s ↔ ∃ (a : α), Iic a = s
have refine_2 : (∃ (a : α), Iic a = s) → SupIrred s
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
hs : SupIrred s
⊢ ∃ (a : α), Iic a = s
have refine_1 : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → a ≤ y → y ≤ a),
  ∃ (a : α), Iic a = s
Tactic: obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal (coe_nonempty.2 hs.ne_bot)
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : { s : LowerSet α // SupIrred s }
inst_3 : Fintype ↥(↑s : LowerSet α)
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : LowerSet α) : Set α).toFinset.sup id
have obtain : ∀ (s : LowerSet α) (hs : SupIrred s)
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)],
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: obtain ⟨s, hs⟩ := s
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : LowerSet α
hs : SupIrred s
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
have obtain : ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)],
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
Cleared hypotheses: s, hs, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
a : α
hs : SupIrred (α := LowerSet α) (LowerSet.Iic a)
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
have intro : ∀ (val : Fintype α),
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
a : α
hs : SupIrred (α := LowerSet α) (LowerSet.Iic a)
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)
val : Fintype α
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
have intro : ∀ (this : LocallyFiniteOrder α),
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : { s : LowerSet α // SupIrred s }
inst_3 : Fintype ↥(↑s : LowerSet α)
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : LowerSet α) : Set α).toFinset.sup id
have obtain : ∀ (s : LowerSet α) (hs : SupIrred s)
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)],
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : { s : LowerSet α // SupIrred s }
inst_3 : Fintype ↥(↑s : LowerSet α)
obtain :
  ∀ (s : LowerSet α) (hs : SupIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)],
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : LowerSet α) : Set α).toFinset.sup id
have obtain₁ : ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)],
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : { s : LowerSet α // SupIrred s }
inst_3 : Fintype ↥(↑s : LowerSet α)
obtain :
  ∀ (s : LowerSet α) (hs : SupIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)],
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
obtain₁ :
  ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)],
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup
        id
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : LowerSet α) : Set α).toFinset.sup id
have intro : ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)]
  (val : Fintype α),
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : Finite α
s : { s : LowerSet α // SupIrred s }
inst_3 : Fintype ↥(↑s : LowerSet α)
obtain :
  ∀ (s : LowerSet α) (hs : SupIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α)],
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) s hs) : LowerSet α) : Set α).toFinset.sup id
obtain₁ :
  ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)],
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup
        id
intro :
  ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)]
    (val : Fintype α),
    (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
        (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup
        id
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : LowerSet α) : Set α).toFinset.sup id
have intro₁ : ∀ (a : α) (hs : SupIrred (α := LowerSet α) (LowerSet.Iic a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α)]
  (val : Fintype α) (this : LocallyFiniteOrder α),
  (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α)
      (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) hs) : LowerSet α) : Set α).toFinset.sup id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id
have obtain : ∀ (s : UpperSet α) (hs : InfIrred s)
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)],
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: obtain ⟨s, hs⟩ := s
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : UpperSet α
hs : InfIrred s
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
have obtain : ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)],
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
Cleared hypotheses: s, hs, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
a : α
hs : InfIrred (α := UpperSet α) (UpperSet.Ici a)
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
have intro : ∀ (val : Fintype α),
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
a : α
hs : InfIrred (α := UpperSet α) (UpperSet.Ici a)
inst_3 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)
val : Fintype α
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
have intro : ∀ (this : LocallyFiniteOrder α),
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id
have obtain : ∀ (s : UpperSet α) (hs : InfIrred s)
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)],
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3