awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
simp_rw₁ :
  ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = iSup (o.familyOfBFamily f)
simp_rw₂ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) =
    sSup (range (o.familyOfBFamily f))
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₃ : sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) sorry) = sSup (o.brange f)
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
simp_rw₁ :
  ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = iSup (o.familyOfBFamily f)
simp_rw₂ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) =
    sSup (range (o.familyOfBFamily f))
simp_rw₃ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) = sSup (o.brange f)
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₄ : Eq (α := Ordinal.{max u_4 u_3})
  (sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) sorry))
  (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
simp_rw₁ :
  ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = iSup (o.familyOfBFamily f)
simp_rw₂ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) =
    sSup (range (o.familyOfBFamily f))
simp_rw₃ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) = sSup (o.brange f)
simp_rw₄ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯))
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₅ : Eq (α := Ordinal.{max u_4 u_3})
  (sSup
    {x : Ordinal.{max u_4 u_3} | ∃ (y : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑y : Ordinal.{u_3}) sorry = x})
  (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
simp_rw₁ :
  ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = iSup (o.familyOfBFamily f)
simp_rw₂ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) =
    sSup (range (o.familyOfBFamily f))
simp_rw₃ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) = sSup (o.brange f)
simp_rw₄ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯))
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
simp_rw₅ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup
      {x : Ordinal.{max u_4 u_3} |
        ∃ (y : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑y : Ordinal.{u_3}) ⋯ = x})
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₆ : Eq (α := Ordinal.{max u_4 u_3})
  (sSup
    {x : Ordinal.{max u_4 u_3} |
      ∃ (a : Ordinal.{u_3}) (h : Membership.mem (γ := Set Ordinal.{u_3}) {x : Ordinal.{u_3} | x < o} a), f a sorry = x})
  (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
have inl : ∀ (h : iSup f = lsub.{u_3, u_4} f), iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
Tactic: rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
inl : ∀ (h : iSup f = lsub.{u_3, u_4} f), iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
have inr : ∀ (h : iSup f < lsub.{u_3, u_4} f), iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
Tactic: rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f ↔ ∃ (i : ι), f i = iSup f
have refine_1 : ∀ (h : succ (iSup f) ≤ lsub.{u_3, u_4} f), ∃ (i : ι), f i = iSup f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
refine_1 : ∀ (h : succ (iSup f) ≤ lsub.{u_3, u_4} f), ∃ (i : ι), f i = iSup f
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f ↔ ∃ (i : ι), f i = iSup f
have refine_2 : (∃ (i : ι), f i = iSup f) → succ (iSup f) ≤ lsub.{u_3, u_4} f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
⊢ ∃ (i : ι), f i = iSup f
have refine_1 : ∀ (hf : ∀ (i : ι), f i ≠ iSup f), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
hf : ∀ (i : ι), f i ≠ iSup f
⊢ False
have this : (∀ (a : ι), f a ≠ ⨆ (i : ι), f i) ↔ ∀ (a : ι), f a < ⨆ (i : ι), f i
Tactic: have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w : ι
hf : f w = iSup f
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f
have refine_2 : f w < lsub.{u_3, u_4} f
Tactic: rw [succ_le_iff, ← hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub.{u_3, u_4} f ↔ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
have refine_1 : ∀ (h : iSup f = lsub.{u_3, u_4} f), ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
Tactic: refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
refine_1 : ∀ (h : iSup f = lsub.{u_3, u_4} f), ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ↔ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
have refine_2 : ∀ (hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f) (i : ι), f i < iSup f
Tactic: refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
⊢ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
have refine_1 : ∀ a < iSup f, succ a < iSup f
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
⊢ f i < iSup f
have refine_2 : ∀ (hle : iSup f ≤ f i), False
Tactic: by_contra! hle
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
⊢ False
have heq : succ (iSup f) = lsub.{u_3, u_4} f
Tactic: have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
⊢ iSup f < lsub.{u_3, u_4} f
have rw : iSup f < succ (iSup f)
Tactic: rw [← heq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
⊢ False
have this : succ (iSup f) < lsub.{u_3, u_4} f
Tactic: have :=
    hf _
      (by
        rw [← heq]
        exact lt_succ (iSup f))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
this : succ (iSup f) < lsub.{u_3, u_4} f
⊢ False
have this₁ : lsub.{u_3, u_4} f < lsub.{u_3, u_4} f
Tactic: rw [heq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
i : ι
⊢ f i < iSup f
have rw : f i < lsub.{u_3, u_4} f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub.{u_3, u_4} f = 0
have rw : ∀ (i : ι), f i < 0
Tactic: rw [← nonpos_iff_eq_zero, lsub_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
⊢ lsub.{u_3, v} f = 0 ↔ IsEmpty ι
have refine : ∀ (h : lsub.{u_3, v} f = 0) (i : ι), False
Tactic: refine ⟨fun h => ⟨fun i => ?_⟩, fun h => @lsub_empty _ h _⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
⊢ False
have this : 0 < lsub.{u_3, v} f
Tactic: have := @lsub_pos.{_, v} _ ⟨i⟩ f
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
this : 0 < lsub.{u_3, v} f
⊢ False
have this₁ : LT.lt (α := Ordinal.{max u_3 v}) 0 0
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)
have h₁ : range (succ ∘ f) = succ '' range f
Tactic: convert! Set.image_mono h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
h₁ : range (succ ∘ f) = succ '' range f
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)
have h₂ : range (succ ∘ g) = succ '' range g
Tactic: convert! Set.image_mono h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
h₁ : range (succ ∘ f) = succ '' range f
h₂ : range (succ ∘ g) = succ '' range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)
have convert_2 : Ordinal.{max (max u v) w} → Ordinal.{max u v w}
Tactic: convert! Set.image_mono h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
⊢ o ≤
    lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u})
have by_contra! : ∀
  (h :
    lsub (ι := o.ToType)
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦
              x1 < x2) (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
          (a : o.ToType) → Ordinal.{u}) <
      o),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
o : Ordinal.{u}
h :
  lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) <
    o
⊢ False
have h₁ : lsub (ι := o.ToType)
    (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
      (a : o.ToType) → Ordinal.{u}) <
  type fun (x1 x2 : o.ToType) ↦ x1 < x2
Tactic: have h := h.trans_eq (type_toType o).symm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ iSup (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) =
    o
have ho₁ : IsSuccPrelimit o
Tactic: replace ho : IsSuccPrelimit o := by rwa [isSuccPrelimit_iff_succ_lt]
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ iSup (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) =
    o
have rw : sSup
    {b : Ordinal.{u} |
      b <
        PrincipalSeg.top (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)} =
  o
Tactic: rw [iSup, PrincipalSeg.range_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
⊢ iSup (ι := (succ o).ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
            x1 < x2) (typein fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) :
        (a : (succ o).ToType) → Ordinal.{u_3}) =
    o
have rw : sSup
    {b : Ordinal.{u_3} |
      b <
        PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
          x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2)} =
  sSup (Iic o)
Tactic: rw [← csSup_Iic (a := o), iSup, PrincipalSeg.range_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
⊢ sSup
      {b : Ordinal.{u_3} |
        b <
          PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2)} =
    sSup (Iic o)
have e_a : Eq.{u_3 + 2} (α := Ordinal.{u_3} → Prop)
  (fun (b : Ordinal.{u_3}) ↦
    b <
      PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
        x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2))
  fun (x : Ordinal.{u_3}) ↦ x ≤ o
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub.{u, v} (familyOfBFamily' r ho f) = lsub.{u, v} (familyOfBFamily' r' ho' f)
have rw : blsub.{u, v} o f = lsub.{u, v} (familyOfBFamily' r' ho' f)
Tactic: rw [lsub_eq_blsub', lsub_eq_blsub']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
rw : blsub.{u, v} o f = lsub.{u, v} (familyOfBFamily' r' ho' f)
⊢ lsub.{u, v} (familyOfBFamily' r ho f) = lsub.{u, v} (familyOfBFamily' r' ho' f)
have rw₁ : blsub.{u, v} o f = blsub.{u, v} o f
Tactic: rw [lsub_eq_blsub', lsub_eq_blsub']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
r r' : ι → ι → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ blsub.{u, v} (type r) (bfamilyOfFamily' r f) = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)
have rw : lsub.{u, v} f = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)
Tactic: rw [blsub_eq_lsub', blsub_eq_lsub']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
r r' : ι → ι → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
rw : lsub.{u, v} f = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)
⊢ blsub.{u, v} (type r) (bfamilyOfFamily' r f) = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)
have rw₁ : lsub.{u, v} f = lsub.{u, v} f
Tactic: rw [blsub_eq_lsub', blsub_eq_lsub']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ blsub.{u, v} o₁ f = blsub.{u, v} o₂ fun (a : Ordinal.{u}) (h : a < o₂) ↦ f a ⋯
have subst : blsub.{u, v} o₁ f = blsub.{u, v} o₁ fun (a : Ordinal.{u}) (h : a < o₁) ↦ f a sorry
Tactic: subst ho
Cleared hypotheses: o₂, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ blsub.{u, v} o f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a
have h : ∀ (a_1 : Ordinal.{u}), (∀ (h : a_1 < o), f a_1 h < a) ↔ ∀ (h : a_1 < o), succ (f a_1 h) ≤ a
Tactic: convert! bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ bsup.{u, v} o f = blsub.{u, v} o f ∨ succ (bsup.{u, v} o f) = blsub.{u, v} o f
have rw : iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ∨
  succ (iSup (o.familyOfBFamily f)) = lsub.{u, v} (o.familyOfBFamily f)
Tactic: rw [← iSup_eq_bsup, ← lsub_eq_blsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
have refine_1 : ∀ (h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f), ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
refine_1 : ∀ (h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f), ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
have refine_2 : (∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f) → succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
⊢ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
have refine_1 : ∀ (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ bsup.{u, v} o f), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w : Ordinal.{u}
w_1 : w < o
hf : f w w_1 = bsup.{u, v} o f
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
have refine_2 : f w w_1 < blsub.{u, v} o f
Tactic: rw [succ_le_iff, ← hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ bsup.{u, v} o f = blsub.{u, v} o f ↔ ∀ a < blsub.{u, v} o f, succ a < blsub.{u, v} o f
have rw : iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ↔
  ∀ a < lsub.{u, v} (o.familyOfBFamily f), succ a < lsub.{u, v} (o.familyOfBFamily f)
Tactic: rw [← iSup_eq_bsup, ← lsub_eq_blsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : bsup.{u, v} o f = blsub.{u, v} o f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < bsup.{u, v} o f
have rw : ∀ (hi : i < o), f i hi < blsub.{u, v} o f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ bsup.{u, v} o f = blsub.{u, v} o f
have rw : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < bsup.{u, v} o f
Tactic: rw [bsup_eq_blsub_iff_lt_bsup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ blsub.{u_3, u_4} o f = 0 ↔ o = 0
have rw : IsEmpty.{u_3 + 1} o.ToType ↔ o = 0
Tactic: rw [← lsub_eq_blsub, lsub_eq_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ blsub.{u_3, u_4} 0 f = 0
have rw : Eq.{u_3 + 2} (α := Ordinal.{u_3}) 0 0
Tactic: rw [blsub_eq_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ blsub.{u, v} (type r) f ≤ o ↔
    (lsub.{u, v} fun (a : α) ↦
        f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a)
          ⋯) ≤
      o
have rw : (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔
  ∀ (i : α),
    f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) i) sorry < o
Tactic: rw [blsub_le_iff, lsub_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
h_1 :
  Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o.brange fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) a
b : Ordinal.{u}
hb : b < o
hb' : (fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) b hb = a
⊢ Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a
have obtain : ∀ (c : Ordinal.{v}) (hc : c < o') (hc' : g c hc = f b hb),
  Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a
Tactic: obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩