awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 + (↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1
have simp : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 - -(↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
  HMul.hMul (α := ℝ) 1 1
Tactic: simp only [← sub_neg_eq_add, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 - -(↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1
have hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
Tactic: have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n
have refine : IsBigO (E := R) (F := ℝ) (𝓝 0)
  (fun (i : R) ↦
    (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ -
      (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R))
  fun (t : R) ↦ ‖t‖ ^ n
Tactic: refine EventuallyEq.trans_isBigO (.fun_sub (inverse_add_nth_order x n) (.refl _ _)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0)
    (fun (i : R) ↦
      (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ -
        (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n
have simp : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (i : R) ↦ (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ) fun (t : R) ↦ ‖t‖ ^ n
Tactic: simp only [add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (i : R) ↦ (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ) fun (t : R) ↦ ‖t‖ ^ n
have refine : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ ‖(-(↑x⁻¹ : R) * x_1) ^ n‖ * 1) fun (t : R) ↦ ‖t‖ ^ n
Tactic: refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ ‖(-(↑x⁻¹ : R) * x_1) ^ n‖ * 1) fun (t : R) ↦ ‖t‖ ^ n
have simp : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (-(↑x⁻¹ : R) * x_1) ^ n) fun (t : R) ↦ ‖t‖ ^ n
Tactic: simp only [mul_one, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * t * (↑x⁻¹ : R))
    fun (t : R) ↦ HPow.hPow (β := ℕ) ‖t‖ 2
have h : ∀ (x_1 : R),
  ((↑x : R) + x_1)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * x_1 * (↑x⁻¹ : R) =
    ((↑x : R) + x_1)⁻¹ʳ - (∑ i ∈ range 2, (-(↑x⁻¹ : R) * x_1) ^ i) * (↑x⁻¹ : R)
Tactic: convert! inverse_add_norm_diff_nth_order x 2 using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ ContinuousAt inverse (↑x : R)
have h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
Tactic: have h_is_o : (fun t : R => (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
    (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (x_1 : R) ↦ ‖x_1 - (↑x : R)‖) (𝓝 (↑x : R)) (𝓝 0)
Tactic: refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
⊢ ContinuousAt inverse (↑x : R)
have h_lim : Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)
Tactic: have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) := by
    refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
    exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h_is_o : IsLittleO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (x : R) ↦ 1
h_lim : Tendsto (β := R) (fun (y : R) ↦ y - (↑x : R)) (𝓝 (↑x : R)) (𝓝 0)
⊢ ContinuousAt inverse (↑x : R)
have rw : Tendsto (β := ℝ) (fun (e : R) ↦ ‖e⁻¹ʳ - (↑x⁻¹ : R)‖) (𝓝 (↑x : R)) (𝓝 0)
Tactic: rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
⊢ I.closure ≠ ⊤
have h : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I : Set R) ⊆ nonunits R
Tactic: have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.WithAbs (hypothesis)
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : Semiring R
v : AbsoluteValue R S
inst_3 : SMul T R
inst_4 : FaithfulSMul T R
m₁ m₂ : T
h : ∀ (a : WithAbs v), m₁ • a = m₂ • a
⊢ m₁ = m₂
have h₁ : ∀ (a : WithAbs v), m₁ • a.ofAbs = m₂ • a.ofAbs
Tactic: simp only [smul_right_def, toAbs.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 f f' : AlgebraNorm R S
h : Eq (α := (a : S) → ℝ) (⇑f.toRingSeminorm : (a : S) → ℝ) (⇑f'.toRingSeminorm : (a : S) → ℝ)
⊢ f = f'
have mk : ∀ (toRingNorm : RingNorm S) (smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x)
  (h :
    Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
      (⇑f'.toRingSeminorm : (a : S) → ℝ)),
  { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = f'
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f f' : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
h :
  Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
    (⇑f'.toRingSeminorm : (a : S) → ℝ)
⊢ { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = f'
have mk : ∀ (toRingNorm_1 : RingNorm S) (smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x)
  (h :
    Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
      (⇑{ toRingNorm := toRingNorm_1, smul' := smul'_1 : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)),
  { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = { toRingNorm := toRingNorm_1, smul' := smul'_1 }
Tactic: cases f'
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h :
  Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
    (⇑{ toRingNorm := toRingNorm_1, smul' := smul'_1 : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
⊢ { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = { toRingNorm := toRingNorm_1, smul' := smul'_1 }
have mk : toRingNorm = toRingNorm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h : Eq (α := (a : S) → ℝ) (⇑toRingNorm.toRingSeminorm : (a : S) → ℝ) (⇑toRingNorm_1.toRingSeminorm : (a : S) → ℝ)
⊢ toRingNorm = toRingNorm_1
have mk : ∀ (s : S), Eq (α := ℝ) ((toRingNorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h : Eq (α := (a : S) → ℝ) (⇑toRingNorm.toRingSeminorm : (a : S) → ℝ) (⇑toRingNorm_1.toRingSeminorm : (a : S) → ℝ)
s : S
⊢ Eq (α := ℝ) ((toRingNorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)
have mk : Eq (α := ℝ) ((toRingNorm_1.toRingSeminorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)
Tactic: erw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
have rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = HMul.hMul (β := ℝ) ‖a‖ ((f : (a : S) → ℝ) 1 : ℝ)
Tactic: rw [← mul_one ‖a‖, ← hf1]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) ((algebraMap R S : (a : R) → S) a : S) = ‖a‖
have rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) (↑x : S) : ℝ) (0 : ℝ)
⊢ x = 0
have rw : (↑x : S) = 0
Tactic: rw [← ZeroMemClass.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x : A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ) (0 : ℝ)
⊢ x = 0
have rw : Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) (0 : S)
Tactic: rw [← map_eq_zero_iff (algebraMap A S) hinj]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
r : R
x : A
⊢ (f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) (r • x) : S) =
    HMul.hMul (β := ℝ) ‖r‖ ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)
have simp : (f : (a : S) → ℝ)
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap A S : (a : A) → S) x : S)) =
  HMul.hMul (β := ℝ) ‖r‖ ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)
Tactic: simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h :
  Eq.{max (u_2 + 1) 1} (α := (a : S) → ℝ) ((fun (f : MulAlgebraNorm R S) ↦ f.toFun) f)
    ((fun (f : MulAlgebraNorm R S) ↦ f.toFun) f')
⊢ f = f'
have h₁ : f.toMulRingSeminorm = f'.toMulRingSeminorm
Tactic: simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe, DFunLike.coe_fn_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h : f.toMulRingSeminorm = f'.toMulRingSeminorm
⊢ f = f'
have obtain : ∀ (toMulRingSeminorm : MulRingSeminorm S) (eq_zero_of_map_eq_zero' : ∀ (x : S), toMulRingSeminorm.toFun x = 0 → x = 0)
  (smul' :
    ∀ (a : R) (x : S),
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
              MulRingNorm S }.toFun
          (a • x) =
        ‖a‖ *
          { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
                MulRingNorm S }.toFun
            x)
  (h :
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
          MulAlgebraNorm R S }.toMulRingSeminorm =
      f'.toMulRingSeminorm),
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
      MulAlgebraNorm R S } =
    f'
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
f' : MulAlgebraNorm R S
toMulRingSeminorm : MulRingSeminorm S
eq_zero_of_map_eq_zero' : ∀ (x : S), toMulRingSeminorm.toFun x = 0 → x = 0
smul' :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm S }.toFun
        (a • x) =
      ‖a‖ *
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
              MulRingNorm S }.toFun
          x
h :
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
        MulAlgebraNorm R S }.toMulRingSeminorm =
    f'.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
      MulAlgebraNorm R S } =
    f'
have obtain : ∀ (toMulRingSeminorm_1 : MulRingSeminorm S)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : S), toMulRingSeminorm_1.toFun x = 0 → x = 0)
  (smul'_1 :
    ∀ (a : R) (x : S),
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
              MulRingNorm S }.toFun
          (a • x) =
        ‖a‖ *
          { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
                MulRingNorm S }.toFun
            x)
  (h :
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
          MulAlgebraNorm R S }.toMulRingSeminorm =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1,
          smul' := smul'_1 : MulAlgebraNorm R S }.toMulRingSeminorm),
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
      MulAlgebraNorm R S } =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1, smul' := smul'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f'
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
have rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * 1
Tactic: rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * 1
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
have rw₁ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * f.toFun 1
Tactic: rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * 1
rw₁ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * f.toFun 1
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
have rw₂ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = f.toFun (HSMul.hSMul (β := S) a 1)
Tactic: rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * 1
rw₁ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * f.toFun 1
rw₂ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = f.toFun (HSMul.hSMul (β := S) a 1)
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
have rw₃ : Eq (α := ℝ) ((f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) : ℝ) ((f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) : ℝ)
Tactic: rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ (f : (a : S) → ℝ) ((algebraMap R S : (a : R) → S) a : S) = ‖a‖
have rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
r : K
x : L
⊢ AddGroupSeminorm.toFun
      (MulRingSeminorm.toAddGroupSeminorm (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L))) (r • x) =
    ‖r‖ *
      AddGroupSeminorm.toFun
        (MulRingSeminorm.toAddGroupSeminorm (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L))) x
have simp : (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L) : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) r : L) =
    ‖r‖ ∨
  x = 0
Tactic: simp only [Algebra.smul_def, AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe,
      map_mul, mul_eq_mul_right_iff, map_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
⊢ (f : (a : A) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) n
have zero : ∀ (hn : LE.le (α := ℕ) 1 0),
  (f : (a : A) → ℝ) (HPow.hPow (β := ℕ) x 0) = HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : A) → ℝ) x : ℝ) 0
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
zero :
  ∀ (hn : LE.le (α := ℕ) 1 0),
    (f : (a : A) → ℝ) (HPow.hPow (β := ℕ) x 0) = HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : A) → ℝ) x : ℝ) 0
⊢ (f : (a : A) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) n
have succ : ∀ (n : ℕ) (hn : 1 ≤ n + 1), (f : (a : A) → ℝ) (x ^ (n + 1)) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (goal)
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n + 1
⊢ (f : (a : A) → ℝ) (x ^ (n + 1)) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)
have succ : HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)
Tactic: rw [map_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖
have simp : (sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
Tactic: simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
have a : (sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
a : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
⊢ (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
have a₁ : ‖x‖ ≤ sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖
have simp : (sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
Tactic: classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)