awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have a : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
Tactic: rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
a : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have a₁ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
Tactic: rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
a : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
a₁ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have a₂ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
Tactic: rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
a : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
a₁ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
a₂ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have a₃ : Eq (α := ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
Tactic: rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
f g : RingSeminorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : RingSeminorm R) ↦ f.toFun) f)
    ((fun (f : RingSeminorm R) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toAddGroupSeminorm : AddGroupSeminorm R)
  (mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
  (h :
    Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
      ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
      ((fun (f : RingSeminorm R) ↦ f.toFun) g)),
  { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
g : RingSeminorm R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) g)
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } = g
have mk : ∀ (toAddGroupSeminorm_1 : AddGroupSeminorm R)
  (mul_le'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y)
  (h :
    Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
      ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
      ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })),
  { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 }
have mk : toAddGroupSeminorm = toAddGroupSeminorm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
⊢ toAddGroupSeminorm = toAddGroupSeminorm_1
have mk : ∀ (x : R), Eq (α := ℝ) ((toAddGroupSeminorm : (a : R) → ℝ) x : ℝ) ((toAddGroupSeminorm_1 : (a : R) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have pos : ∀ (h : x * y = 0), AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Tactic: by_cases h : x * y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
pos : ∀ (h : x * y = 0), AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have neg : ∀ (h : ¬x * y = 0), AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Tactic: by_cases h : x * y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have pos : 0 ≤ AddGroupSeminorm.toFun 1 x
Tactic: refine (if_pos h).trans_le (mul_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : 0 ≤ AddGroupSeminorm.toFun 1 x
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have pos₁ : 0 ≤ AddGroupSeminorm.toFun 1 y
Tactic: refine (if_pos h).trans_le (mul_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x
have pos : LE.le (α := ℝ) 0 (if x = 0 then 0 else 1)
Tactic: change _ ≤ ite _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ LE.le (α := ℝ) 0 (if x = 0 then 0 else 1)
have pos : x = 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : x = 0 → LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 (if x = 0 then 0 else 1)
have neg : ¬x = 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y
have pos : LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
Tactic: change _ ≤ ite _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
have pos : y = 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : y = 0 → LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
have neg : ¬y = 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have 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)
Tactic: change ite _ _ _ ≤ ite _ _ _ * ite _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)
have rw : Ne (α := ℝ) 1 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ) ↔ p ≠ 0
have h : ∀ (h : p ≠ 0), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: refine
    ⟨fun h => ne_zero_iff.mpr ⟨1, by rw [h]; exact one_ne_zero⟩,
      fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : Ring R
p : RingSeminorm R
hp : LE.le (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : p ≠ 0
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have inl : ∀ (hp0 : Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (0 : ℝ)), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: obtain hp0 | hp0 := (apply_nonneg p (1 : R)).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have inr : ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)), Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: obtain hp0 | hp0 := (apply_nonneg p (1 : R)).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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
have inl : ∀ (x : R), LE.le (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine h (ext fun x => (apply_nonneg _ _).antisymm' ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 : ℝ)
have inr : (p : (a : R) → ℝ) 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((p : (a : R) → ℝ) 1 : ℝ) ((p : (a : R) → ℝ) 1 : ℝ)
Tactic: refine hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑p : (a : R) → ℝ)
x y : R
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 : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨m, hm_lt, hm⟩ := IsNonarchimedean.add_pow_le hna n x y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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)) : ℝ)
⊢ 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 : ℝ)
have h : LE.le (α := ℝ) (0 : ℝ) ((p : (a : R) → ℝ) ((x + y) ^ n) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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) : ℝ)
⊢ 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 : ℝ)
have h₂ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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
⊢ (f : (a : α) → ℝ) (a ^ (n + 2)) ≤ HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 2)
have simp : (f : (a : α) → ℝ) (a ^ (n + 1) * a) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)
Tactic: simp only [pow_succ _ (n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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
⊢ (f : (a : α) → ℝ) (a ^ (n + 1) * a) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)
have grw : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) (a ^ (n + 1)) : ℝ) ((f : (a : α) → ℝ) 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 : ℝ)
⊢ (f : (a : α) → ℝ) (a ^ (n + 1) * a) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : α) → ℝ) a : ℝ) (n + 1)) ((f : (a : α) → ℝ) a : ℝ)
have 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 : ℝ)
Tactic: grw [map_mul_le_mul, map_pow_le_pow _ _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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) : ℝ))
have 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) : ℝ)
Tactic: rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 : ℝ) (s (ψ m)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)
have h₁ : LE.le (α := ℝ) 0 ((p : (a : R) → ℝ) (x ^ s (ψ m)))
Tactic: grw [map_pow_le_pow' hp x]