awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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
⊢ 0 ≤ ‖f + g‖

Tactic:
positivity
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖

Tactic:
exact le_antisymm (by rw [key]; positivity) (by rw [← key]; positivity)

Premises used: le_antisymm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊

Tactic:
NNReal.eq <| norm_add_eq_max h

Premises used: NNReal.eq, BoundedContinuousFunction.norm_add_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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 = 0

Tactic:
simpa
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖

Tactic:
simpa [sub_eq_add_neg] using norm_add_eq_max (f := f) (g := -g) (by simpa)

Premises used: sub_eq_add_neg, BoundedContinuousFunction.norm_add_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊

Tactic:
NNReal.eq <| norm_sub_eq_max h

Premises used: NNReal.eq, BoundedContinuousFunction.norm_sub_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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)
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
simpa [hj, ← ih] using nnnorm_add_eq_max this

Premises used: BoundedContinuousFunction.nnnorm_add_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
insert : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
i : ι
hi : i ∈ s
⊢ j ≠ i

Tactic:
grind
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
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.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = 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)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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‖₊
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.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm (E := α →ᵇ R) (∑ i ∈ s, f i) = 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)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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
rw₂ rw₃ : Eq (α := (a : α) → R) 1 1
⊢ (⇑(npowRec 0 f) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (β := ℕ) (⇑f : (a : α) → R) 0

Tactic:
rw [npowRec, pow_zero, coe_one]

Premises used: BoundedContinuousFunction.coe_one, npowRec, pow_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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)
rw₃ rw₄ :
  HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n * (⇑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)

Tactic:
rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]

Premises used: BoundedContinuousFunction.coe_mul, pow_succ, npowRec
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ∃ (C : ℝ), ∀ (x y : α), dist ((f.toContinuousMap ^ n).toFun x) ((f.toContinuousMap ^ n).toFun y) ≤ C

Tactic:
simpa [coe_npowRec] using (npowRec n f).map_bounded'

Premises used: npowRec, BoundedContinuousFunction.map_bounded', BoundedContinuousFunction.coe_npowRec
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
n : ℕ
⊢ Eq (α := (a : α) → R) (⇑(↑n : α →ᵇ R) : (a : α) → R) (↑n : (a : α) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq (α := (a : α) → R) (⇑(OfNat.ofNat n) : (a : α) → R) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : SeminormedRing R
n : ℤ
⊢ Eq (α := (a : α) → R) (⇑(↑n : α →ᵇ R) : (a : α) → R) (↑n : (a : α) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
γ : Type w
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : TopologicalSpace α
inst_2 : NormedRing γ
inst_3 : NormedAlgebra 𝕜 γ
k : 𝕜
a : α
⊢ (((algebraMap 𝕜 (α →ᵇ γ) : (a : 𝕜) → α →ᵇ γ) k : α →ᵇ γ) : (a : α) → γ) a = HSMul.hSMul (β := γ) k 1

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, coe_smul, coe_one, Pi.one_apply]

Premises used: BoundedContinuousFunction.coe_one, BoundedContinuousFunction.coe_smul, Pi.one_apply, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
γ : Type w
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : TopologicalSpace α
inst_2 : NormedRing γ
inst_3 : NormedAlgebra 𝕜 γ
f : α →ᵇ γ
⊢ Eq (α := (a : α) → γ) (⇑((toContinuousMapₐ 𝕜 : (a : α →ᵇ γ) → C(α, γ)) f : C(α, γ)) : (a : α) → γ) (⇑f : (a : α) → γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : TopologicalSpace α
inst_2 : NormedRing γ
inst_3 : NormedAlgebra 𝕜 γ
inst_4 : SeminormedAddCommGroup β
inst_5 : NormedSpace 𝕜 β
⊢ IsBoundedSMul (α →ᵇ 𝕜) (α →ᵇ β)

Tactic:
IsBoundedSMul.of_norm_smul_le fun _ _ =>
    norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _

Premises used: mul_nonneg, IsBoundedSMul.of_norm_smul_le, BoundedContinuousFunction.instSMul'._proof_2, norm_nonneg, BoundedContinuousFunction.norm_ofNormedAddCommGroup_le, BoundedContinuousFunction.instSMul'._proof_1
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
⊢ Injective (β := α → β) fun (f : α →ᵇ β) ↦ f.toFun

Tactic:
simp [Injective]

Premises used: Function.Injective
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
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
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
obtain ⟨C₁, hf⟩ := f.bounded

Premises used: BoundedContinuousFunction.bounded
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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₁
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
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
obtain ⟨C₂, hg⟩ := g.bounded

Premises used: BoundedContinuousFunction.bounded
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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

Tactic:
⟨C₁ + C₂, fun x y ↦ ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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₂
refine :
  ∀ (x y : α),
    dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
        (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
      C₁ + C₂
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
refine ⟨C₁ + C₂, fun x y ↦ ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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 : α
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₂
⊢ dist.{v} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂

Tactic:
simp_rw [dist_eq_norm_sub] at hf hg ⊢

Premises used: dist_eq_norm_sub
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
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:
(norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))

Premises used: add_le_add, norm_sup_sub_sup_le_add_norm, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
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:
exact (norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))

Premises used: add_le_add, norm_sup_sub_sup_le_add_norm, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
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
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
obtain ⟨C₁, hf⟩ := f.bounded

Premises used: BoundedContinuousFunction.bounded
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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₁
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
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
obtain ⟨C₂, hg⟩ := g.bounded

Premises used: BoundedContinuousFunction.bounded
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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

Tactic:
⟨C₁ + C₂, fun x y ↦ ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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₂
refine :
  ∀ (x y : α),
    dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
        (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
      C₁ + C₂
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
          (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
        C

Tactic:
refine ⟨C₁ + C₂, fun x y ↦ ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
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 : α
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₂
⊢ dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂

Tactic:
simp_rw [dist_eq_norm_sub] at hf hg ⊢

Premises used: dist_eq_norm_sub
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
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:
(norm_inf_sub_inf_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))

Premises used: add_le_add, LE.le.trans, norm_inf_sub_inf_le_add_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
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:
exact (norm_inf_sub_inf_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))

Premises used: add_le_add, LE.le.trans, norm_inf_sub_inf_le_add_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑|f| : (a : α) → β) |(⇑f : (a : α) → β)|

Tactic:
rfl

Premises used: abs, rfl