awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
⊢ id t ≤ s
have refine_1 : ∀ A ∈ F.powerset, id ({i ∈ s | ∀ t ∈ F, t ∈ A ↔ i ∈ t}) ≤ s
Tactic: obtain ⟨A, _, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ Membership.mem (γ := Finset α)
    (sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id) a
have refine_2 : ∃ (i : Finset α),
  Membership.mem (γ := Finset (Finset α))
      (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) i ∧
    a ∈ id i
Tactic: rw [mem_sup]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ (i : Finset α),
    Membership.mem (γ := Finset (Finset α))
        (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) i ∧
      a ∈ id i
have refine_2 : ∀ (t : Finset α) (ht : t ∈ F), t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t
Tactic: refine
          ⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t
have refine_2 : t ∈ F ∧ a ∈ t ↔ a ∈ t
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ parts (atomise s ∅) = {s}
have simp : parts (a := s) (ofErase {s} sorry sorry) = {s}
Tactic: simp only [atomise, powerset_empty, image_singleton, notMem_empty, IsEmpty.forall_iff,
    imp_true_iff, filter_true]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id = t
have h : ∀ (a : α), a ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t
have h : ∀ (ha : a ∈ t), ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
Tactic: refine mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
have h : ∀ (u : Finset α) (hu : u ∈ parts (atomise s F)) (hau : a ∈ u),
  ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
Tactic: obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ parts (atomise s F)
hau : a ∈ u
⊢ ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
have h : ∀ (b : α) (hb : b ∈ u), b ∈ t
Tactic: refine ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ parts (atomise s F)
hau : a ∈ u
b : α
hb : b ∈ u
⊢ b ∈ t
have h : ∀ (Q : Finset (Finset α)) (_hQ : Q ⊆ F) (hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F))
  (hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}) (hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}), b ∈ t
Tactic: obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2
Cleared hypotheses: u, hu, hau, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
⊢ b ∈ t
have hau₁ : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
Tactic: rw [mem_filter] at hau hb
Cleared hypotheses: hau, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hau₁ : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
⊢ b ∈ t
have hb₁ : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
Tactic: rw [mem_filter] at hau hb
Cleared hypotheses: hau, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t
have h : t ∈ Q
Tactic: rwa [← hb.2 _ ht, hau.2 _ ht]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #({u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
have refine : #(F.erase t).powerset ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
Tactic: refine (card_le_card h).trans (card_image_le.trans ?_)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #(F.erase t).powerset ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
have rw : HPow.hPow (α := ℕ) 2 #(F.erase t) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
Tactic: rw [card_powerset, card_erase_of_mem ht]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
rw : HPow.hPow (α := ℕ) 2 #(F.erase t) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
⊢ #(F.erase t).powerset ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
have rw₁ : HPow.hPow (α := ℕ) 2 (#F - 1) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
Tactic: rw [card_powerset, card_erase_of_mem ht]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ #({u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
have suffices : {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
  image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
Tactic: suffices h :
    {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
      (F.erase t).powerset.image fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x} by
    refine (card_le_card h).trans (card_image_le.trans ?_)
    rw [card_powerset, card_erase_of_mem ht]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} →
      Membership.mem (γ := Finset (Finset α))
        (image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset) x
have simp_rw : ∀ ⦃x : Finset α⦄,
  ∀ x_1 ∈ x,
    ∀ x_2 ⊆ F,
      {i ∈ s | ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u} = x →
        x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Tactic: simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise,
    and_imp, Finset.Nonempty, exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
hy₂ : {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u} ⊆ t
j : α
_hj : j ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
⊢ ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
have refine : {i ∈ s | ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
Tactic: refine ⟨P.erase t, erase_subset_erase _ PQ, ?_⟩
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex (β := β) r (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) x y
have simp_rw : ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
Tactic: simp_rw [Pi.Lex, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
⊢ a = b
have by_contra! : ∀ (h : a ≠ b), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.PiLex (hypothesis)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : a ≠ b
⊢ False
have h₁ : ∃ (a_1 : ι), a a_1 ≠ b a_1
Tactic: rw [Function.ne_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.PiLex (hypothesis)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
⊢ False
have hri : ∀ (j : ι) (hr : r j i), a j = b j
Tactic: have hri j (hr : r j i) : a j = b j := not_not.mp (wf.not_lt_min _ · hr)
-- Lean 4 proof step from Mathlib.Order.PiLex (hypothesis)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
hri : ∀ (j : ι) (hr : r j i), a j = b j
⊢ False
have this : ¬s (b i) (a i) → a i = b i
Tactic: have := Std.Trichotomous.trichotomous (a i) (b i) (hab ⟨i, hri, ·⟩)
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
⊢ a < c
have inl : ∀ (H : N₁ < N₂), a < c
Tactic: rcases lt_trichotomy N₁ N₂ with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
inl : ∀ (H : N₁ < N₂), a < c
⊢ a < c
have inr : ∀ (lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → b j = c j) (b_lt_c : b N₁ < c N₁), a < c
Tactic: rcases lt_trichotomy N₁ N₂ with (H | rfl | H)
Cleared hypotheses: N₂, lt_N₂, b_lt_c
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
inl : ∀ (H : N₁ < N₂), a < c
inr : ∀ (lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → b j = c j) (b_lt_c : b N₁ < c N₁), a < c
⊢ a < c
have inr₁ : ∀ (H : N₂ < N₁), a < c
Tactic: rcases lt_trichotomy N₁ N₂ with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₁ : LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₂ : LT.lt (α := β default) (x default) (y default) ∨
    Eq (α := (i : ι) → β i) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
      ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₃ : (LT.lt (α := β default) (x default) (y default) ∨
    ∀ (x_1 : ι),
      Eq.{u_2 + 1} (α := β x_1) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
        ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₃ :
  (LT.lt (α := β default) (x default) (y default) ∨
      ∀ (x_1 : ι),
        Eq.{u_2 + 1} (α := β x_1) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
          ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₄ : LT.lt (α := β default) (x default) (y default) ∨
    Eq.{u_2 + 1} (α := β default) ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x default : β default)
      ((ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) y default : β default) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Lex.lt_iff_of_unique, ← ofLex_inj, funext_iff, Unique.forall_iff,
    ofLex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₁ : LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₂ : LT.lt (α := β default) (x default) (y default) ∨
    Eq (α := (i : ι) → β i) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
      ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₃ : (LT.lt (α := β default) (x default) (y default) ∨
    ∀ (x_1 : ι),
      Eq.{u_2 + 1} (α := β x_1) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
        ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
simp_rw : x < y ∨ x = y ↔ LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₁ :
  LT.lt (α := β default) (x default) (y default) ∨ x = y ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₂ :
  LT.lt (α := β default) (x default) (y default) ∨
      Eq (α := (i : ι) → β i) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x : (i : ι) → β i)
        ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y : (i : ι) → β i) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
simp_rw₃ :
  (LT.lt (α := β default) (x default) (y default) ∨
      ∀ (x_1 : ι),
        Eq.{u_2 + 1} (α := β x_1) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x x_1 : β x_1)
          ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y x_1 : β x_1)) ↔
    LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
⊢ x ≤ y ↔ LE.le (α := β default) (x default) (y default)
have simp_rw₄ : LT.lt (α := β default) (x default) (y default) ∨
    Eq.{u_2 + 1} (α := β default) ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x default : β default)
      ((ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) y default : β default) ↔
  LT.lt (α := β default) (x default) (y default) ∨ Eq (α := β default) (x default) (y default)
Tactic: simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]