awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ f (x * 1) ≤ f x * f 1

Tactic:
specialize hx 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
hx : f (x * 1) ≤ f x * f 1
⊢ 1 ≤ f 1

Tactic:
rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx

Premises used: le_mul_iff_one_le_right, Ne.symm, mul_one, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
hx : 1 ≤ f 1
⊢ 1 ≤ f 1

Tactic:
hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
hx : 1 ≤ f 1
⊢ 1 ≤ f 1

Tactic:
exact hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ f 1 = 1

Tactic:
have heq : f 1 = 1 := by
        apply h_one.antisymm
        specialize hx 1
        rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx
        exact hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
neg : f x = f (x * 1) / 1
neg₁ : f x = f x / 1
neg₂ neg₃ : f x = f x
⊢ f x = f (x * 1) / f 1

Tactic:
rw [heq, mul_one, div_one]

Premises used: mul_one, div_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
obtain : ∀ (x : R) (hx : f x ≠ 0 x), seminormFromBounded' f ≠ 0
⊢ seminormFromBounded' f ≠ 0

Tactic:
obtain ⟨x, hx⟩ := Function.ne_iff.mp f_ne_zero

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
rw : ∃ (a : R), seminormFromBounded' f a ≠ 0 a
⊢ seminormFromBounded' f ≠ 0

Tactic:
rw [Function.ne_iff]

Premises used: Function.ne_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
h : seminormFromBounded' f x ≠ 0 x
⊢ ∃ (a : R), seminormFromBounded' f a ≠ 0 a

Tactic:
use x
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
h : ¬f x = 0
⊢ seminormFromBounded' f x ≠ 0 x

Tactic:
rw [ne_eq, Pi.zero_apply, seminormFromBounded_eq_zero_iff f_nonneg f_mul x]

Premises used: Pi.zero_apply, seminormFromBounded_eq_zero_iff, ne_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ¬f x = 0

Tactic:
hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ¬f x = 0

Tactic:
exact hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h : ∀ (x : R), x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}
⊢ seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}

Tactic:
seminormFromBounded_eq_zero_iff f_nonneg f_mul x

Premises used: Set.Mem, setOf, seminormFromBounded_eq_zero_iff, Set.preimage, Set.singleton
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}

Tactic:
exact seminormFromBounded_eq_zero_iff f_nonneg f_mul x

Premises used: seminormFromBounded_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
⊢ (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}

Tactic:
⟨fun h0 ↦ ?_, fun h_ker x hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
refine_1 :
  ∀ (h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0), f ⁻¹' {0} = {0}
refine_2 :
  ∀ (h_ker : f ⁻¹' {0} = {0}) (x : R) (hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0), x = 0
⊢ (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}

Tactic:
refine ⟨fun h0 ↦ ?_, fun h_ker x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
refine_1 : seminormFromBounded' f ⁻¹' {0} = {0}
⊢ f ⁻¹' {0} = {0}

Tactic:
rw [← seminormFromBounded_ker f_nonneg f_mul]

Premises used: seminormFromBounded_ker
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
refine_1 : ∀ (x : R), x ∈ seminormFromBounded' f ⁻¹' {0} ↔ Membership.mem (γ := Set R) {0} x
⊢ seminormFromBounded' f ⁻¹' {0} = {0}

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
rw : seminormFromBounded' f 0 = 0
⊢ seminormFromBounded' f x = 0

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f 0 = 0

Tactic:
seminormFromBounded_zero f_zero

Premises used: seminormFromBounded_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f 0 = 0

Tactic:
exact seminormFromBounded_zero f_zero

Premises used: seminormFromBounded_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
⊢ seminormFromBounded' f x = 0 ↔ x = 0

Tactic:
exact ⟨fun h ↦ h0 x h, fun h ↦ by rw [h]; exact seminormFromBounded_zero f_zero⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h_ker : f ⁻¹' {0} = {0}
x : R
hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0
refine_2 : seminormFromBounded' f x = 0
⊢ x = 0

Tactic:
rw [← Set.mem_singleton_iff, ← h_ker, Set.mem_preimage, Set.mem_singleton_iff,
      ← seminormFromBounded_eq_zero_iff f_nonneg f_mul x]

Premises used: seminormFromBounded_eq_zero_iff, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h_ker : f ⁻¹' {0} = {0}
x : R
hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0
⊢ seminormFromBounded' f x = 0

Tactic:
hx

Premises used: iSup, seminormFromBounded'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h_ker : f ⁻¹' {0} = {0}
x : R
hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0
⊢ seminormFromBounded' f x = 0

Tactic:
exact hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
rw : seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y
⊢ seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
rw [seminormFromBounded_of_mul_apply f_nonneg f_mul hx]

Premises used: seminormFromBounded_of_mul_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y

Tactic:
simp only [seminormFromBounded', mul_assoc, hx, mul_div_assoc,
    Real.mul_iSup_of_nonneg (f_nonneg _)]

Premises used: mul_assoc, mul_div_assoc, seminormFromBounded', Real.mul_iSup_of_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ seminormFromConst_seq c f x = fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)

Tactic:
rfl

Premises used: seminormFromConst_seq, rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ 0 ≤ seminormFromConst_seq c f x

Tactic:
fun n ↦ div_nonneg (apply_nonneg f (x * c ^ n)) (pow_nonneg (apply_nonneg f c) n)

Premises used: HMul.hMul, pow_nonneg, HPow.hPow, div_nonneg, NonnegHomClass.apply_nonneg, seminormFromConst_seq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
h : 0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))
⊢ BddBelow (Set.range (seminormFromConst_seq c f x))

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
n : ℕ
⊢ 0 ≤ seminormFromConst_seq c f x n

Tactic:
seminormFromConst_seq_nonneg c f x n

Premises used: seminormFromConst_seq_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
n : ℕ
⊢ 0 ≤ seminormFromConst_seq c f x n

Tactic:
exact seminormFromConst_seq_nonneg c f x n

Premises used: seminormFromConst_seq_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
h :
  ∀ (n : ℕ),
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n))
    0

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
n : ℕ
h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
h₁ : 0 / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 0 n
h₂ : Eq (α := ℝ) 0 (0 n)
h₃ h₄ : Eq (α := ℝ) 0 0
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n

Tactic:
rw [zero_mul, hf, zero_div, Pi.zero_apply]

Premises used: MulZeroClass.zero_mul, zero_div, Pi.zero_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
rw₁ : HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (1 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1

Tactic:
rw [one_mul, hpm _ hn, div_self (pow_ne_zero n hc)]

Premises used: pow_ne_zero, one_mul, div_self
-- 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
nth_rw :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (m + (n - m))) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)

Tactic:
nth_rw 1 [← Nat.add_sub_of_le hmn]

Premises used: Nat.add_sub_of_le
-- 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
rw :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m * c ^ (n - m)) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (m + (n - m))) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)

Tactic:
rw [pow_add, ← mul_assoc]

Premises used: mul_assoc, pow_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 : R
m n : ℕ
hmn : m ≤ n
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)

Tactic:
have hc_pos : 0 < f c := lt_of_le_of_ne (apply_nonneg f _) hc.symm
-- 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 : ℝ)
apply :
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) ((f : (a : R) → ℝ) (c ^ (n - m)) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m * c ^ (n - m)) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)

Tactic:
apply le_trans ((div_le_div_iff_of_pos_right (pow_pos hc_pos _)).mpr (map_mul_le_mul f _ _))

Premises used: Iff.mpr, pow_pos, div_le_div_iff_of_pos_right, le_trans, 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
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
rw : n - n = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ n - m = 0

Tactic:
rw [heq, Nat.sub_self n]

Premises used: Nat.sub_self
-- 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 : ℝ)
heq : m = n
⊢ n - m = 0

Tactic:
have hnm : n - m = 0 := by rw [heq, Nat.sub_self 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 : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
hnm : n - m = 0
inl :
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    (f : (a : R) → ℝ) (x * c ^ n)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) ((f : (a : R) → ℝ) (c ^ (n - m)) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)

Tactic:
rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]

Premises used: pow_pos, div_le_div_iff_of_pos_right, pow_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 : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
hnm : n - m = 0
rw : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)
| (f : (a : R) → ℝ) (x * c ^ n)

Tactic:
rw [← mul_one (f (x * c ^ n))]

Premises used: HMul.hMul, HPow.hPow, mul_one, DFunLike.coe
-- 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 : ℝ)
heq : m = n
hnm : n - m = 0
inl :
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    (f : (a : R) → ℝ) (x * c ^ n)

Tactic:
conv_rhs => rw [← mul_one (f (x * c ^ n))]

Premises used: HMul.hMul, HPow.hPow, mul_one, DFunLike.coe
-- 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 : ℝ)
heq : m = n
hnm : n - m = 0
inl : LE.le (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)

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
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
hlt : m < n
rw : n - m ≠ 0
⊢ 1 ≤ n - m

Tactic:
rw [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_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 : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
hlt : m < n
⊢ n - m ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt hlt

Premises used: Nat.sub_ne_zero_of_lt
-- 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 : ℝ)
hlt : m < n
⊢ n - m ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hlt

Premises used: Nat.sub_ne_zero_of_lt
-- 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 : ℝ)
hlt : m < n
⊢ 1 ≤ n - m

Tactic:
have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt