awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
zero :
  ∀
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)),
    Eq (α := ℕ) 0 0
⊢ 0 = m
have zero₁ : ∀ (m : ℕ)
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        0)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        (m + 1))),
  0 = m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
⊢ n + 1 = m
have succ : ∀
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        (n + 1))
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        0)),
  n + 1 = 0
Tactic: rcases m with - | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
succ :
  ∀
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (n + 1))
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)),
    n + 1 = 0
⊢ n + 1 = m
have succ₁ : ∀ (m : ℕ)
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        (n + 1))
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        (m + 1))),
  n + 1 = m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (m + 1))
⊢ n + 1 = m + 1
have succ : Eq (α := WType β)
  ((fun (n : ℕ) ↦
      have this : WType β :=
        Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
          mk (β := β) a fun (x : β a) ↦ ih;
      this)
    n)
  ((fun (n : ℕ) ↦
      have this : WType β :=
        Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
          mk (β := β) a fun (x : β a) ↦ ih;
      this)
    m)
Tactic: refine congr_arg Nat.succ (ih ?_)
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      n)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
⊢ n = m
have zero : ∀ ⦃m : ℕ⦄
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        0)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        m)),
  0 = m
Tactic: induction n generalizing m with
    | zero => rcases m with - | m <;> simp_all
    | succ n ih =>
      rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      n)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
zero :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    0 = m
⊢ n = m
have succ : ∀ (n : ℕ)
  (ih :
    ∀ ⦃m : ℕ⦄
      (h :
        Eq (α := WType β)
          ((fun (n : ℕ) ↦
              have this : WType β :=
                Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                  mk (β := β) a fun (x : β a) ↦ ih;
              this)
            n)
          ((fun (n : ℕ) ↦
              have this : WType β :=
                Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                  mk (β := β) a fun (x : β a) ↦ ih;
              this)
            m)),
      n = m)
  ⦃m : ℕ⦄
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        (n + 1))
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        m)),
  n + 1 = m
Tactic: induction n generalizing m with
    | zero => rcases m with - | m <;> simp_all
    | succ n ih =>
      rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth (β := β)
have mk : ∀ (a : α) (f : β a → WType β), 0 < (mk (β := β) a f).depth (β := β)
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : t.depth (β := β) ≤ n + 1
⊢ (a : α) × (β a → WType' β n)
have obtain : (a : α) → (f : β a → WType β) → (h : (mk (β := β) a f).depth (β := β) ≤ n + 1) → (a : α) × (β a → WType' β n)
Tactic: obtain ⟨a, f⟩ := t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : (mk (β := β) a f).depth (β := β) ≤ n + 1
⊢ (a : α) × (β a → WType' β n)
have h₀ : ∀ (i : β a), (f i).depth (β := β) ≤ n
Tactic: have h₀ : ∀ i : β a, WType.depth (f i) ≤ n := fun i =>
      Nat.le_of_lt_succ (lt_of_lt_of_le (WType.depth_lt_depth_mk a f i) h)
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
⊢ Encodable (WType β)
have haveI : (h' : (n : ℕ) → Encodable (WType' β n)) → Encodable (WType β)
Tactic: haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
-- Lean 4 proof step from Mathlib.Data.W.Basic (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
h' : (n : ℕ) → Encodable (WType' β n)
f : WType β → (n : ℕ) × WType' β n :=
  fun (t : WType β) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ WType' β n) (t.depth (β := β))
      (Subtype.mk (p := fun (t_1 : WType β) ↦ t_1.depth (β := β) ≤ t.depth (β := β)) t ⋯)
finv : (n : ℕ) × WType' β n → WType β :=
  fun (p : (n : ℕ) × WType' β n) ↦ (↑(p.snd (β := fun (n : ℕ) ↦ WType' β n)) : WType β)
⊢ Encodable (WType β)
have this : ∀ (t : WType β), finv (f t) = t
Tactic: have : ∀ t, finv (f t) = t := fun t => rfl
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
⊢ #((a : α) × (β a → WType β)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
have simp_rw : (sum fun (i : α) ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) =
  sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
Tactic: simp_rw [mk_sigma, mk_arrow]
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
⊢ (sum fun (i : α) ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) =
    sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
have rw : (sum fun (i : α) ↦ #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
Tactic: rw [lift_id'.{v, u}, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
rw : (sum fun (i : α) ↦ #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
⊢ (sum fun (i : α) ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) =
    sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
have rw₁ : (sum fun (i : α) ↦ #(WType β) ^ lift.{u, v} #(β i)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
Tactic: rw [lift_id'.{v, u}, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
κ : Cardinal.{max u v}
hκ : (sum fun (a : α) ↦ κ ^ lift.{u, v} #(β a)) ≤ κ
⊢ #(WType β) ≤ κ
have mk : ∀ (γ : Type (max u v)) (hκ : (sum fun (a : α) ↦ #γ ^ lift.{u, v} #(β a)) ≤ #γ), #(WType β) ≤ #γ
Tactic: induction κ using Cardinal.inductionOn with | _ γ
Cleared hypotheses: κ, hκ
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (hypothesis)
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ #γ ^ lift.{u, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
have hκ₁ : (sum fun (a : α) ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
Tactic: simp_rw [← lift_umax.{v, u}] at hκ
Cleared hypotheses: hκ
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (hypothesis)
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
have hκ₁ : (sum fun (a : α) ↦ lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
Tactic: nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ
Cleared hypotheses: hκ
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (hypothesis)
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
have hκ₁ : Nonempty ((i : α) × (β i → γ) ↪ γ)
Tactic: simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ
Cleared hypotheses: hκ
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ
have mk : ∀ (hκ : (i : α) × (β i → γ) ↪ γ), #(WType β) ≤ #γ
Tactic: obtain ⟨hκ⟩ := hκ
Cleared hypotheses: hκ
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ LE.le (α := Cardinal.{max u v}) (Order.succ 0) (⨆ (a : α), m ^ lift.{u, v} #(β a))
have rw : LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
Tactic: rw [succ_zero]
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
have obtain : ∀ (a : α), LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
Tactic: obtain ⟨a⟩ : Nonempty α := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
have refine : 1 ≤ m ^ lift.{u, v} #(β a)
Tactic: refine le_trans ?_ (le_ciSup bddAbove_of_small a)
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ 1 ≤ m ^ lift.{u, v} #(β a)
have rw : HPow.hPow (β := Cardinal.{max u v}) m 0 ≤ m ^ lift.{u, v} #(β a)
Tactic: rw [← power_zero]
-- Lean 4 proof step from Mathlib.Data.W.Cardinal (goal)
Goal:
α : Type u
β : α → Type u
inst : ∀ (a : α), Finite.{u + 1} (β a)
⊢ max (lift.{u, u} #α) ℵ₀ = max #α ℵ₀
have rw : max #α ℵ₀ = max #α ℵ₀
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
f : Natβ Natα.zero → WType Natβ
⊢ mk (β := Natβ) Natα.zero Empty.elim = mk (β := Natβ) Natα.zero f
have e_f : Empty.elim = f
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f
have e_f : ∀ (x : Empty), x.elim = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
f : Natβ Natα.succ → WType Natβ
⊢ ofNat (mk (β := Natβ) Natα.succ f).toNat = mk (β := Natβ) Natα.succ f
have simp : (fun (x : Natβ Natα.succ) ↦ f ()) = f
Tactic: simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
n : ℕ
⊢ (ofNat n.succ).toNat = n.succ
have rw : toNat (mk (β := Natβ) Natα.succ fun (x : Natβ Natα.succ) ↦ ofNat n) = n.succ
Tactic: rw [ofNat, toNat, rightInverse_nat n]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
n : ℕ
rw : toNat (mk (β := Natβ) Natα.succ fun (x : Natβ Natα.succ) ↦ ofNat n) = n.succ
⊢ (ofNat n.succ).toNat = n.succ
have rw₁ : (ofNat n).toNat.succ = n.succ
Tactic: rw [ofNat, toNat, rightInverse_nat n]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
n : ℕ
rw : toNat (mk (β := Natβ) Natα.succ fun (x : Natβ Natα.succ) ↦ ofNat n) = n.succ
rw₁ : (ofNat n).toNat.succ = n.succ
⊢ (ofNat n.succ).toNat = n.succ
have rw₂ : n.succ = n.succ
Tactic: rw [ofNat, toNat, rightInverse_nat n]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (β := Listβ γ) Listα.nil f)) = mk (β := Listβ γ) Listα.nil f
have simp : PEmpty.elim = f
Tactic: simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
have h : ∀ (x : PEmpty.{u + 1}), x.elim = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.W.Constructions (goal)
Goal:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (β := Listβ γ) (Listα.cons x) f)) = mk (β := Listβ γ) (Listα.cons x) f
have simp : (fun (x : Listβ γ (Listα.cons x)) ↦ f PUnit.unit) = f
Tactic: simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ flatten (Computation.pure s) = s
have refine : Seq.IsBisimulation.{u} (α := Option α) fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1
Tactic: refine Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) ?_ rfl
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct
have rw : Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1)
  (Seq.destruct (flatten (Computation.pure s))) s.destruct
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1)
    (Seq.destruct (flatten (Computation.pure s))) s.destruct
have simp : match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
  match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
    match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) s.destruct with
    | none => none
    | some (a, b) => some (a, Computation.pure b) with
  | none => none
  | some (a, b) =>
    some
      (a,
        Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          b),
  s.destruct with
| none, none => True
| some (a, s), some (a', s') =>
  a = a' ∧
    Seq.corec
        (fun (c : Computation (WSeq α)) ↦
          match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
          | Sum.inl s =>
            match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) Seq.destruct s with
            | none => none
            | some (a, b) => some (a, Computation.pure b)
          | Sum.inr c' => some (none, c'))
        (Computation.pure s') =
      s
| x, x_1 => False
Tactic: simp only [Seq.BisimO, flatten, Seq.omap, pure_def, Seq.corec_eq, destruct_pure]