awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
inr : ∀ (hne : Ne (α := ℕ∞) 0 ⊤), 0 ≤ 0 * c
⊢ a ≤ a * c
have inr₁ : ∀ (h0 : a ≠ 0), a ≤ a * c
Tactic: obtain rfl | h0 := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ c * a
have rw : a ≤ a * c
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
⊢ x = default
have this : (↑x : ℕ∞) * x.inv = 1
Tactic: have := x.val_inv
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
⊢ x = default
have x_top : (↑x : ℕ∞) ≠ ⊤
Tactic: have x_top : x.val ≠ ⊤ := by
      intro h
      simp [h] at this
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
⊢ x = default
have x_inv_top : x.inv ≠ ⊤
Tactic: have x_inv_top : x.inv ≠ ⊤ := by
      intro h
      simp only [h, ne_eq, x.ne_zero, not_false_eq_true, mul_top, top_ne_one] at this
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
⊢ x = default
have obtain : ∀ (y : ℕ) (x_y : (↑y : ℕ∞) = (↑x : ℕ∞)), x = default
Tactic: obtain ⟨y, x_y⟩ := ne_top_iff_exists.1 x_top
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y : ℕ
x_y : (↑y : ℕ∞) = (↑x : ℕ∞)
⊢ x = default
have obtain : ∀ (z : ℕ) (x_z : (↑z : ℕ∞) = x.inv), x = default
Tactic: obtain ⟨z, x_z⟩ := ne_top_iff_exists.1 x_inv_top
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y : ℕ
x_y : (↑y : ℕ∞) = (↑x : ℕ∞)
z : ℕ
x_z : (↑z : ℕ∞) = x.inv
⊢ x = default
have x_y₁ : (↑x : ℕ∞) = (↑y : ℕ∞)
Tactic: replace x_y := x_y.symm
Cleared hypotheses: x_y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : (↑x : ℕ∞) * x.inv = 1
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
⊢ x = default
have rw : ∀ (z : ℕ) (this : y = 1 ∧ z = 1) (x_z : (↑z : ℕ∞) = x.inv) (x_y : (↑x : ℕ∞) = (↑y : ℕ∞)), x = default
Tactic: rw [x_y, ← x_z, ← coe_mul, ← coe_one, coe_inj, _root_.mul_eq_one] at this
Cleared hypotheses: this, z, x_z, x_y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
⊢ x = default
have rwa : ∀ (x_y : (↑x : ℕ∞) = (↑1 : ℕ∞)), x = default
Tactic: rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y
Cleared hypotheses: x_y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
rwa : ∀ (x_y : (↑x : ℕ∞) = (↑1 : ℕ∞)), x = default
⊢ x = default
have rwa₁ : ∀ (x_y : (↑x : ℕ∞) = 1), x = default
Tactic: rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y
Cleared hypotheses: x_y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : (↑x : ℕ∞) ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : (↑z : ℕ∞) = x.inv
x_y : (↑x : ℕ∞) = (↑y : ℕ∞)
rwa : ∀ (x_y : (↑x : ℕ∞) = (↑1 : ℕ∞)), x = default
rwa₁ : ∀ (x_y : (↑x : ℕ∞) = 1), x = default
⊢ x = default
have rwa₂ : ∀ (x_y : x = 1), x = default
Tactic: rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y
Cleared hypotheses: x_y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n_1 : WithTop ℕ∞
n : ℕ
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 = (↑⊤ : WithTop ℕ∞) ↔
    Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)
have norm_cast : Eq (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤ ↔ Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
⊢ LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast n)
have top : LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast ⊤)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ∞
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
top : LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast ⊤)
⊢ LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast n)
have coe : ∀ (a : ℕ), LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast (↑a : ℕ∞))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
Tactic: have : ∀ z, map f z = 0 ↔ z = 0 := fun z =>
        (WithTop.map_injective hf).eq_iff' f.toZeroHom.ENatMap.map_zero
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inl : map (⇑f : (a : ℕ) → S) (0 * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) 0) (map (⇑f : (a : ℕ) → S) y)
Tactic: rcases Decidable.eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
inl : map (⇑f : (a : ℕ) → S) (0 * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) 0) (map (⇑f : (a : ℕ) → S) y)
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inr : ∀ (hx : x ≠ 0),
  map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
Tactic: rcases Decidable.eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inr : map (⇑f : (a : ℕ) → S) (x * 0) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) 0)
Tactic: rcases Decidable.eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hx : x ≠ 0
inr : map (⇑f : (a : ℕ) → S) (x * 0) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) 0)
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inr₁ : ∀ (hy : y ≠ 0),
  map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
Tactic: rcases Decidable.eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (hypothesis)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
x : ℕ
hx : Ne (α := ℕ∞) (↑x : ℕ∞) 0
hy : Ne (α := ℕ∞) ⊤ 0
⊢ map (⇑f : (a : ℕ) → S) (HMul.hMul (α := ℕ∞) (↑x : ℕ∞) ⊤) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) ⊤)
have this₁ : Ne (α := WithTop S) ((↑((f : (a : ℕ) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)
Tactic: have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hy : y ≠ 0
x : ℕ
hx : Ne (α := ℕ∞) (↑x : ℕ∞) 0
⊢ map (⇑f : (a : ℕ) → S) ((↑x : ℕ∞) * y) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) y)
have inr : ∀ (hy : Ne (α := ℕ∞) ⊤ 0),
  map (⇑f : (a : ℕ) → S) (HMul.hMul (α := ℕ∞) (↑x : ℕ∞) ⊤) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) ⊤)
Tactic: induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -coe_mul]
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hy : y ≠ 0
x : ℕ
hx : Ne (α := ℕ∞) (↑x : ℕ∞) 0
inr :
  ∀ (hy : Ne (α := ℕ∞) ⊤ 0),
    map (⇑f : (a : ℕ) → S) (HMul.hMul (α := ℕ∞) (↑x : ℕ∞) ⊤) =
      HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) ⊤)
⊢ map (⇑f : (a : ℕ) → S) ((↑x : ℕ∞) * y) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) y)
have inr₁ : ∀ (y : ℕ) (hy : Ne (α := ℕ∞) (↑y : ℕ∞) 0),
  map (⇑f : (a : ℕ) → S) (HMul.hMul (α := ℕ∞) (↑x : ℕ∞) (↑y : ℕ∞)) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) (↑y : ℕ∞))
Tactic: induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -coe_mul]
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inr : ∀ (hx : Ne (α := ℕ∞) ⊤ 0),
  map (⇑f : (a : ℕ) → S) (⊤ * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) ⊤) (map (⇑f : (a : ℕ) → S) y)
Tactic: induction x with
      | top => simp [hy, this]
      | coe x =>
        induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -coe_mul]
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst : MulZeroOneClass S
inst_1 : DecidableEq S
inst_2 : Nontrivial S
f : ℕ →*₀ S
hf : Injective (α := ℕ) (β := S) (⇑f : (a : ℕ) → S)
x y : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
inr :
  ∀ (hx : Ne (α := ℕ∞) ⊤ 0),
    map (⇑f : (a : ℕ) → S) (⊤ * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) ⊤) (map (⇑f : (a : ℕ) → S) y)
⊢ map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) y)
have inr₁ : ∀ (x : ℕ) (hx : Ne (α := ℕ∞) (↑x : ℕ∞) 0),
  map (⇑f : (a : ℕ) → S) ((↑x : ℕ∞) * y) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) y)
Tactic: induction x with
      | top => simp [hy, this]
      | coe x =>
        induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -coe_mul]
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : WithBot ℕ∞
m : ℕ
⊢ n < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ n ≤ (↑m : WithBot ℕ∞)
have bot : LT.lt (α := WithBot ℕ∞) ⊥ (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ LE.le (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : WithBot ℕ∞
m : ℕ
bot : LT.lt (α := WithBot ℕ∞) ⊥ (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ LE.le (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
⊢ n < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ n ≤ (↑m : WithBot ℕ∞)
have coe : ∀ (a : ℕ∞), (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe₁ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑1 : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₁ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑1 : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe₂ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₁ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑1 : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₂ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe₃ : a ≤ (↑m : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₁ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑1 : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₂ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₃ : a ≤ (↑m : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe₄ : (↑a : WithBot ℕ∞) ≤ (↑(↑m : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
a : ℕ∞
coe : a < (↑(m + 1) : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₁ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑1 : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₂ : a < HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₃ : a ≤ (↑m : ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
coe₄ : (↑a : WithBot ℕ∞) ≤ (↑(↑m : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
have coe₅ : (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
Tactic: rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
m : WithBot ℕ∞
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ m ↔ (↑n : WithBot ℕ∞) < m
have bot : LE.le (α := WithBot ℕ∞) (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ⊥ ↔ LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊥
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
m : WithBot ℕ∞
bot : LE.le (α := WithBot ℕ∞) (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ⊥ ↔ LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊥
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ m ↔ (↑n : WithBot ℕ∞) < m
have coe : ∀ (a : ℕ∞), (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑1 : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑1 : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑1 : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe₃ : (↑n : ℕ∞) < a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑1 : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₃ : (↑n : ℕ∞) < a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe₄ : (↑(↑n : ℕ∞) : WithBot ℕ∞) < (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : ℕ
a : ℕ∞
coe : (↑(n + 1) : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑1 : ℕ∞) ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₃ : (↑n : ℕ∞) < a ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
coe₄ : (↑(↑n : ℕ∞) : WithBot ℕ∞) < (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
have coe₅ : (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
Tactic: rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
m : ℕ
n : ℕ∞
⊢ (↑n : WithBot ℕ∞) + 1 ≤ (↑m : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑m : WithBot ℕ∞)
have coe : n + 1 ≤ (↑m : ℕ∞) ↔ n < (↑m : ℕ∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : WithBot ℕ∞
m : ℕ
⊢ n + 1 ≤ (↑m : WithBot ℕ∞) ↔ n < (↑m : WithBot ℕ∞)
have bot : HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ (↑m : WithBot ℕ∞) ↔ LT.lt (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
Tactic: induction n with
  | bot => simp
  | coe n =>
    norm_cast
    simp [add_one_le_iff']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
n : WithBot ℕ∞
m : ℕ
bot : HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ (↑m : WithBot ℕ∞) ↔ LT.lt (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
⊢ n + 1 ≤ (↑m : WithBot ℕ∞) ↔ n < (↑m : WithBot ℕ∞)
have coe : ∀ (n : ℕ∞), (↑n : WithBot ℕ∞) + 1 ≤ (↑m : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑m : WithBot ℕ∞)
Tactic: induction n with
  | bot => simp
  | coe n =>
    norm_cast
    simp [add_one_le_iff']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : WithBot ℕ∞
c : ℕ
⊢ (↑c : WithBot ℕ∞) + a ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
have rw : a + (↑c : WithBot ℕ∞) ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
Tactic: rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : WithBot ℕ∞
c : ℕ
rw : a + (↑c : WithBot ℕ∞) ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
⊢ (↑c : WithBot ℕ∞) + a ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
have rw₁ : a + (↑c : WithBot ℕ∞) ≤ b + (↑c : WithBot ℕ∞) ↔ a ≤ b
Tactic: rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Basic (goal)
Goal:
a b : WithBot ℕ∞
c : ℕ
rw : a + (↑c : WithBot ℕ∞) ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
rw₁ : a + (↑c : WithBot ℕ∞) ≤ b + (↑c : WithBot ℕ∞) ↔ a ≤ b
⊢ (↑c : WithBot ℕ∞) + a ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)
have cons : ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
Tactic: simp only [Finset.sum_cons, ← ih]