awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)

Tactic:
simpa only [add_sub_cancel_left, sub_zero] using hg

Premises used: sub_zero, add_sub_cancel_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 = f.norm

Tactic:
have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ g.norm = 0

Tactic:
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw : max f.norm 0 = f.norm
⊢ max f.norm g.norm = f.norm

Tactic:
rw [hcl]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 0 = f.norm

Tactic:
max_eq_left (norm_nonneg _)

Premises used: PadicSeq.norm_nonneg, max_eq_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 0 = f.norm

Tactic:
exact max_eq_left (norm_nonneg _)

Premises used: PadicSeq.norm_nonneg, max_eq_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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

Tactic:
have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw₁ rw₂ : f.norm ≤ f.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
rw [this, hcfg]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
exact if hfg : f + g ≈ 0 then by
    have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
    simpa only [hfg, norm]
  else
    if hf : f ≈ 0 then by
      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
      have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
      have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
      have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
      rw [this, hcfg]
    else
      if hg : g ≈ 0 then by
        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
        have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
        have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
        have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
        rw [this, hcfg]
      else norm_nonarchimedean_aux hfg hf hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
classical
  exact if hfg : f + g ≈ 0 then by
    have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
    simpa only [hfg, norm]
  else
    if hf : f ≈ 0 then by
      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
      have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
      have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
      have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
      rw [this, hcfg]
    else
      if hg : g ≈ 0 then by
        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
        have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
        have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
        have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
        rw [this, hcfg]
      else norm_nonarchimedean_aux hfg hf hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : f ≈ 0
⊢ g ≈ 0

Tactic:
have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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

Tactic:
simp only [hf, hg, norm, dif_pos]

Premises used: dif_pos, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ ∀ (k : ℕ), padicNorm p ((↑g : ℕ → ℚ) k) = padicNorm p ((↑f : ℕ → ℚ) k)

Tactic:
simp only [h, forall_const]

Premises used: forall_const
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : ¬f ≈ 0
⊢ ¬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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
simp : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
⊢ f.norm = g.norm

Tactic:
simp only [hg, hf, norm, dif_neg, not_false_iff]

Premises used: dif_neg, not_false_iff, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
a₁ : stationaryPoint hf ≤ stationaryPoint hf
hf₁ : ¬f ≈ 0
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) i)

Tactic:
apply stationaryPoint_spec

Premises used: PadicSeq.stationaryPoint_spec
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hf ≤ i

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)

Tactic:
have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
a₁ : stationaryPoint hg ≤ stationaryPoint hg
hf₁ : ¬g ≈ 0
⊢ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) = padicNorm p ((↑g : ℕ → ℚ) i)

Tactic:
apply stationaryPoint_spec

Premises used: PadicSeq.stationaryPoint_spec
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hg ≤ i

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hg ≤ stationaryPoint hg

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
⊢ stationaryPoint hg ≤ stationaryPoint hg

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)

Tactic:
have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
rw₂ rw₃ : padicNorm p ((↑g : ℕ → ℚ) i) = padicNorm p ((↑g : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))

Tactic:
rw [hpf, hpg, h]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
⊢ f.norm = g.norm

Tactic:
exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]
  else by
    have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
    simp only [hg, hf, norm, dif_neg, not_false_iff]
    let i := max (stationaryPoint hf) (stationaryPoint hg)
    have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
    have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
    rw [hpf, hpg, h]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
⊢ f.norm = g.norm

Tactic:
classical
  exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]
  else by
    have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
    simp only [hg, hf, norm, dif_neg, not_false_iff]
    let i := max (stationaryPoint hf) (stationaryPoint hg)
    have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
    have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
    rw [hpf, hpg, h]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
⊢ ∀ (k : ℕ), padicNorm p ((↑(-a) : ℕ → ℚ) k) = padicNorm p ((↑a : ℕ → ℚ) k)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
⊢ (f + g - 0).LimZero

Tactic:
have : LimZero (f + g - 0) := h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ LimZero (f - -g)

Tactic:
simpa only [sub_zero, sub_neg_eq_add]

Premises used: sub_zero, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ f ≈ -g

Tactic:
have : f ≈ -g := show LimZero (f - -g) by simpa only [sub_zero, sub_neg_eq_add]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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

Tactic:
have : f.norm = (-g).norm := norm_equiv this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this_1 : (f + g - 0).LimZero
this_2 : f ≈ -g
this : f.norm = (-g).norm
⊢ f.norm = g.norm

Tactic:
simpa only [norm_neg] using this

Premises used: PadicSeq.norm_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
⊢ ¬f + g ≈ 0

Tactic:
have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ (f - 0).LimZero

Tactic:
have : LimZero (f - 0) := hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ LimZero (f + g - g)

Tactic:
simpa only [sub_zero, add_sub_cancel_right]

Premises used: sub_zero, add_sub_cancel_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ≈ g

Tactic:
have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 = g.norm

Tactic:
have h1 : (f + g).norm = g.norm := norm_equiv this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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.norm = 0

Tactic:
have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw₂ rw₃ : g.norm = g.norm
⊢ (f + g).norm = max f.norm g.norm

Tactic:
rw [h1, h2, max_eq_right (norm_nonneg _)]

Premises used: PadicSeq.norm_nonneg, max_eq_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ (g - 0).LimZero

Tactic:
have : LimZero (g - 0) := hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ LimZero (f + g - f)

Tactic:
simpa only [add_sub_cancel_left, sub_zero]

Premises used: sub_zero, add_sub_cancel_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ≈ f

Tactic:
have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 = f.norm

Tactic:
have h1 : (f + g).norm = f.norm := norm_equiv this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ g.norm = 0

Tactic:
have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw₂ rw₃ : f.norm = f.norm
⊢ (f + g).norm = max f.norm g.norm

Tactic:
rw [h1, h2, max_eq_left (norm_nonneg _)]

Premises used: PadicSeq.norm_nonneg, max_eq_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
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)))
⊢ 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))))

Tactic:
split_ifs at hfgne ⊢
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)))
v1 v2 :
  (hfgne :
      padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
        padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))) →
    ℕ
v1₁ v3 : ℕ
⊢ 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

Premises used: PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))))
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)))))
v1 v2 v1₁ v3 v2₁ v3₁ : ℕ
⊢ padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) =
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))

Tactic:
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]

Premises used: PadicSeq.lift_index_left_left, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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) : ℕ → ℚ) (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:
padicNorm.add_eq_max_of_ne hfgne

Premises used: padicNorm.add_eq_max_of_ne