awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
⊢ l₂_2 ⊆ l₁
have C1 : ∀ (a : Lists α), a ∈ l₂_2.toList → a ∈ l₁
Tactic: apply Lists'.subset_def.2
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
⊢ a₁ ∈ l₂_2
have C1 : ∀ (a₂ : Lists α) (m₂ : a₂ ∈ l₂_1.toList) (e₁₂ : a₁ ~ a₂), a₁ ∈ l₂_2
Tactic: rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₁₂ : a₁ ~ a₂
⊢ a₁ ∈ l₂_2
have C1 : ∀ (a₃ : Lists α) (m₃ : a₃ ∈ l₂_2.toList) (e₂₃ : a₂ ~ a₃), a₁ ∈ l₂_2
Tactic: rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
⊢ a₃ ∈ l₁
have C1 : ∀ (a₂ : Lists α) (m₂ : a₂ ∈ l₂_1.toList) (e₃₂ : a₃ ~ a₂), a₃ ∈ l₁
Tactic: rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₃₂ : a₃ ~ a₂
⊢ a₃ ∈ l₁
have C1 : ∀ (a₁ : Lists α) (m₁ : a₁ ∈ l₁.toList) (e₂₁ : a₂ ~ a₁), a₃ ∈ l₁
Tactic: rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l
have atom : ∀ (a : α), 0 < sizeOf (Lists'.atom a)
Tactic: cases l
Cleared hypotheses: b, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
l : Lists' α b
atom : ∀ (a : α), 0 < sizeOf (Lists'.atom a)
⊢ 0 < sizeOf l
have nil : 0 < sizeOf.{u_1 + 1} (α := Lists' α true) Lists'.nil
Tactic: cases l
Cleared hypotheses: b, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
l : Lists' α b
atom : ∀ (a : α), 0 < sizeOf (Lists'.atom a)
nil : 0 < sizeOf.{u_1 + 1} (α := Lists' α true) Lists'.nil
⊢ 0 < sizeOf l
have cons' : ∀ {b : Bool} (a : Lists' α b) (a_1 : Lists' α true), 0 < sizeOf (a.cons' a_1)
Tactic: cases l
Cleared hypotheses: b, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a) < sizeOf (a.cons' l)
have simp : 0 < sizeOf l
Tactic: simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α false
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔ l₁ = l₂
have atom : ∀ (a : α),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) ~
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂
Tactic: cases l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : Lists' α false
a : α
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) ~
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂
have atom : atom a = Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔ Lists'.atom a = l₂
Tactic: apply equiv_atom.trans
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : Lists' α false
a : α
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂
have atom : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ →
  Lists'.atom a = l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : Lists' α false
a : α
atom :
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ →
    Lists'.atom a = l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂
have atom₁ : Lists'.atom a = l₂ →
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
⊢ sizeOf l₁ + sizeOf l₂ <
    sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁) +
      sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
have decreasing_tactic : sizeOf l₁ + sizeOf l₂ < 2 + sizeOf l₁ + (2 + sizeOf l₂)
Tactic: decreasing_tactic
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
⊢ Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
have haveI : (this : Decidable (l₁ ⊆ l₂)) →
  Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
Tactic: haveI : Decidable (l₁ ⊆ l₂) :=
        have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) := by
          decreasing_tactic
        Subset.decidable l₁ l₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ sizeOf l₂ + sizeOf l₁ <
    sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁) +
      sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
have decreasing_tactic : sizeOf l₂ + sizeOf l₁ < 2 + sizeOf l₁ + (2 + sizeOf l₂)
Tactic: decreasing_tactic
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
have haveI : (this : Decidable (l₂ ⊆ l₁)) →
  Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
Tactic: haveI : Decidable (l₂ ⊆ l₁) :=
        have : SizeOf.sizeOf l₂ + SizeOf.sizeOf l₁ <
            SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) := by
          decreasing_tactic
        Subset.decidable l₂ l₁
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ Decidable (a.cons' l₁ ⊆ l₂)
have haveI : (this : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)) → Decidable (a.cons' l₁ ⊆ l₂)
Tactic: haveI :=
        have : sizeOf (⟨b, a⟩ : Lists α) < 1 + 1 + sizeOf a + sizeOf l₁ := by simp [sizeof_pos]
        mem.decidable ⟨b, a⟩ l₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)
⊢ Decidable (a.cons' l₁ ⊆ l₂)
have haveI : (this : Decidable (l₁ ⊆ l₂)) → Decidable (a.cons' l₁ ⊆ l₂)
Tactic: haveI :=
        have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf (Lists'.cons' a l₁) + SizeOf.sizeOf l₂ := by
          decreasing_tactic
        Subset.decidable l₁ l₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
⊢ Decidable (a ∈ b.cons' l₂)
have haveI : (this : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)) → Decidable (a ∈ b.cons' l₂)
Tactic: haveI :=
        have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
        Equiv.decidable a ⟨_, b⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
⊢ Decidable (a ∈ b.cons' l₂)
have haveI : (this : Decidable (a ∈ l₂)) → Decidable (a ∈ b.cons' l₂)
Tactic: haveI :=
        have :
          SizeOf.sizeOf a + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
          decreasing_tactic
        mem.decidable a l₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this_1 : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
this : Decidable (a ∈ l₂)
⊢ Decidable (a ∈ b.cons' l₂)
have refine : a ∈ b.cons' l₂ ↔ a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b ∨ a ∈ l₂
Tactic: refine decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this_1 : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b ∨ a ∈ l₂
have rw : a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b) l₂
Tactic: rw [← Lists'.mem_cons]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ c + a ≤ c + b → a ≤ b
have refine : ∀ (α : Type u) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u) (s : β → β → Prop) (x_1 : IsWellOrder β s)
  (γ : Type u) (t : γ → γ → Prop) (x_2 : IsWellOrder γ t),
  type t + type r ≤ type t + type s → ∀ (f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)), type r ≤ type s
Tactic: refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
⊢ type r ≤ type s
have H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
Tactic: have H₁ a : f (Sum.inl a) = Sum.inl a := by
      simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a_1 b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
⊢ ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)
have generalize : ∀ (x : γ ⊕ β) (hx : (f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) = x), ∃ (b : β), x = Sum.inr b
Tactic: generalize hx : f (Sum.inr a) = x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a_1 b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ ⊕ β
hx : (f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) = x
⊢ ∃ (b : β), x = Sum.inr b
have inl : ∀ (x : γ) (hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inl x : γ ⊕ β)),
  ∃ (b : β), Sum.inl x = Sum.inr b
Tactic: obtain x | x := x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a_1 b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ ⊕ β
hx : (f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) = x
inl :
  ∀ (x : γ) (hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inl x : γ ⊕ β)),
    ∃ (b : β), Sum.inl x = Sum.inr b
⊢ ∃ (b : β), x = Sum.inr b
have inr : ∀ (x : β) (hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr x : γ ⊕ β)),
  ∃ (b : β), Eq (α := γ ⊕ β) (Sum.inr x) (Sum.inr b)
Tactic: obtain x | x := x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a_1 b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ
hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inl x : γ ⊕ β)
⊢ ∃ (b : β), Sum.inl x = Sum.inr b
have hx₁ : Sum.inr a = Sum.inl x
Tactic: rw [← H₁, f.inj] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
⊢ type r ≤ type s
have H₂ : ∀ (a : α), ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)
Tactic: have H₂ a : ∃ b, f (Sum.inr a) = Sum.inr b := by
      generalize hx : f (Sum.inr a) = x
      obtain x | x := x
      · rw [← H₁, f.inj] at hx
        contradiction
      · exact ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
H₂ : ∀ (a : α), ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)
⊢ type r ≤ type s
have choose : ∀ (g : (a : α) → β)
  (hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)),
  type r ≤ type s
Tactic: choose g hg using H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
⊢ type r ≤ type s
have refine : ∀ (x x_1 : α) (h : r x x_1), s (g x) (g x_1)
Tactic: refine (RelEmbedding.ofMonotone g fun _ _ h ↦ ?_).ordinal_type_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u
s : β → β → Prop
h_2 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_3 : IsWellOrder γ t
h_4 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
x x_1 : α
h : r x x_1
⊢ s (g x) (g x_1)
have rwa : Sum.Lex t s (Sum.inr (g x)) (Sum.inr (g x_1))
Tactic: rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u
s : β → β → Prop
h_2 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_3 : IsWellOrder γ t
h_4 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
x x_1 : α
h : r x x_1
rwa : Sum.Lex t s (Sum.inr (g x)) (Sum.inr (g x_1))
⊢ s (g x) (g x_1)
have rwa₁ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) (Sum.inr (g x_1))
Tactic: rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u
s : β → β → Prop
h_2 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_3 : IsWellOrder γ t
h_4 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
x x_1 : α
h : r x x_1
rwa : Sum.Lex t s (Sum.inr (g x)) (Sum.inr (g x_1))
rwa₁ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) (Sum.inr (g x_1))
⊢ s (g x) (g x_1)
have rwa₂ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x_1))
Tactic: rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u
s : β → β → Prop
h_2 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_3 : IsWellOrder γ t
h_4 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
x x_1 : α
h : r x x_1
rwa : Sum.Lex t s (Sum.inr (g x)) (Sum.inr (g x_1))
rwa₁ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) (Sum.inr (g x_1))
rwa₂ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x_1))
⊢ s (g x) (g x_1)
have rwa₃ : Sum.Lex t r (Sum.inr x) (Sum.inr x_1)
Tactic: rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a + b < a + c ↔ b < c
have rw : ¬a + c ≤ a + b ↔ b < c
Tactic: rw [← not_le, ← not_le, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
rw : ¬a + c ≤ a + b ↔ b < c
⊢ a + b < a + c ↔ b < c
have rw₁ : ¬a + c ≤ a + b ↔ ¬c ≤ b
Tactic: rw [← not_le, ← not_le, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
rw : ¬a + c ≤ a + b ↔ b < c
rw₁ : ¬a + c ≤ a + b ↔ ¬c ≤ b
⊢ a + b < a + c ↔ b < c
have rw₂ : ¬c ≤ b ↔ ¬c ≤ b
Tactic: rw [← not_le, ← not_le, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h : IsWellOrder α r
β : Type u_4
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0
have simp_rw : IsEmpty.{u_4 + 1} (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
Tactic: simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]