awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
⊢ InfIrred s ↔ ∃ (a : α), Ici a = s

Tactic:
⟨fun hs ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
refine_1 : ∀ (hs : InfIrred s), ∃ (a : α), Ici a = s
refine_2 : (∃ (a : α), Ici a = s) → InfIrred s
⊢ InfIrred s ↔ ∃ (a : α), Ici a = s

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
hs : InfIrred s
refine_1 :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → y ≤ a → a ≤ y),
    ∃ (a : α), Ici a = s
⊢ ∃ (a : α), Ici a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal (coe_nonempty.2 hs.ne_top)

Premises used: Iff.mpr, InfIrred.ne_top, Set.toFinite, SetLike.coe, UpperSet.coe_nonempty, Set.Finite.exists_minimal
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
hs : InfIrred s
a : α
ha : a ∈ (↑s : Set α)
has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → y ≤ a → a ≤ y
⊢ ∃ (a : α), Ici a = s

Tactic:
⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left
      (lt_erase.2 ha).ne'⟩

Premises used: Iff.mpr, Or.resolve_left, UpperSet.erase_inf_Ici, LT.lt.ne', And.right, le_imp_eq_iff_le_imp_ge, Exists.intro, UpperSet.lt_erase
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : UpperSet α
inst_1 : Finite α
hs : InfIrred s
a : α
ha : a ∈ (↑s : Set α)
has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → y ≤ a → a ≤ y
⊢ ∃ (a : α), Ici a = s

Tactic:
exact ⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left
      (lt_erase.2 ha).ne'⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ InfIrred (α := UpperSet α) (Ici a)

Tactic:
infIrred_Ici _

Premises used: UpperSet.infIrred_Ici
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ InfIrred (α := UpperSet α) (Ici a)

Tactic:
exact infIrred_Ici _

Premises used: UpperSet.infIrred_Ici
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ SupIrred (α := LowerSet α) (Iic a)

Tactic:
⟨fun h ↦ Iic_ne_bot h.eq_bot, fun s t hst ↦ ?_⟩

Premises used: LowerSet.Iic_ne_bot, IsMin.eq_bot, And.intro, SupIrred
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
refine : ∀ (s t : LowerSet α) (hst : s ⊔ t = Iic a), s = Iic a ∨ t = Iic a
⊢ SupIrred (α := LowerSet α) (Iic a)

Tactic:
refine ⟨fun h ↦ Iic_ne_bot h.eq_bot, fun s t hst ↦ ?_⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
⊢ Membership.mem (γ := LowerSet α) (Iic a) a

Tactic:
have := mem_Iic_iff.2 (le_refl a)
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : Membership.mem (γ := LowerSet α) (Iic a) a
⊢ a ∈ s ⊔ t

Tactic:
rw [← hst] at this
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ s ⊔ t
⊢ s = Iic a ∨ t = Iic a

Tactic:
this.imp (fun ha ↦ (le_sup_left.trans_eq hst).antisymm <| Iic_le.2 ha) fun ha ↦
    (le_sup_right.trans_eq hst).antisymm <| Iic_le.2 ha

Premises used: Iff.mpr, LE.le.trans_eq, le_sup_left, LE.le.antisymm, le_sup_right, LowerSet.Iic_le, Or.imp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ s ⊔ t
⊢ s = Iic a ∨ t = Iic a

Tactic:
exact this.imp (fun ha ↦ (le_sup_left.trans_eq hst).antisymm <| Iic_le.2 ha) fun ha ↦
    (le_sup_right.trans_eq hst).antisymm <| Iic_le.2 ha

Premises used: Iff.mpr, LE.le.trans_eq, le_sup_left, LE.le.antisymm, le_sup_right, LowerSet.Iic_le, Or.imp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
⊢ SupIrred s ↔ ∃ (a : α), Iic a = s

Tactic:
⟨fun hs ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
refine_1 : ∀ (hs : SupIrred s), ∃ (a : α), Iic a = s
refine_2 : (∃ (a : α), Iic a = s) → SupIrred s
⊢ SupIrred s ↔ ∃ (a : α), Iic a = s

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
hs : SupIrred s
refine_1 :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → a ≤ y → y ≤ a),
    ∃ (a : α), Iic a = s
⊢ ∃ (a : α), Iic a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal (coe_nonempty.2 hs.ne_bot)

Premises used: Iff.mpr, SupIrred.ne_bot, Set.toFinite, SetLike.coe, Set.Finite.exists_maximal, LowerSet.coe_nonempty
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
hs : SupIrred s
a : α
ha : a ∈ (↑s : Set α)
has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → a ≤ y → y ≤ a
⊢ ∃ (a : α), Iic a = s

Tactic:
⟨a, (hs.2 <| erase_sup_Iic ha fun b hb ↦
      le_imp_eq_iff_le_imp_ge'.2 <| has hb).resolve_left (erase_lt.2 ha).ne⟩

Premises used: Iff.mpr, LowerSet.erase_sup_Iic, Or.resolve_left, LowerSet.erase_lt, And.right, le_imp_eq_iff_le_imp_ge', Exists.intro, LT.lt.ne
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
s : LowerSet α
inst_1 : Finite α
hs : SupIrred s
a : α
ha : a ∈ (↑s : Set α)
has : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ (↑s : Set α)) y → a ≤ y → y ≤ a
⊢ ∃ (a : α), Iic a = s

Tactic:
exact ⟨a, (hs.2 <| erase_sup_Iic ha fun b hb ↦
      le_imp_eq_iff_le_imp_ge'.2 <| has hb).resolve_left (erase_lt.2 ha).ne⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ SupIrred (α := LowerSet α) (Iic a)

Tactic:
supIrred_Iic _

Premises used: LowerSet.supIrred_Iic
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ SupIrred (α := LowerSet α) (Iic a)

Tactic:
exact supIrred_Iic _

Premises used: LowerSet.supIrred_Iic
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
x : α
⊢ ∀ ⦃a₂ : α⦄,
    Eq.{u_1 + 1} (α := { s : LowerSet α // SupIrred s })
        ((fun (a : α) ↦
            (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯ : { s : LowerSet α // SupIrred s }))
          x)
        ((fun (a : α) ↦
            (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯ : { s : LowerSet α // SupIrred s }))
          a₂) →
      x = a₂

Tactic:
simp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
⊢ ∀ {a b : α},
    LE.le (α := { s : LowerSet α // SupIrred s })
        (({ toFun := fun (a : α) ↦ Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯, inj' := ⋯ } :
              (a : α) → { s : LowerSet α // SupIrred s })
            a :
          { s : LowerSet α // SupIrred s })
        (({ toFun := fun (a : α) ↦ Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯, inj' := ⋯ } :
              (a : α) → { s : LowerSet α // SupIrred s })
            b :
          { s : LowerSet α // SupIrred s }) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
x : α
⊢ ∀ ⦃a₂ : α⦄,
    Eq.{u_1 + 1} (α := { s : UpperSet α // InfIrred s })
        ((fun (a : α) ↦
            (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯ : { s : UpperSet α // InfIrred s }))
          x)
        ((fun (a : α) ↦
            (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯ : { s : UpperSet α // InfIrred s }))
          a₂) →
      x = a₂

Tactic:
simp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
⊢ ∀ {a b : α},
    LE.le (α := { s : UpperSet α // InfIrred s })
        (({ toFun := fun (a : α) ↦ Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯, inj' := ⋯ } :
              (a : α) → { s : UpperSet α // InfIrred s })
            a :
          { s : UpperSet α // InfIrred s })
        (({ toFun := fun (a : α) ↦ Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯, inj' := ⋯ } :
              (a : α) → { s : UpperSet α // InfIrred s })
            b :
          { s : UpperSet α // InfIrred s }) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ Eq (α := { s : LowerSet α // SupIrred s })
    ((supIrredLowerSet : (a : α) → { s : LowerSet α // SupIrred s }) a : { s : LowerSet α // SupIrred s })
    (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯ : { s : LowerSet α // SupIrred s })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ Eq (α := { s : UpperSet α // InfIrred s })
    ((infIrredUpperSet : (a : α) → { s : UpperSet α // InfIrred s }) a : { s : UpperSet α // InfIrred s })
    (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯ : { s : UpperSet α // InfIrred s })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α) (β := { s : LowerSet α // SupIrred s })
    (⇑supIrredLowerSet : (a : α) → { s : LowerSet α // SupIrred s })

Tactic:
aesop (add simp Surjective)

Premises used: Function.Surjective
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α) (β := { s : UpperSet α // InfIrred s })
    (⇑infIrredUpperSet : (a : α) → { s : UpperSet α // InfIrred s })

Tactic:
aesop (add simp Surjective)

Premises used: Function.Surjective
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ Eq (α := { s : LowerSet α // SupIrred s })
    ((supIrredLowerSet : (a : α) → { s : LowerSet α // SupIrred s }) a : { s : LowerSet α // SupIrred s })
    (Subtype.mk (p := fun (s : LowerSet α) ↦ SupIrred s) (LowerSet.Iic a) ⋯ : { s : LowerSet α // SupIrred s })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Finite α
a : α
⊢ Eq (α := { s : UpperSet α // InfIrred s })
    ((infIrredUpperSet : (a : α) → { s : UpperSet α // InfIrred s }) a : { s : UpperSet α // InfIrred s })
    (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) ⋯ : { s : UpperSet α // InfIrred s })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Birkhoff
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

Tactic:
obtain ⟨s, hs⟩ := s
-- Module: Mathlib.Order.Birkhoff
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 α)
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 }) → α)
      (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 ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs

Premises used: LowerSet.supIrred_iff_of_finite, Iff.mp, rfl
-- Module: Mathlib.Order.Birkhoff
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 α)
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
⊢ (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 α

Premises used: nonempty_fintype
-- Module: Mathlib.Order.Birkhoff
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 α
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
⊢ (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
-- Module: Mathlib.Order.Birkhoff
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 α
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:
simp [symm_apply_eq]

Premises used: OrderIso.symm_apply_eq
-- Module: Mathlib.Order.Birkhoff
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
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
⊢ (symm supIrredLowerSet : (a : { s : LowerSet α // SupIrred s }) → α) s = (↑(↑s : 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]

Premises used: OrderIso.symm_apply_eq, nonempty_fintype, rfl
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
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
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id

Tactic:
obtain ⟨s, hs⟩ := s
-- Module: Mathlib.Order.Birkhoff
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 α)
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
⊢ (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 ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs

Premises used: Iff.mp, UpperSet.infIrred_iff_of_finite, rfl
-- Module: Mathlib.Order.Birkhoff
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 α)
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
⊢ (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 α

Premises used: nonempty_fintype
-- Module: Mathlib.Order.Birkhoff
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 α
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
⊢ (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
-- Module: Mathlib.Order.Birkhoff
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 α
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:
simp [symm_apply_eq]

Premises used: OrderIso.symm_apply_eq
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
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
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
intro :
  ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
    [inst_4 : 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
intro₁ :
  ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)]
    (val : Fintype α) (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
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : 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]

Premises used: OrderIso.symm_apply_eq, nonempty_fintype, rfl