awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
n : ℤ
⊢ Eq (α := ℝ≥0) (↑n.natAbs : ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ))
have a : (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
n : ℤ
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
have a : (↑n.natAbs : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
Tactic: rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
n : ℤ
a : (↑n.natAbs : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
have a₁ : (↑|n| : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
Tactic: rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
n : ℤ
a : (↑n.natAbs : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
a₁ : (↑|n| : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
have a₂ : Eq (α := ℝ) (↑|n| : ℝ) |(↑n : ℝ)|
Tactic: rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
n : ℤ
a : (↑n.natAbs : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
a₁ : (↑|n| : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
a₂ : Eq (α := ℝ) (↑|n| : ℝ) |(↑n : ℝ)|
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
have a₃ : Eq (α := ℝ) |(↑n : ℝ)| |(↑n : ℝ)|
Tactic: rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
have inl : ∀ (hr : 0 ≤ r), ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
Tactic: obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
inl : ∀ (hr : 0 ≤ r), ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
have inr : ∀ (hr : 0 ≤ -r), ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
Tactic: obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
have inl : ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
Tactic: rw [← neg_neg r]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
have inl : ∀ (r : ℝ≥0), ∃ (x : ℝ≥0), - -(↑r : ℝ) = (↑x : ℝ) ∨ - -(↑r : ℝ) = -(↑x : ℝ)
Tactic: lift (_ : ℝ) to ℝ≥0 using hr with r
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
hr : 0 ≤ -r
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
have inr : ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
Tactic: rw [← neg_neg r]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
hr : 0 ≤ -r
⊢ ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
have inr : ∀ (r : ℝ≥0), ∃ (x : ℝ≥0), -(↑r : ℝ) = (↑x : ℝ) ∨ -(↑r : ℝ) = -(↑x : ℝ)
Tactic: lift (_ : ℝ) to ℝ≥0 using hr with r
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
⊢ r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
have obtain : ∀ (x : ℝ≥0) (hx : r = (↑x : ℝ) ∨ r = -(↑x : ℝ)), r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
Tactic: obtain ⟨x, hx⟩ := nnreal_dichotomy r
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ
x : ℝ≥0
hx : r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
⊢ r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
have rw : ¬r = 0 → ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive (↑x : ℝ)
nonpos : ∀ (x : ℝ≥0), motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ
inl : ∀ (r : ℝ≥0), motive (↑r : ℝ)
⊢ motive r
have inr : ∀ (r : ℝ≥0), motive (-(↑r : ℝ))
Tactic: obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ)
neg : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ
inl : motive 0
inr : ∀ (r : ℝ≥0) (hr : 0 < r), motive (↑r : ℝ)
⊢ motive r
have inr₁ : ∀ (r : ℝ≥0) (hr : 0 < r), motive (-(↑r : ℝ))
Tactic: obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
have obtain : ∀ (g : Γ₀ˣ) (hg1 : g ≠ 1), ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
Tactic: obtain ⟨g, hg1⟩ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mp h
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
have hu : let u := if g < 1 then g else g⁻¹;
u = if g < 1 then g else g⁻¹
Tactic: set u : Γ₀ˣ := if g < 1 then g else g⁻¹ with hu
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑(if g < 1 then g else g⁻¹) : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have pos : ∀ (hu1 : g < 1), LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (1 : ℝ≥0)
Tactic: split_ifs with hu1
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
pos : ∀ (hu1 : g < 1), LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑(if g < 1 then g else g⁻¹) : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have neg : ∀ (hu1 : ¬g < 1), LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)
Tactic: split_ifs with hu1
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have pos : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0)
Tactic: rw [← map_one f]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
Tactic: have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have hg1' : 1 < g
Tactic: have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
hg1' : 1 < g
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)
have neg : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0)
Tactic: rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
have hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
Tactic: have hfu : f u < 1 := by
    rw [hu]
    split_ifs with hu1
    · rw [← map_one f]; exact hf hu1
    · have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
      have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
      rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
      exact hf hg1'
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r),
  ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
Tactic: obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hr hfu
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
n : ℕ
hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
have h₁ : (f : (a : Γ₀) → ℝ≥0) (↑(u ^ n) : Γ₀) < r
Tactic: use u ^ n
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
n : ℕ
hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r
⊢ (f : (a : Γ₀) → ℝ≥0) (↑(u ^ n) : Γ₀) < r
have h₁ : (f : (a : Γ₀) → ℝ≥0) ((↑u : Γ₀) ^ n) < r
Tactic: rwa [Units.val_pow_eq_pow_val, map_pow]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (hypothesis)
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ
hr : 0 < r
s : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r ⋯
⊢ ∃ (d : Γ₀ˣ), (↑((f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀)) : ℝ) < r
have hs : 0 < s
Tactic: have hs : 0 < s := hr
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a b c : ℕ
⊢ a / b / c = a / c / b
have rw : a / (b * c) = a / c / b
Tactic: rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a b c : ℕ
rw : a / (b * c) = a / c / b
⊢ a / b / c = a / c / b
have rw₁ : a / (c * b) = a / c / b
Tactic: rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a b c : ℕ
rw : a / (b * c) = a / c / b
rw₁ : a / (c * b) = a / c / b
⊢ a / b / c = a / c / b
have rw₂ : a / c / b = a / c / b
Tactic: rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ (a - 1) = x ^ a / x
have rw : x ^ a / HPow.hPow (β := ℕ) x 1 = x ^ a / x
Tactic: rw [← Nat.pow_div (one_le_iff_ne_zero.mpr ha) (Nat.pos_iff_ne_zero.mpr hx), Nat.pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
rw : x ^ a / HPow.hPow (β := ℕ) x 1 = x ^ a / x
⊢ x ^ (a - 1) = x ^ a / x
have rw₁ : x ^ a / x = x ^ a / x
Tactic: rw [← Nat.pow_div (one_le_iff_ne_zero.mpr ha) (Nat.pos_iff_ne_zero.mpr hx), Nat.pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
x y : C n
H : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y
⊢ x = y
have refl : ∀ (H : x = leRecOn (C := C) sorry (fun {k : ℕ} ↦ next) y), x = y
Tactic: rwa [leRecOn_self, leRecOn_self] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
x y : C n
H : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y
refl : ∀ (H : x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y), x = y
⊢ x = y
have refl₁ : ∀ (H : x = y), x = y
Tactic: rwa [leRecOn_self, leRecOn_self] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (hypothesis)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x y : C n
H : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y
⊢ x = y
have H₁ : next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) y)
Tactic: rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
⊢ Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
have refl : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) sorry fun {k : ℕ} ↦ next)
Tactic: induction hnm with
  | refl =>
    intro x y H
    rwa [leRecOn_self, leRecOn_self] at H
  | step hnm ih =>
    intro x y H
    rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
    exact ih (Hnext _ H)
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
refl : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
⊢ Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
have step : ∀ {m : ℕ} (hnm : n.le m) (ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)),
  Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) sorry fun {k : ℕ} ↦ next)
Tactic: induction hnm with
  | refl =>
    intro x y H
    rwa [leRecOn_self, leRecOn_self] at H
  | step hnm ih =>
    intro x y H
    rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
    exact ih (Hnext _ H)
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
x : C n
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = x
have refl : leRecOn (C := C) sorry (fun {k : ℕ} ↦ next) x = x
Tactic: refine ⟨x, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
x : C n
⊢ leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = x
have refl : x = x
Tactic: rw [leRecOn_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C m_1.succ
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = x
have step : ∀ (w : C m_1), ∃ (a : C n), leRecOn (C := C) sorry (fun {k : ℕ} ↦ next) a = next w
Tactic: obtain ⟨w, rfl⟩ := Hnext _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
w : C m_1
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next w
have step : ∀ (x : C n), ∃ (a : C n), leRecOn (C := C) sorry (fun {k : ℕ} ↦ next) a = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
Tactic: obtain ⟨x, rfl⟩ := ih w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
have step : leRecOn (C := C) sorry (fun {k : ℕ} ↦ next) x = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
Tactic: refine ⟨x, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
⊢ leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
have step : next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
Tactic: rw [leRecOn_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
step :
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
⊢ leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
have step₁ : n ≤ m_1
Tactic: rw [leRecOn_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
⊢ Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
have refl : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) sorry fun {k : ℕ} ↦ next)
Tactic: induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
refl : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
⊢ Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
have step : ∀ {m : ℕ} (hnm : n.le m) (ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)),
  Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) sorry fun {k : ℕ} ↦ next)
Tactic: induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
have inl : ∀ (h : n ≤ m), n ∣ n - m ↔ m = 0 ∨ n ≤ m
Tactic: rcases le_or_gt n m with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
inl : ∀ (h : n ≤ m), n ∣ n - m ↔ m = 0 ∨ n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
have inr : ∀ (h : m < n), n ∣ n - m ↔ m = 0 ∨ n ≤ m
Tactic: rcases le_or_gt n m with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
have inr : ∀ (h : 0 < n), n ∣ n - 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ 0
Tactic: rcases eq_or_ne m 0 with rfl | hm
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
h : m < n
inr : ∀ (h : 0 < n), n ∣ n - 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
have inr₁ : ∀ (hm : m ≠ 0), n ∣ n - m ↔ m = 0 ∨ n ≤ m
Tactic: rcases eq_or_ne m 0 with rfl | hm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
have inr : ¬n ∣ n - m
Tactic: simp only [hm, h.not_ge, or_self, iff_false]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ ¬n ∣ n - m
have inr : 0 < n - m
Tactic: refine not_dvd_of_pos_of_lt ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
inr : 0 < n - m
⊢ ¬n ∣ n - m
have inr₁ : n - m < n
Tactic: refine not_dvd_of_pos_of_lt ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
have inl : ∀ (h : m ≤ n), n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Tactic: rcases le_or_gt m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
n m : ℕ
inl : ∀ (h : m ≤ n), n ∣ m - n ↔ n ∣ m ∨ m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
have inr : ∀ (h : n < m), n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Tactic: rcases le_or_gt m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * (b + 1) ≤ a ^ (b + 1)
have succ : ∀ (ha : Ne (α := ℕ) 0 1), 0 * (b + 1) ≤ HPow.hPow (α := ℕ) 0 (b + 1)
Tactic: obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
succ : ∀ (ha : Ne (α := ℕ) 0 1), 0 * (b + 1) ≤ HPow.hPow (α := ℕ) 0 (b + 1)
⊢ a * (b + 1) ≤ a ^ (b + 1)
have succ₁ : ∀ (ha0 : a > 0), a * (b + 1) ≤ a ^ (b + 1)
Tactic: obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
b : ℕ
ha : Ne (α := ℕ) 0 1
⊢ 0 * (b + 1) ≤ HPow.hPow (α := ℕ) 0 (b + 1)
have succ : 0 ≤ HPow.hPow (α := ℕ) 0 (b + 1)
Tactic: rw [Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (hypothesis)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)
have ha1 : a > 1
Tactic: have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a ^ (b + 1)
have succ : a * (b + 1) ≤ a * a ^ b
Tactic: rw [Nat.pow_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * b ≤ a ^ b
have zero : a * 0 ≤ HPow.hPow (β := ℕ) a 0
Tactic: cases b with
  | zero => exact Nat.zero_le _
  | succ b =>
      obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
      · rw [Nat.zero_mul]; exact Nat.zero_le _
      · have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)
Cleared hypotheses: b