-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem uniformContinuous_coe [_i : Fact (1 ≤ p)] :
    UniformContinuous (α := lp E p) ((↑) : lp E p → ∀ i, E i)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ ∀ (i_1 : ℝ),
    0 < i_1 →
      ∃ j, 0 < j ∧ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < i_1}

Tactic:
intro ε hε

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∃ j, 0 < j ∧ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < ε}

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : ↥(lp E p)
hfg : ‖f - g‖ < ε
this : ‖↑f i - ↑g i‖ ≤ ‖f - g‖
⊢ (↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}

Tactic:
exact this.trans_lt hfg

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < ε} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < ε}

Tactic:
rintro f g (hfg : ‖f - g‖ < ε)

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : ↥(lp E p)
hfg : ‖f - g‖ < ε
⊢ (↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
⊢ UniformContinuous Subtype.val

Tactic:
have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ UniformContinuous Subtype.val

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ UniformContinuous Subtype.val

Tactic:
rw [uniformContinuous_pi]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ ∀ (i : α), UniformContinuous fun x => ↑x i

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ UniformContinuous fun x => ↑x i

Tactic:
rw [NormedAddCommGroup.uniformity_basis_dist.uniformContinuous_iff
  NormedAddCommGroup.uniformity_basis_dist]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ ∀ (i_1 : ℝ),
    0 < i_1 →
      ∃ j, 0 < j ∧ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < i_1}

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∃ j, 0 < j ∧ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < ε}

Tactic:
refine ⟨ε, hε, ?_⟩

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < ε} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < ε}

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : ↥(lp E p)
hfg : ‖f - g‖ < ε
⊢ (↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}

Tactic:
have : ‖f i - g i‖ ≤ ‖f - g‖ := norm_apply_le_norm hp (f - g) i

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : ↥(lp E p)
hfg : ‖f - g‖ < ε
this : ‖↑f i - ↑g i‖ ≤ ‖f - g‖
⊢ (↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ ∀ (i : α), UniformContinuous fun x => ↑x i

Tactic:
intro i

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ UniformContinuous fun x => ↑x i