awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
⊢ LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast ⊤)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
a : ℕ
⊢ LE.le.{u_1} (α := WithTop α) 0 (map Nat.cast (↑a : ℕ∞))

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
⊢ StrictMono.{0, u_1} (β := WithTop α) (map Nat.cast)

Tactic:
strictMono_map_iff.2 Nat.strictMono_cast

Premises used: Iff.mpr, Nat.strictMono_cast, ENat.strictMono_map_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
⊢ Injective.{1, u_1 + 1} (β := WithTop α) (map Nat.cast)

Tactic:
map_natCast_strictMono.injective

Premises used: ENat.map_natCast_strictMono, StrictMono.injective
-- Module: Mathlib.Data.ENat.Basic
Goal:
m n : ℕ∞
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
⊢ Eq.{u_1 + 1} (α := WithTop α) (map Nat.cast m) (map Nat.cast n) ↔ m = n

Tactic:
map_natCast_injective.eq_iff

Premises used: Function.Injective.eq_iff, ENat.map_natCast_injective
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ∞
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
⊢ Eq.{u_1 + 1} (α := WithTop α) (map Nat.cast n) 0 ↔ n = 0

Tactic:
simp [← map_natCast_inj (α := α)]

Premises used: ENat.map_natCast_inj
-- Module: Mathlib.Data.ENat.Basic
Goal:
β : Type u_2
F : Type u_3
inst : Add β
inst_1 : FunLike F ℕ β
inst_2 : AddHomClass F ℕ β
f : F
a b : ℕ∞
⊢ map (⇑f : (a : ℕ) → β) (a + b) = HAdd.hAdd (α := WithTop β) (map (⇑f : (a : ℕ) → β) a) (map (⇑f : (a : ℕ) → β) b)

Tactic:
WithTop.map_add f a b

Premises used: ENat.map, WithTop.map_add
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst : One N
f : OneHom ℕ N
⊢ Eq (α := WithTop N) (map (⇑f : (a : ℕ) → N) 1) 1

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst : Zero N
f : ZeroHom ℕ N
⊢ Eq (α := WithTop N) (map (⇑f : (a : ℕ) → N) 0) 0

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
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 : ℕ∞
⊢ ∀ (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
-- Module: Mathlib.Data.ENat.Basic
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)
inr :
  ∀ (hx : x ≠ 0),
    map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (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)

Tactic:
rcases Decidable.eq_or_ne x 0 with (rfl | hx)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENat.Basic
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
⊢ map (⇑f : (a : ℕ) → S) (0 * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) 0) (map (⇑f : (a : ℕ) → S) y)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
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)
inr₁ :
  ∀ (hy : y ≠ 0),
    map (⇑f : (a : ℕ) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (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)

Tactic:
rcases Decidable.eq_or_ne y 0 with (rfl | hy)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENat.Basic
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 : ℕ∞
this : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f : (a : ℕ) → S) (x * 0) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) x) (map (⇑f : (a : ℕ) → S) 0)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
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
hx : Ne (α := ℕ∞) ⊤ 0
⊢ map (⇑f : (a : ℕ) → S) (⊤ * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) ⊤) (map (⇑f : (a : ℕ) → S) y)

Tactic:
simp [hy, this]
-- Module: Mathlib.Data.ENat.Basic
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
⊢ Ne (α := WithTop S) ((↑((f : (a : ℕ) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)

Tactic:
simpa [hf.eq_iff' (map_zero f)] using hx

Premises used: map_zero, Function.Injective.eq_iff'
-- Module: Mathlib.Data.ENat.Basic
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
⊢ 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
-- Module: Mathlib.Data.ENat.Basic
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_1 : ∀ (z : ℕ∞), Eq (α := WithTop S) (map (⇑f : (a : ℕ) → S) z) 0 ↔ z = 0
x : ℕ
hx : Ne (α := ℕ∞) (↑x : ℕ∞) 0
hy : Ne (α := ℕ∞) ⊤ 0
this : Ne (α := WithTop S) ((↑((f : (a : ℕ) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)
⊢ map (⇑f : (a : ℕ) → S) (HMul.hMul (α := ℕ∞) (↑x : ℕ∞) ⊤) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : ℕ) → S) (↑x : ℕ∞)) (map (⇑f : (a : ℕ) → S) ⊤)

Tactic:
simp [mul_top hx, WithTop.mul_top this]

Premises used: WithTop.mul_top, ENat.mul_top
-- Module: Mathlib.Data.ENat.Basic
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
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:
simp [← Nat.cast_mul, -coe_mul]

Premises used: ENat.coe_mul, Nat.cast_mul
-- Module: Mathlib.Data.ENat.Basic
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) ⊤)
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 : ℕ∞))
⊢ map (⇑f : (a : ℕ) → S) ((↑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]

Premises used: ENat.coe_mul, Nat.cast_mul, ENat.mul_top
-- Module: Mathlib.Data.ENat.Basic
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)
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)
⊢ 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]

Premises used: ENat.coe_mul, Nat.cast_mul, ENat.mul_top
-- Module: Mathlib.Data.ENat.Basic
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : DecidableEq R
inst_2 : CharZero R
a b : ℕ∞
⊢ map Nat.cast (a * b) = HMul.hMul (α := WithTop R) (map Nat.cast a) (map Nat.cast b)

Tactic:
map_mul ((Nat.castRingHom R : ℕ →*₀ R).ENatMap Nat.cast_injective) a b

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, WithTop.map, ENat.map, map_mul, Nat.castRingHom, Nat.cast_injective, MonoidWithZeroHom.ENatMap
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ Eq (α := WithBot ℕ∞) (↑(↑n : ℕ∞) : WithBot ℕ∞) (↑n : WithBot ℕ∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithBot ℕ∞
m : ℕ
bot : LT.lt (α := WithBot ℕ∞) ⊥ (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ LE.le (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
coe : ∀ (a : ℕ∞), (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ n < (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ n ≤ (↑m : WithBot ℕ∞)

Tactic:
cases n
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
⊢ LT.lt (α := WithBot ℕ∞) ⊥ (↑(↑(m + 1) : ℕ∞) : WithBot ℕ∞) ↔ LE.le (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)

Tactic:
simp only [bot_le, WithBot.bot_lt_coe]

Premises used: WithBot.bot_lt_coe, bot_le
-- Module: Mathlib.Data.ENat.Basic
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 ℕ∞)
coe₅ coe₆ : (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞) ↔ (↑a : WithBot ℕ∞) ≤ (↑m : WithBot ℕ∞)
⊢ (↑a : WithBot ℕ∞) < (↑(↑(m + 1) : ℕ∞) : 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]

Premises used: ENat.coe_one, WithBot.coe_le_coe, Nat.cast_add, ENat.lt_add_one_iff, WithBot.coe_lt_coe, ENat.coe_ne_top, WithBot.coe_natCast
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
m : WithBot ℕ∞
bot : LE.le (α := WithBot ℕ∞) (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ⊥ ↔ LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊥
coe : ∀ (a : ℕ∞), (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ≤ m ↔ (↑n : WithBot ℕ∞) < m

Tactic:
cases m
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : ℕ
⊢ LE.le (α := WithBot ℕ∞) (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ⊥ ↔ LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊥

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
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 ℕ∞)
coe₅ coe₆ : (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑a : WithBot ℕ∞)
⊢ (↑(↑(n + 1) : ℕ∞) : 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]

Premises used: ENat.coe_one, ENat.add_one_le_iff, WithBot.coe_le_coe, WithBot.coe_lt_coe, ENat.coe_ne_top, WithBot.coe_natCast, ENat.coe_add
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
⊢ HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ (↑m : WithBot ℕ∞) ↔ LT.lt (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : ℕ∞
coe : n + 1 ≤ (↑m : ℕ∞) ↔ n < (↑m : ℕ∞)
⊢ (↑n : WithBot ℕ∞) + 1 ≤ (↑m : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑m : WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENat.Basic
Goal:
m : ℕ
n : ℕ∞
⊢ n + 1 ≤ (↑m : ℕ∞) ↔ n < (↑m : ℕ∞)

Tactic:
simp [add_one_le_iff']

Premises used: ENat.add_one_le_iff'
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithBot ℕ∞
m : ℕ
bot : HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ (↑m : WithBot ℕ∞) ↔ LT.lt (α := WithBot ℕ∞) ⊥ (↑m : WithBot ℕ∞)
coe : ∀ (n : ℕ∞), (↑n : WithBot ℕ∞) + 1 ≤ (↑m : WithBot ℕ∞) ↔ (↑n : WithBot ℕ∞) < (↑m : WithBot ℕ∞)
⊢ n + 1 ≤ (↑m : WithBot ℕ∞) ↔ n < (↑m : WithBot ℕ∞)

Tactic:
induction n with
  | bot => simp
  | coe n =>
    norm_cast
    simp [add_one_le_iff']

Premises used: ENat.add_one_le_iff'
-- Module: Mathlib.Data.ENat.Basic
Goal:
n : WithBot ℕ∞
⊢ n + 1 ≤ 0 ↔ n = ⊥

Tactic:
add_one_le_natCast_iff.trans (WithBot.lt_zero_iff_eq_bot n)

Premises used: WithTop.some, Iff.trans, ENat.WithBot.add_one_le_natCast_iff, WithBot.lt_zero_iff_eq_bot
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
⊢ a + (↑c : WithBot ℕ∞) = b + (↑c : WithBot ℕ∞) ↔ a = b

Tactic:
(IsAddRightRegular.all c).withTop.withBot.eq_iff

Premises used: Function.Injective.eq_iff, IsAddRightRegular.withBot, IsAddRightRegular.all, ENat, IsAddRightRegular.withTop
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
⊢ a + 1 = b + 1 ↔ a = b

Tactic:
(IsAddRightRegular.all 1).withTop.withBot.eq_iff

Premises used: Function.Injective.eq_iff, IsAddRightRegular.withBot, WithTop.some, IsAddRightRegular.all, ENat, IsAddRightRegular.withTop, OfNat.ofNat
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
inst : c.AtLeastTwo
⊢ a + OfNat.ofNat c = b + OfNat.ofNat c ↔ a = b

Tactic:
WithBot.add_natCast_cancel

Premises used: ENat.WithBot.add_natCast_cancel
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
⊢ (↑c : WithBot ℕ∞) + a = (↑c : WithBot ℕ∞) + b ↔ a = b

Tactic:
(IsAddLeftRegular.all c).withTop.withBot.eq_iff

Premises used: Function.Injective.eq_iff, IsAddLeftRegular.all, ENat, IsAddLeftRegular.withTop, IsAddLeftRegular.withBot
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
⊢ 1 + a = 1 + b ↔ a = b

Tactic:
(IsAddLeftRegular.all 1).withTop.withBot.eq_iff

Premises used: Function.Injective.eq_iff, WithTop.some, IsAddLeftRegular.all, ENat, IsAddLeftRegular.withTop, OfNat.ofNat, IsAddLeftRegular.withBot
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
inst : c.AtLeastTwo
⊢ OfNat.ofNat c + a = OfNat.ofNat c + b ↔ a = b

Tactic:
WithBot.natCast_add_cancel

Premises used: ENat.WithBot.natCast_add_cancel
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
⊢ a + (↑c : WithBot ℕ∞) ≤ b + (↑c : WithBot ℕ∞) ↔ a ≤ b

Tactic:
(Contravariant.AddLECancellable (a := c)).withTop.withBot.add_le_add_iff_right

Premises used: AddLECancellable.withTop, ENat, AddLECancellable.add_le_add_iff_right, Contravariant.AddLECancellable, AddLECancellable.withBot
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
⊢ a + 1 ≤ b + 1 ↔ a ≤ b

Tactic:
WithBot.add_le_add_natCast_right_iff

Premises used: WithTop.some, ENat.WithBot.add_le_add_natCast_right_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
c : ℕ
rw : a + (↑c : WithBot ℕ∞) ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b
rw₁ : a + (↑c : WithBot ℕ∞) ≤ b + (↑c : WithBot ℕ∞) ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ (↑c : WithBot ℕ∞) + a ≤ (↑c : WithBot ℕ∞) + b ↔ a ≤ b

Tactic:
rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]

Premises used: add_comm, ENat.WithBot.add_le_add_natCast_right_iff
-- Module: Mathlib.Data.ENat.Basic
Goal:
a b : WithBot ℕ∞
⊢ 1 + a ≤ 1 + b ↔ a ≤ b

Tactic:
WithBot.add_le_add_natCast_left_iff

Premises used: ENat.WithBot.add_le_add_natCast_left_iff, WithTop.some
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
ι : Type u_2
s : Finset ι
f : ι → ℕ∞
⊢ toNat (∏ i ∈ s, f i) = ∏ i ∈ s, (f i).toNat

Tactic:
map_prod toNatHom _ _

Premises used: ENat.toNatHom, map_prod, ENat.toNat, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Data.ENat.BigOperators
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
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)

Tactic:
simp only [Finset.sum_empty, ciInf_const]

Premises used: Finset.sum_empty, ciInf_const
-- Module: Mathlib.Data.ENat.BigOperators
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)
cons : ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)

Tactic:
simp only [Finset.sum_cons, ← ih]

Premises used: Finset.sum_cons
-- Module: Mathlib.Data.ENat.BigOperators
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)
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)

Tactic:
(iInf_add_iInf fun i j => ?_).symm

Premises used: ENat.iInf_add_iInf, Eq.symm
-- Module: Mathlib.Data.ENat.BigOperators
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)
cons : ∀ (i j : ι), ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)

Tactic:
refine (iInf_add_iInf fun i j => ?_).symm

Premises used: ENat.iInf_add_iInf, Eq.symm
-- Module: Mathlib.Data.ENat.BigOperators
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)
i j : ι
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
(h (Finset.cons a s ha) i j).imp fun k hk => ?_

Premises used: Finset.cons, Exists.imp
-- Module: Mathlib.Data.ENat.BigOperators
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)
i j : ι
cons :
  ∀ (k : ι) (hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1),
    f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_

Premises used: Finset.cons, Exists.imp
-- Module: Mathlib.Data.ENat.BigOperators
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)
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x

Tactic:
rw [Finset.forall_mem_cons] at hk

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Data.ENat.BigOperators
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)
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: add_le_add, And.right, And.left, Finset.sum_le_sum
-- Module: Mathlib.Data.ENat.BigOperators
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)
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: add_le_add, And.right, And.left, Finset.sum_le_sum
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
empty : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
cons :
  ∀ (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)
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: ENat.iInf_add_iInf, Finset.sum_cons, Finset.forall_mem_cons, Finset.sum_empty, Eq.symm, ciInf_const
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
h : ∀ a ∈ s, f a ≠ ⊤
⊢ Ne (α := ℕ∞) (∏ a ∈ s, f a) ⊤

Tactic:
WithTop.prod_ne_top h

Premises used: ENat, WithTop.prod_ne_top