awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) ≤
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
have rw : padicNorm p ((↑(f + g) : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
  max (padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))))
    (padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))))
Tactic: rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
⊢ (f + g).norm ≤ max f.norm g.norm
have this : 0 ≤ max f.norm g.norm
Tactic: have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ f + g ≈ g
have hf₁ : (f - 0).LimZero
Tactic: change LimZero (f - 0) at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ (f + g).norm ≤ max f.norm g.norm
have hfg' : f + g ≈ g
Tactic: have hfg' : f + g ≈ g := by
        change LimZero (f - 0) at hf
        change LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel_right] using hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
⊢ (f + g).norm ≤ max f.norm g.norm
have hcfg : (f + g).norm = g.norm
Tactic: have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have hcl : f.norm = 0
Tactic: have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max f.norm g.norm = g.norm
have rw : max 0 g.norm = g.norm
Tactic: rw [hcl]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ (f + g).norm ≤ max f.norm g.norm
have this : max f.norm g.norm = g.norm
Tactic: have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have rw : (f + g).norm ≤ g.norm
Tactic: rw [this, hcfg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
rw : (f + g).norm ≤ g.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have rw₁ : g.norm ≤ g.norm
Tactic: rw [this, hcfg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ f + g ≈ f
have hg₁ : (g - 0).LimZero
Tactic: change LimZero (g - 0) at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (f + g).norm ≤ max f.norm g.norm
have hfg' : f + g ≈ f
Tactic: have hfg' : f + g ≈ f := by
          change LimZero (g - 0) at hg
          change LimZero (f + g - f); · simpa only [add_sub_cancel_left, sub_zero] using hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
⊢ (f + g).norm ≤ max f.norm g.norm
have hcfg : (f + g).norm = f.norm
Tactic: have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have hcl : g.norm = 0
Tactic: have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ max f.norm g.norm = f.norm
have rw : max f.norm 0 = f.norm
Tactic: rw [hcl]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ (f + g).norm ≤ max f.norm g.norm
have this : max f.norm g.norm = f.norm
Tactic: have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : max f.norm g.norm = f.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have rw : (f + g).norm ≤ f.norm
Tactic: rw [this, hcfg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : max f.norm g.norm = f.norm
rw : (f + g).norm ≤ f.norm
⊢ (f + g).norm ≤ max f.norm g.norm
have rw₁ : f.norm ≤ f.norm
Tactic: rw [this, hcfg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : f ≈ 0
⊢ f.norm = g.norm
have hg : g ≈ 0
Tactic: have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
⊢ f.norm = g.norm
have hg : ¬g ≈ 0
Tactic: have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.norm = g.norm
have simp : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint sorry)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint sorry))
Tactic: simp only [hg, hf, norm, dif_neg, not_false_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
have a : stationaryPoint hf ≤ i
Tactic: apply stationaryPoint_spec
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
a : stationaryPoint hf ≤ i
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
have a₁ : stationaryPoint hf ≤ stationaryPoint hf
Tactic: apply stationaryPoint_spec
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
Tactic: have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
⊢ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
have a : stationaryPoint hg ≤ i
Tactic: apply stationaryPoint_spec
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
a : stationaryPoint hg ≤ i
⊢ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
have a₁ : stationaryPoint hg ≤ stationaryPoint hg
Tactic: apply stationaryPoint_spec
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have hpg : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
Tactic: have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
hpg : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have rw : padicNorm p ((↑f : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint sorry))
Tactic: rw [hpf, hpg, h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
hpg : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
rw : padicNorm p ((↑f : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have rw₁ : padicNorm p ((↑f : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) i)
Tactic: rw [hpf, hpg, h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)
hpg : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)
rw : padicNorm p ((↑f : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
rw₁ : padicNorm p ((↑f : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have rw₂ : padicNorm p ((↑g : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) i)
Tactic: rw [hpf, hpg, h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
⊢ f.norm = g.norm
have this : (f + g - 0).LimZero
Tactic: have : LimZero (f + g - 0) := h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ f.norm = g.norm
have this₁ : f ≈ -g
Tactic: have : f ≈ -g := show LimZero (f - -g) by simpa only [sub_zero, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this_1 : (f + g - 0).LimZero
this : f ≈ -g
⊢ f.norm = g.norm
have this₁ : f.norm = (-g).norm
Tactic: have : f.norm = (-g).norm := norm_equiv this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
⊢ (f + g).norm = max f.norm g.norm
have hfg : ¬f + g ≈ 0
Tactic: have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ (f + g).norm = max f.norm g.norm
have this : (f - 0).LimZero
Tactic: have : LimZero (f - 0) := hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this : (f - 0).LimZero
⊢ (f + g).norm = max f.norm g.norm
have this₁ : f + g ≈ g
Tactic: have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : f + g ≈ g
⊢ (f + g).norm = max f.norm g.norm
have h1 : (f + g).norm = g.norm
Tactic: have h1 : (f + g).norm = g.norm := norm_equiv this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
⊢ (f + g).norm = max f.norm g.norm
have h2 : f.norm = 0
Tactic: have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
⊢ (f + g).norm = max f.norm g.norm
have rw : g.norm = max f.norm g.norm
Tactic: rw [h1, h2, max_eq_right (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
rw : g.norm = max f.norm g.norm
⊢ (f + g).norm = max f.norm g.norm
have rw₁ : g.norm = max 0 g.norm
Tactic: rw [h1, h2, max_eq_right (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
rw : g.norm = max f.norm g.norm
rw₁ : g.norm = max 0 g.norm
⊢ (f + g).norm = max f.norm g.norm
have rw₂ : g.norm = g.norm
Tactic: rw [h1, h2, max_eq_right (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (f + g).norm = max f.norm g.norm
have this : (g - 0).LimZero
Tactic: have : LimZero (g - 0) := hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : (g - 0).LimZero
⊢ (f + g).norm = max f.norm g.norm
have this₁ : f + g ≈ f
Tactic: have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this_1 : (g - 0).LimZero
this : f + g ≈ f
⊢ (f + g).norm = max f.norm g.norm
have h1 : (f + g).norm = f.norm
Tactic: have h1 : (f + g).norm = f.norm := norm_equiv this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this_1 : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
⊢ (f + g).norm = max f.norm g.norm
have h2 : g.norm = 0
Tactic: have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this_1 : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ (f + g).norm = max f.norm g.norm
have rw : f.norm = max f.norm g.norm
Tactic: rw [h1, h2, max_eq_left (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this_1 : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
rw : f.norm = max f.norm g.norm
⊢ (f + g).norm = max f.norm g.norm
have rw₁ : f.norm = max f.norm 0
Tactic: rw [h1, h2, max_eq_left (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this_1 : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
rw : f.norm = max f.norm g.norm
rw₁ : f.norm = max f.norm 0
⊢ (f + g).norm = max f.norm g.norm
have rw₂ : f.norm = f.norm
Tactic: rw [h1, h2, max_eq_left (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne :
  Ne (α := ℚ) (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
    (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf)))
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ Eq (α := ℚ) (if hf : f + g ≈ 0 then 0 else padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hf)))
    (max (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf))))
have split_ifs : ∀ (hfgne : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))),
  padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
Tactic: split_ifs at hfgne ⊢
Cleared hypotheses: hfgne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
have rw : ∀
  (hfgne :
    padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
      padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
  (hfgne :
    padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
      padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg))))),
  padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
Tactic: rw [lift_index_left hf, lift_index_right hg] at hfgne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
rw :
  ∀
    (hfgne :
      padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
        padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
    (hfgne :
      padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
        padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg))))),
    padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
      max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
⊢ padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
have v1 : (hfgne :
    padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
      padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))) →
  ℕ
Tactic: rw [lift_index_left hf, lift_index_right hg] at hfgne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne_1 : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hfgne_2 :
  padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hfgne :
  padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
have rw : padicNorm p ((↑(f + g) : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) =
  max (padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))))
    (padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))))
Tactic: rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]