awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
⊢ ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑(c • f) : (a : α) → β)) ⋯
      (‖g‖ * ‖c • f‖) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
        (‖g‖ * ‖f‖) ⋯)
have h : ∀ (x : α),
  Eq.{w + 1} (α := γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑(c • f) : (a : α) → β)) sorry
            (‖g‖ * ‖c • f‖) sorry :
          (a : α) → γ)
        x :
      γ)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) sorry
              (‖g‖ * ‖f‖) sorry) :
          (a : α) → γ)
        x :
      γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ‖f + g‖ = max ‖f‖ ‖g‖
have hfg : ∀ (x : α),
  Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
Tactic: have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
x : α
⊢ norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
have inl : ∀ (h : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R)),
  norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
Tactic: obtain (h | h) := hfg x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
x : α
inl :
  ∀ (h : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R)),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
⊢ norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
have inr : ∀ (h : Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)),
  norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
Tactic: obtain (h | h) := hfg x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
⊢ ‖f + g‖ = max ‖f‖ ‖g‖
have hfg' : ∀ (x : α),
  norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
Tactic: have hfg' x : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
c : ℝ
hc : 0 ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
have simp_rw : (∀ (x : α), norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) ≤ c) ↔ max ‖f‖ ‖g‖ ≤ c
Tactic: simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
c : ℝ
hc : 0 ≤ c
simp_rw : (∀ (x : α), norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) ≤ c) ↔ max ‖f‖ ‖g‖ ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
have simp_rw₁ : (∀ (x : α), max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R)) ≤ c) ↔
  max ‖f‖ ‖g‖ ≤ c
Tactic: simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
c : ℝ
hc : 0 ≤ c
simp_rw : (∀ (x : α), norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) ≤ c) ↔ max ‖f‖ ‖g‖ ≤ c
simp_rw₁ :
  (∀ (x : α), max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R)) ≤ c) ↔
    max ‖f‖ ‖g‖ ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
have simp_rw₂ : (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c ∧ norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c) ↔
  ‖f‖ ≤ c ∧ ‖g‖ ≤ c
Tactic: simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
c : ℝ
hc : 0 ≤ c
simp_rw : (∀ (x : α), norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) ≤ c) ↔ max ‖f‖ ‖g‖ ≤ c
simp_rw₁ :
  (∀ (x : α), max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R)) ≤ c) ↔
    max ‖f‖ ‖g‖ ≤ c
simp_rw₂ :
  (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c ∧ norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c) ↔
    ‖f‖ ≤ c ∧ ‖g‖ ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
have simp_rw₃ : (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c ∧ norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c) ↔
  (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c) ∧
    ∀ (x : α), norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c
Tactic: simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
⊢ ‖f + g‖ = max ‖f‖ ‖g‖
have key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
Tactic: have key (c : ℝ) (hc : 0 ≤ c) : ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c := by
    simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
⊢ ‖f + g‖ ≤ max ‖f‖ ‖g‖
have hc : 0 ≤ max ‖f‖ ‖g‖
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
⊢ max ‖f‖ ‖g‖ ≤ ‖f + g‖
have hc : 0 ≤ ‖f + g‖
Tactic: rw [← key]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
h : Pairwise ((fun (x1 x2 : α →ᵇ R) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
have insert : f j * ∑ i ∈ s, f i = 0
Tactic: suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
s : Finset ι
h : Pairwise ((fun (x1 x2 : α →ᵇ R) ↦ x1 * x2 = 0) on f)
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : nnnorm (E := α →ᵇ R) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
s : Finset ι
h : Pairwise ((fun (x1 x2 : α →ᵇ R) ↦ x1 * x2 = 0) on f)
empty : nnnorm (E := α →ᵇ R) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
  nnnorm (E := α →ᵇ R) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
s : Finset ι
h : Pairwise ((fun (x1 x2 : α →ᵇ R) ↦ x1 * x2 = 0) on f)
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : nnnorm (E := α →ᵇ R) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
s : Finset ι
h : Pairwise ((fun (x1 x2 : α →ᵇ R) ↦ x1 * x2 = 0) on f)
empty : nnnorm (E := α →ᵇ R) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
  nnnorm (E := α →ᵇ R) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
⊢ (⇑(npowRec 0 f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
have rw : (⇑1 : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
rw : (⇑1 : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
⊢ (⇑(npowRec 0 f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
have rw₁ : Eq (α := (a : α) → R) (⇑1 : (a : α) → R) 1
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
rw : (⇑1 : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
rw₁ : Eq (α := (a : α) → R) (⇑1 : (a : α) → R) 1
⊢ (⇑(npowRec 0 f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0
have rw₂ : Eq (α := (a : α) → R) 1 1
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ (⇑(npowRec (n + 1) f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
have rw : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
Tactic: rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
n : ℕ
rw : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
⊢ (⇑(npowRec (n + 1) f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
have rw₁ : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
Tactic: rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
n : ℕ
rw : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
rw₁ : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
⊢ (⇑(npowRec (n + 1) f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
have rw₂ : HMul.hMul (α := (a : α) → R) (⇑(npowRec n f) : (a : α) → R) (⇑f : (a : α) → R) =
  HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
Tactic: rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
n : ℕ
rw : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
rw₁ : (⇑(npowRec n f * f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
rw₂ :
  HMul.hMul (α := (a : α) → R) (⇑(npowRec n f) : (a : α) → R) (⇑f : (a : α) → R) =
    HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
⊢ (⇑(npowRec (n + 1) f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) (n + 1)
have rw₃ : HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R) =
  HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑f : (a : α) → R)
Tactic: rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C
have obtain : ∀ (C₁ : ℝ) (hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁),
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C
Tactic: obtain ⟨C₁, hf⟩ := f.bounded
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C
have obtain : ∀ (C₂ : ℝ) (hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂),
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C
Tactic: obtain ⟨C₂, hg⟩ := g.bounded
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C
have refine : ∀ (x y : α),
  dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂
Tactic: refine ⟨C₁ + C₂, fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂
x y : α
⊢ dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂
have simp_rw : ∀ (hf : ∀ (x y : α), ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)‖ ≤ C₁)
  (hg : ∀ (x y : α), ‖HSub.hSub (α := β) (β := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β)‖ ≤ C₂),
  ‖HSub.hSub (α := β) (β := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
        (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β)‖ ≤
    C₁ + C₂
Tactic: simp_rw [dist_eq_norm_sub] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C
have obtain : ∀ (C₁ : ℝ) (hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁),
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C
Tactic: obtain ⟨C₁, hf⟩ := f.bounded
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C
have obtain : ∀ (C₂ : ℝ) (hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂),
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C
Tactic: obtain ⟨C₂, hg⟩ := g.bounded
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C
have refine : ∀ (x y : α),
  dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂
Tactic: refine ⟨C₁ + C₂, fun x y ↦ ?_⟩