awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
⊢ m = n ∨ m < n

Tactic:
cases hmn.eq_or_lt with
  | inl heq =>
    have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
    rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
    conv_rhs => rw [← mul_one (f (x * c ^ n))]
    gcongr
  | inr hlt =>
    have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt
    rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]

Premises used: LE.le.eq_or_lt, pow_pos, HMul.hMul, mul_inv_cancel₀, mul_assoc, mul_div_assoc, pow_ne_zero, div_le_div_iff_of_pos_right, div_eq_mul_inv, pow_zero, Inv.inv, HPow.hPow, mul_comm, pow_sub₀, mul_one, DFunLike.coe, one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (seminormFromConst' c f x))

Tactic:
tendsto_atTop_ciInf (seminormFromConst_seq_antitone hf1 hc hpm x)
    (seminormFromConst_bddBelow c f x)

Premises used: seminormFromConst_seq_antitone, seminormFromConst', tendsto_atTop_ciInf, seminormFromConst_bddBelow
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
apply : seminormFromConst_seq c f 1 =ᶠ[atTop] fun (x : ℕ) ↦ 1
⊢ seminormFromConst' c f 1 = 1

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_seminormFromConst_seq_atTop hf1 hc hpm 1)
    tendsto_const_nhds

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, tendsto_seminormFromConst_seq_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1
⊢ seminormFromConst_seq c f 1 =ᶠ[atTop] fun (x : ℕ) ↦ 1

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1

Tactic:
⟨1, seminormFromConst_seq_one hc hpm⟩

Premises used: seminormFromConst_seq_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1

Tactic:
exact ⟨1, seminormFromConst_seq_one hc hpm⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ Tendsto (seminormFromConst_seq c f 0) atTop (𝓝 0)

Tactic:
simpa [seminormFromConst_seq_zero c (map_zero _)] using tendsto_const_nhds

Premises used: tendsto_const_nhds, map_zero, seminormFromConst_seq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
apply :
  ∀ (x_1 : ℕ), seminormFromConst_seq c f (x + y) x_1 ≤ seminormFromConst_seq c f x x_1 + seminormFromConst_seq c f y x_1
⊢ seminormFromConst' c f (x + y) ≤ seminormFromConst' c f x + seminormFromConst' c f y

Tactic:
apply le_of_tendsto_of_tendsto' (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x + y)) <|
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).add
        (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)

Premises used: HAdd.hAdd, Filter.Tendsto.add, le_of_tendsto_of_tendsto', tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)

Tactic:
simp only [add_mul, map_add_le_add f _ _]

Premises used: add_mul, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)

Tactic:
have h_add : f ((x + y) * c ^ n) ≤ f (x * c ^ n) + f (y * c ^ n) := by
      simp only [add_mul, map_add_le_add f _ _]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
h_add :
  (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
simp :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n + seminormFromConst_seq c f y n

Tactic:
simp only [seminormFromConst_seq, ← add_div]

Premises used: seminormFromConst_seq, add_div
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
h_add :
  (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
hc₁ : 0 ≤ HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
apply : seminormFromConst_seq c f (-x) =ᶠ[atTop] seminormFromConst_seq c f x
⊢ seminormFromConst' c f (-x) = seminormFromConst' c f x

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (-x))
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x)

Premises used: tendsto_nhds_unique_of_eventuallyEq, tendsto_seminormFromConst_seq_atTop, Neg.neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
simp : ∃ (a : ℕ), ∀ b ≥ a, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
⊢ seminormFromConst_seq c f (-x) =ᶠ[atTop] seminormFromConst_seq c f x

Tactic:
simp only [EventuallyEq, eventually_atTop]

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
h : ∀ b ≥ 0, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
⊢ ∃ (a : ℕ), ∀ b ≥ a, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ ∀ b ≥ 0, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b

Tactic:
simp only [seminormFromConst_seq, neg_mul, map_neg_eq_map, zero_le, implies_true]

Premises used: zero_le, AddGroupSeminormClass.map_neg_eq_map, neg_mul, implies_true, seminormFromConst_seq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
x_1 x_2 : ℕ
hnm : x_1 ≤ x_2
⊢ 2 * x_1 ≤ 2 * x_2

Tactic:
simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]

Premises used: Nat.succ_pos', mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ 2 * a
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))

Tactic:
apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
        (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by
          simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)

Premises used: HMul.hMul, Filter.tendsto_atTop_atTop_of_monotone, Filter.Tendsto.comp, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
h : n ≤ 2 * n
⊢ ∃ (a : ℕ), n ≤ 2 * a

Tactic:
use n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ n ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))

Tactic:
have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop
        (𝓝 (seminormFromConst' c f (x * y))) := by
      apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
        (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by
          simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)
      · rintro n; use n; lia
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
⊢ seminormFromConst' c f (x * y) ≤ seminormFromConst' c f x * seminormFromConst' c f y

Tactic:
le_of_tendsto_of_tendsto' hlim ((tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).mul
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)) (fun n ↦ ?_)

Premises used: Filter.Tendsto.mul, le_of_tendsto_of_tendsto', tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
refine :
  ∀ (n : ℕ), seminormFromConst_seq c f (x * y) (2 * n) ≤ seminormFromConst_seq c f x n * seminormFromConst_seq c f y n
⊢ seminormFromConst' c f (x * y) ≤ seminormFromConst' c f x * seminormFromConst' c f y

Tactic:
refine le_of_tendsto_of_tendsto' hlim ((tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).mul
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)) (fun n ↦ ?_)

Premises used: Filter.Tendsto.mul, le_of_tendsto_of_tendsto', tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
rw :
  (f : (a : R) → ℝ) (x * c ^ n * (y * c ^ n)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * y * c ^ (2 * n)) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (2 * n)) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) *
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)

Tactic:
rw [div_mul_div_comm, ← pow_add, two_mul,
      div_le_div_iff_of_pos_right (pow_pos (lt_of_le_of_ne (apply_nonneg f _) hc.symm) _), pow_add,
      ← mul_assoc, mul_comm (x * y), ← mul_assoc, mul_assoc, mul_comm (c ^ n)]

Premises used: pow_pos, HMul.hMul, div_mul_div_comm, mul_assoc, two_mul, pow_add, Ne.symm, div_le_div_iff_of_pos_right, HPow.hPow, mul_comm, NonnegHomClass.apply_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ (f : (a : R) → ℝ) (x * c ^ n * (y * c ^ n)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)

Tactic:
map_mul_le_mul f (x * c ^ n) (y * c ^ n)

Premises used: HMul.hMul, HPow.hPow, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ (f : (a : R) → ℝ) (x * c ^ n * (y * c ^ n)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)

Tactic:
exact map_mul_le_mul f (x * c ^ n) (y * c ^ n)

Premises used: HMul.hMul, HPow.hPow, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ (seminormFromConst hf1 hc hpm : (a : R) → ℝ) x = seminormFromConst' c f x

Tactic:
rfl

Premises used: iInf, seminormFromConst', rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ seminormFromConst' c f 1 ≤ 1

Tactic:
le_of_eq (seminormFromConst_one hf1 hc hpm)

Premises used: seminormFromConst_one, le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
apply :
  ∀ (x_1 : ℕ),
    seminormFromConst_seq c f (x + y) x_1 ≤ max (seminormFromConst_seq c f x x_1) (seminormFromConst_seq c f y x_1)
⊢ seminormFromConst' c f (x + y) ≤ max (seminormFromConst' c f x) (seminormFromConst' c f y)

Tactic:
apply le_of_tendsto_of_tendsto' (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x + y)) <|
    (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).max
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)

Premises used: Filter.Tendsto.max, HAdd.hAdd, le_of_tendsto_of_tendsto', tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ)
    (max ((f : (a : R) → ℝ) (x * c ^ n)) ((f : (a : R) → ℝ) (y * c ^ n)) : ℝ)

Tactic:
simp only [add_mul, hna _ _]

Premises used: add_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ)
    (max ((f : (a : R) → ℝ) (x * c ^ n)) ((f : (a : R) → ℝ) (y * c ^ n)) : ℝ)

Tactic:
have hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n)) := by
    simp only [add_mul, hna _ _]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ)
    (max ((f : (a : R) → ℝ) (x * c ^ n)) ((f : (a : R) → ℝ) (y * c ^ n)) : ℝ)
rw :
  ∀
    (hmax :
      LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
        LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)),
    seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ∨
      seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f y n
⊢ seminormFromConst_seq c f (x + y) n ≤ max (seminormFromConst_seq c f x n) (seminormFromConst_seq c f y n)

Tactic:
rw [le_max_iff] at hmax ⊢

Premises used: le_max_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
f₁ :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) →
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
g :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) →
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ∨
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)

Tactic:
apply hmax.imp

Premises used: Or.imp
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
h : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ)
f₁ : 0 ≤ HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)

Tactic:
gcongr