awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
h₁ : LE.le (α := ℝ) 0 ((p : (a : R) → ℝ) (x ^ s (ψ 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₂ : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ)
Tactic: grw [map_pow_le_pow' hp x]
-- 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 : ℕ
h₁ : LE.le (α := ℝ) 0 ((p : (a : R) → ℝ) (x ^ s (ψ m)))
h₂ : 0 ≤ 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) : ℝ)
have 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) : ℝ)
Tactic: grw [map_pow_le_pow' hp x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (hypothesis)
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
ψ : ℕ → ℕ
⊢ IsBoundedUnder (α := ℝ) LE.le atTop fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
have 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) : ℝ))
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]
-- 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
ψ : ℕ → ℕ
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) : ℝ))
⊢ IsBoundedUnder (α := ℝ) LE.le atTop fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
have a : ∃ (b : ℝ),
  ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
Tactic: apply isBoundedUnder_of
-- 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
ψ : ℕ → ℕ
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 : ℝ)
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
have w : ℝ
Tactic: use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))
-- 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
ψ : ℕ → ℕ
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 : ℝ
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
have h : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ 1
Tactic: use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))
-- 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
ψ : ℕ → ℕ
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 : ℝ)
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
have h : ∀ (x_1 : ℕ),
  HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ (p : (a : R) → ℝ) x
Tactic: use p x
-- 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
ψ : ℕ → ℕ
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
have h : ∀ (m : ℕ), HDiv.hDiv (α := ℝ) (↑(s (ψ m)) : ℝ) (↑(ψ m) : ℝ) ≤ 1
Tactic: refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (hypothesis)
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) : ℝ))
⊢ ∃ (b : ℝ),
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) ((p : (a : R) → ℝ) (x ^ s (ψ x_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)) ≤ b
have x₁ : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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)
⊢ f = g
have 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
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 : 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)
⊢ { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : RingNorm R } = g
have 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 }
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
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 })
⊢ { 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 }
have mk : toRingSeminorm = toRingSeminorm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
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 })
⊢ toRingSeminorm = toRingSeminorm_1
have mk : ∀ (x : R), Eq (α := ℝ) ((toRingSeminorm : (a : R) → ℝ) x : ℝ) ((toRingSeminorm_1 : (a : R) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
f g : MulRingSeminorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : MulRingSeminorm R) ↦ f.toFun) f)
    ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toAddGroupSeminorm : AddGroupSeminorm R) (map_one' : toAddGroupSeminorm.toFun 1 = 1)
  (map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
  (h :
    Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
      ((fun (f : MulRingSeminorm R) ↦ f.toFun)
        { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)),
  { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm 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 : NonAssocRing R
g : MulRingSeminorm R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } = g
have mk : ∀ (toAddGroupSeminorm_1 : AddGroupSeminorm R) (map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1)
  (map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
        { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : MulRingSeminorm R) ↦ f.toFun)
        { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
  { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have inl : AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun.{u_1} (G := R) 1 0 * AddGroupSeminorm.toFun 1 y
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
inl : AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun.{u_1} (G := R) 1 0 * AddGroupSeminorm.toFun 1 y
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have inr : ∀ (hx : x ≠ 0), AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have inr : AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun.{u_1} (G := R) 1 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
hx : x ≠ 0
inr : AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun.{u_1} (G := R) 1 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
have inr₁ : ∀ (hy : y ≠ 0), AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
f g : MulRingNorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : MulRingNorm R) ↦ f.toFun) f)
    ((fun (f : MulRingNorm R) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toMulRingSeminorm : MulRingSeminorm R) (eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0)
  (h :
    Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
      ((fun (f : MulRingNorm R) ↦ f.toFun)
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
      ((fun (f : MulRingNorm R) ↦ f.toFun) g)),
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm 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 : NonAssocRing R
g : MulRingNorm R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun) g)
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } = g
have mk : ∀ (toMulRingSeminorm_1 : MulRingSeminorm R)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0)
  (h :
    Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
      ((fun (f : MulRingNorm R) ↦ f.toFun)
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
      ((fun (f : MulRingNorm R) ↦ f.toFun)
        { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })),
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_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 : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }
have mk : toMulRingSeminorm = toMulRingSeminorm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
⊢ toMulRingSeminorm = toMulRingSeminorm_1
have mk : ∀ (x : R), Eq (α := ℝ) ((toMulRingSeminorm : (a : R) → ℝ) x : ℝ) ((toMulRingSeminorm_1 : (a : R) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R_1 : Type u_1
inst : NonAssocRing R_1
inst_1 : DecidableEq R_1
inst_2 : NoZeroDivisors R_1
inst_3 : Nontrivial R_1
R : Type u_2
inst_4 : Ring R
inst_5 : Nontrivial R
v : AbsoluteValue R ℝ
⊢ (fun (N : MulRingNorm R) ↦
        { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ : AbsoluteValue R ℝ })
      ((fun (v : AbsoluteValue R ℝ) ↦
          { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
            eq_zero_of_map_eq_zero' := ⋯ : MulRingNorm R })
        v) =
    v
have a : ∀ (x : R),
  Eq (α := ℝ)
    (((fun (N : MulRingNorm R) ↦
              { toFun := N.toFun, map_mul' := sorry, nonneg' := sorry, eq_zero' := sorry, add_le' := sorry : AbsoluteValue R ℝ })
            ((fun (v : AbsoluteValue R ℝ) ↦
                { toFun := v.toFun, map_zero' := sorry, add_le' := sorry, neg' := sorry, map_one' := sorry, map_mul' := sorry,
                  eq_zero_of_map_eq_zero' := sorry : MulRingNorm R })
              v) :
          (a : R) → ℝ)
        x :
      ℝ)
    ((v : (a : R) → ℝ) x : ℝ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
⊢ x = 0
have obtain : ∀ (c : K) (hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)), x = 0
Tactic: obtain ⟨c, hc⟩ := RingSeminorm.ne_zero_iff.mp hnt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
⊢ x = 0
have by_contra : ∀ (hn0 : ¬x = 0), False
Tactic: by_contra hn0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
⊢ Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((f : (a : K) → ℝ) (x * (c * x⁻¹)) : ℝ) (0 : ℝ)
Tactic: rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]