awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : ¬x * y = 0
neg : (if x * y = 0 then 0 else 1) ≤ HMul.hMul (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
change ite _ _ _ ≤ ite _ _ _ * ite _ _ _

Premises used: ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ (if x * y = 0 then 0 else 1) ≤ HMul.hMul (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
simp only [if_false, h, left_ne_zero_of_mul h, right_ne_zero_of_mul h, mul_one,
            le_refl]

Premises used: le_refl, if_false, right_ne_zero_of_mul, left_ne_zero_of_mul, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x : R
⊢ Eq (α := ℝ) ((1 : (a : R) → ℝ) x : ℝ) (if x = 0 then 0 else 1 : ℝ)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
rw : Ne (α := ℝ) 1 0
⊢ Ne (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Ne (α := ℝ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Ne (α := ℝ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : ∀ (h : p ≠ 0), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ) ↔ p ≠ 0

Tactic:
refine
    ⟨fun h => ne_zero_iff.mpr ⟨1, by rw [h]; exact one_ne_zero⟩,
      fun h => ?_⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
inl : ∀ (hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
inr : ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
obtain hp0 | hp0 := (apply_nonneg p (1 : R)).eq_or_lt'

Premises used: NonnegHomClass.apply_nonneg, OfNat.ofNat, LE.le.eq_or_lt'
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)
inl : False
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
exfalso
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ False

Tactic:
h (ext fun x => (apply_nonneg _ _).antisymm' ?_)

Premises used: LE.le.antisymm', RingSeminorm.ext, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)
inl : ∀ (x : R), LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ False

Tactic:
refine h (ext fun x => (apply_nonneg _ _).antisymm' ?_)

Premises used: LE.le.antisymm', RingSeminorm.ext, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)
x : R
⊢ LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simpa only [hp0, mul_one, mul_zero] using map_mul_le_mul p x 1

Premises used: MulZeroClass.mul_zero, mul_one, OfNat.ofNat, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)

Premises used: LE.le.antisymm, le_mul_iff_one_le_left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)
inr : (p : (a : R) → ℝ) 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
refine hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)

Premises used: LE.le.antisymm, le_mul_iff_one_le_left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)
⊢ (p : (a : R) → ℝ) 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)

Tactic:
simpa only [one_mul] using map_mul_le_mul p (1 : R) _

Premises used: OfNat.ofNat, one_mul, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑p : (a : R) → ℝ)
x y : R
n : ℕ
obtain :
  ∀ (m : ℕ) (hm_lt : m < n + 1)
    (hm :
      (p : (a : R) → ℝ) ((x + y) ^ n) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ)),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ ∃ m < n + 1,
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
        HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
obtain ⟨m, hm_lt, hm⟩ := IsNonarchimedean.add_pow_le hna n x y

Premises used: IsNonarchimedean.add_pow_le
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑p : (a : R) → ℝ)
x y : R
n m : ℕ
hm_lt : m < n + 1
hm :
  (p : (a : R) → ℝ) ((x + y) ^ n) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ)
h : LE.le (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ)
h₂ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑p : (a : R) → ℝ)
x y : R
n m : ℕ
hm_lt : m < n + 1
hm :
  (p : (a : R) → ℝ) ((x + y) ^ n) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ)
⊢ ∃ m < n + 1,
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) (x ^ m) : ℝ) ((p : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
        HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact ⟨m, hm_lt, by gcongr⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
F : Type u_2
α : Type u_3
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f : F
a : α
h : Ne (α := ℕ) 1 0
⊢ (f : (a : α) → ℝ) (HPow.hPow (β := ℕ) a 1) ≤ HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : α) → ℝ) a : ℝ) 1

Tactic:
simp only [pow_one, le_refl]

Premises used: le_refl, pow_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
F : Type u_2
α : Type u_3
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
h : n + 2 ≠ 0
simp :
  (f : (a : α) → ℝ) (a ^ (n + 1) * a) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)
⊢ (f : (a : α) → ℝ) (a ^ (n + 2)) ≤ HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 2)

Tactic:
simp only [pow_succ _ (n + 1)]

Premises used: pow_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
F : Type u_2
α : Type u_3
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
h : n + 2 ≠ 0
grw :
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) (a ^ (n + 1)) : ℝ) ((f : (a : α) → ℝ) a : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)
grw₁ grw₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) n.succ) ((f : (a : α) → ℝ) a : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) n.succ) ((f : (a : α) → ℝ) a : ℝ)
⊢ (f : (a : α) → ℝ) (a ^ (n + 1) * a) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)

Tactic:
grw [map_mul_le_mul, map_pow_le_pow _ _ n.succ_ne_zero]

Premises used: Nat.succ_ne_zero, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
F : Type u_2
α : Type u_3
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f : F
hf1 : LE.le (α := ℝ) ((f : (a : α) → ℝ) 1 : ℝ) (1 : ℝ)
a : α
⊢ (f : (a : α) → ℝ) (HPow.hPow (β := ℕ) a 0) ≤ HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : α) → ℝ) a : ℝ) 0

Tactic:
simp only [pow_zero, hf1]

Premises used: pow_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
rw :
  HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (s (ψ m)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)
⊢ HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))

Tactic:
rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]

Premises used: Nat.cast, mul_one_div, NonnegHomClass.apply_nonneg, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
h₁ : LE.le (α := ℝ) 0 ((p : (a : R) → ℝ) (x ^ s (ψ m)))
h₂ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)
grw grw₁ :
  HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (s (ψ m)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ) ≤
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (s (ψ m)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)
⊢ HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (s (ψ m)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)

Tactic:
grw [map_pow_le_pow' hp x]

Premises used: map_pow_le_pow'
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))

Tactic:
have h_le : ∀ m : ℕ, p (x ^ s (ψ m)) ^ (1 / (ψ m : ℝ)) ≤ p x ^ ((s (ψ m) : ℝ) / (ψ m : ℝ)) := by
    intro m
    rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]
    grw [map_pow_le_pow' hp x]
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
a :
  ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
⊢ IsBoundedUnder (α := ℝ) LE.le atTop fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
apply isBoundedUnder_of

Premises used: Filter.isBoundedUnder_of
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (1 : ℝ)
m : ℕ
⊢ LE.le (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) x : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (1 : ℝ)
m : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (1 : ℝ)
w : ℝ
h : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ 1
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b

Tactic:
use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))

Premises used: Real.rpow_le_one, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)
h :
  ∀ (x_1 : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤
      (p : (a : R) → ℝ) x
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b

Tactic:
use p x

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)
⊢ ∀ (x_1 : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤
      (p : (a : R) → ℝ) x

Tactic:
fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_

Premises used: Real.rpow_le_self_of_one_le, LT.lt.le, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)
h : ∀ (m : ℕ), HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ) ≤ 1
⊢ ∀ (x_1 : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤
      (p : (a : R) → ℝ) x

Tactic:
refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_

Premises used: Real.rpow_le_self_of_one_le, LT.lt.le, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)
m : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ) ≤ 1

Tactic:
div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

Premises used: div_le_one_of_le₀, Nat.cast_nonneg, cast, Nat.cast_le._simp_1, Eq.symm
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
hfx : LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)
m : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ) ≤ 1

Tactic:
exact div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le :
  ∀ (m : ℕ),
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)) ≤
      HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ))
⊢ LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (1 : ℝ) ∨ LT.lt (α := ℝ) (1 : ℝ) ((p : (a : R) → ℝ) x : ℝ)

Tactic:
cases le_or_gt (p x) 1 with
  | inl hfx =>
    use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))
  | inr hfx =>
    use p x
    refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_
    exact div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

Premises used: div_le_one_of_le₀, le_or_gt, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
f g : RingNorm R
h : Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : RingNorm R) ↦ f.toFun) f) ((fun (f : RingNorm R) ↦ f.toFun) g)
mk :
  ∀ (toRingSeminorm : RingSeminorm R) (eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : RingNorm R) ↦ f.toFun)
          { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : RingNorm R) ↦ f.toFun) g)),
    { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : RingNorm R } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
g : RingNorm R
toRingSeminorm : RingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : RingNorm R) ↦ f.toFun) g)
mk :
  ∀ (toRingSeminorm_1 : RingSeminorm R) (eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : RingNorm R) ↦ f.toFun)
          { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : RingNorm R) ↦ f.toFun)
          { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })),
    { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : RingNorm R } =
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }
⊢ { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : RingNorm R } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toRingSeminorm : RingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0
toRingSeminorm_1 : RingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
mk : toRingSeminorm = toRingSeminorm_1
⊢ { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : RingNorm R } =
    { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toRingSeminorm : RingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0
toRingSeminorm_1 : RingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
mk : ∀ (x : R), Eq (α := ℝ) ((toRingSeminorm : (a : R) → ℝ) x : ℝ) ((toRingSeminorm_1 : (a : R) → ℝ) x : ℝ)
⊢ toRingSeminorm = toRingSeminorm_1

Tactic:
ext x