awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h : norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3
h₁ : norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β)) < ε / 3
⊢ ‖HSub.hSub (α := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β))
        (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β))‖ <
    ε / 3 + ε / 3

Tactic:
refine (norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)

Premises used: norm_sub_le, add_lt_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3

Tactic:
((norm_tsum_le_tsum_norm (h_suma.subtype _)).trans ?_).trans_lt h1

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h :
  LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖f n (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))
⊢ norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3

Tactic:
refine ((norm_tsum_le_tsum_norm (h_suma.subtype _)).trans ?_).trans_lt h1

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖f n (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))

Tactic:
(h_suma.subtype _).tsum_le_tsum (h_bound ·) (h_sum.subtype _)

Premises used: Summable.subtype, Summable.tsum_le_tsum, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖f n (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))

Tactic:
exact (h_suma.subtype _).tsum_le_tsum (h_bound ·) (h_sum.subtype _)
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β)) < ε / 3

Tactic:
((norm_tsum_le_tsum_norm <| h_sumg.subtype _).trans ?_).trans_lt h1

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h :
  LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖g (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))
⊢ norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β)) < ε / 3

Tactic:
refine ((norm_tsum_le_tsum_norm <| h_sumg.subtype _).trans ?_).trans_lt h1

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖g (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))

Tactic:
(h_sumg.subtype _).tsum_le_tsum (h_g_le ·) (h_sum.subtype _)

Premises used: Summable.subtype, Summable.tsum_le_tsum, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖g (↑i : β)‖)
    (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))

Tactic:
exact (h_sumg.subtype _).tsum_le_tsum (h_g_le ·) (h_sum.subtype _)
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
⊢ ‖x * y‖ ≤ max ‖x‖ ‖y‖

Tactic:
simpa [le_max_iff, dist_eq_norm_inv_mul] using dist_triangle_max x⁻¹ 1 y

Premises used: IsUltrametricDist.dist_triangle_max, dist_eq_norm_inv_mul, Inv.inv, OfNat.ofNat, le_max_iff
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S' : Type u_2
inst : SeminormedGroup S'
h : ∀ (x y : S'), ‖x * y‖ ≤ max ‖x‖ ‖y‖
x y z : S'
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simpa [dist_eq_norm_inv_mul] using h (x⁻¹ * y) (y⁻¹ * z)

Premises used: HMul.hMul, dist_eq_norm_inv_mul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S' : Type u_4
inst : SeminormedAddGroup S'
h : IsNonarchimedean.{0, u_4} (α := S') norm
⊢ IsUltrametricDist S'

Tactic:
isUltrametricDist_of_forall_norm_add_le_max_norm h

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ dist 0 (x + y) ≤ max (dist 0 x) (dist x (x + y))

Tactic:
dist_triangle_max 0 x (x + y)

Premises used: IsUltrametricDist.dist_triangle_max, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
h : (fun (x : R) ↦ ‖x‖) (x + y) = dist 0 (x + y)
h₁ : max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))
⊢ LE.le (α := ℝ) ((fun (x : R) ↦ ‖x‖) (x + y)) (max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y))

Tactic:
convert! dist_triangle_max 0 x (x + y) using 1

Premises used: IsUltrametricDist.dist_triangle_max, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ (fun (x : R) ↦ ‖x‖) (x + y) = dist 0 (x + y)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
h : (fun (x : R) ↦ ‖x‖) x = dist 0 x
h₁ : (fun (x : R) ↦ ‖x‖) y = dist x (x + y)
⊢ max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ (fun (x : R) ↦ ‖x‖) x = dist 0 x

Tactic:
simp [SeminormedAddGroup.dist_eq]

Premises used: SeminormedAddGroup.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ (fun (x : R) ↦ ‖x‖) y = dist x (x + y)

Tactic:
simp [SeminormedAddGroup.dist_eq]

Premises used: SeminormedAddGroup.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
⊢ IsUltrametricDist R ↔ IsNonarchimedean (R := ℝ) fun (x : R) ↦ ‖x‖

Tactic:
⟨fun h => h.isNonarchimedean_norm, IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm⟩

Premises used: IsUltrametricDist.isNonarchimedean_norm, Iff.intro, IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
⊢ ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊

Tactic:
norm_mul_le_max _ _

Premises used: IsUltrametricDist.norm_mul_le_max
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S' : Type u_2
inst : SeminormedGroup S'
h : ∀ (x y : S'), ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊
⊢ IsUltrametricDist S'

Tactic:
isUltrametricDist_of_forall_norm_mul_le_max_norm h

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_mul_le_max_norm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S' : Type u_4
inst : SeminormedAddGroup S'
h : IsNonarchimedean.{0, u_4} (α := S') nnnorm
⊢ IsUltrametricDist S'

Tactic:
isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm h

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
⊢ IsNonarchimedean (R := ℝ) fun (x : R) ↦ (↑‖x‖₊ : ℝ)

Tactic:
simpa using isNonarchimedean_norm

Premises used: IsUltrametricDist.isNonarchimedean_norm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
⊢ IsUltrametricDist R ↔ IsNonarchimedean (R := ℝ) fun (x : R) ↦ (↑‖x‖₊ : ℝ)

Tactic:
⟨fun h => h.isNonarchimedean_norm, IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm⟩

Premises used: IsUltrametricDist.isNonarchimedean_norm, Iff.intro, IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ dist x⁻¹ 1 ≠ dist 1 y

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
rw : max (dist x⁻¹ 1) (dist 1 y) = max ‖x⁻¹⁻¹‖ ‖y‖
⊢ ‖x * y‖ = max ‖x‖ ‖y‖

Tactic:
rw [← inv_inv x, ← dist_eq_norm_inv_mul, dist_eq_max_of_dist_ne_dist _ 1 _ (by simp [h])]

Premises used: dist_eq_norm_inv_mul, inv_inv, IsUltrametricDist.dist_eq_max_of_dist_ne_dist, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ max (dist x⁻¹ 1) (dist 1 y) = max ‖x⁻¹⁻¹‖ ‖y‖

Tactic:
simp only [dist_one_right, dist_one_left, norm_inv']

Premises used: norm_inv', dist_one_left, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x * y‖ < max ‖x‖ ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
not_ne_iff.mp (h.ne ∘ norm_mul_eq_max_of_norm_ne_norm)

Premises used: Function.comp, IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm, not_ne_iff, Iff.mp, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x‖₊ ≠ ‖y‖₊
⊢ ‖x * y‖₊ = max ‖x‖₊ ‖y‖₊

Tactic:
simpa only [← NNReal.coe_inj, NNReal.coe_max] using
    norm_mul_eq_max_of_norm_ne_norm (NNReal.coe_injective.ne h)

Premises used: Function.Injective.ne, IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm, NNReal.coe_injective, NNReal.coe_inj, NNReal.coe_max
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x * y‖₊ < max ‖x‖₊ ‖y‖₊
⊢ ‖x‖₊ = ‖y‖₊

Tactic:
not_ne_iff.mp (h.ne ∘ nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm)

Premises used: Function.comp, not_ne_iff, Iff.mp, IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y z : S
h : ‖x / y‖ ≠ ‖y / z‖
⊢ ‖x / z‖ = max ‖x / y‖ ‖y / z‖

Tactic:
simpa only [div_mul_div_cancel] using norm_mul_eq_max_of_norm_ne_norm h

Premises used: IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm, div_mul_div_cancel
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y z : S
h : ‖x / y‖₊ ≠ ‖y / z‖₊
⊢ ‖x / z‖₊ = max ‖x / y‖₊ ‖y / z‖₊

Tactic:
simpa only [← NNReal.coe_inj, NNReal.coe_max] using
    norm_div_eq_max_of_norm_div_ne_norm_div _ _ _ (NNReal.coe_injective.ne h)

Premises used: Function.Injective.ne, IsUltrametricDist.norm_div_eq_max_of_norm_div_ne_norm_div, NNReal.coe_injective, NNReal.coe_inj, NNReal.coe_max
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
⊢ ‖HPow.hPow (β := ℕ) x 0‖₊ ≤ ‖x‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
n : ℕ
hn : ‖x ^ n‖₊ ≤ ‖x‖₊
⊢ ‖x ^ (n + 1)‖₊ ≤ ‖x‖₊

Tactic:
simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x

Premises used: pow_add, IsUltrametricDist.nnnorm_mul_le_max, HPow.hPow
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
n : ℕ
zero : ‖HPow.hPow (β := ℕ) x 0‖₊ ≤ ‖x‖₊
succ : ∀ (n : ℕ) (hn : ‖x ^ n‖₊ ≤ ‖x‖₊), ‖x ^ (n + 1)‖₊ ≤ ‖x‖₊
⊢ ‖x ^ n‖₊ ≤ ‖x‖₊

Tactic:
induction n with
  | zero => simp
  | succ n hn => simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x

Premises used: pow_add, IsUltrametricDist.nnnorm_mul_le_max, HPow.hPow
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
n : ℕ
⊢ ‖x ^ n‖ ≤ ‖x‖

Tactic:
nnnorm_pow_le x n

Premises used: IsUltrametricDist.nnnorm_pow_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
z : ℤ
ofNat : ∀ (a : ℕ), ‖x ^ Int.ofNat a‖₊ ≤ ‖x‖₊
negSucc : ∀ (a : ℕ), ‖x ^ Int.negSucc a‖₊ ≤ ‖x‖₊
⊢ ‖x ^ z‖₊ ≤ ‖x‖₊

Tactic:
cases z
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
a : ℕ
⊢ ‖x ^ Int.ofNat a‖₊ ≤ ‖x‖₊

Tactic:
simpa using nnnorm_pow_le _ _

Premises used: IsUltrametricDist.nnnorm_pow_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
a : ℕ
⊢ ‖x ^ Int.negSucc a‖₊ ≤ ‖x‖₊

Tactic:
simpa using nnnorm_pow_le _ _

Premises used: IsUltrametricDist.nnnorm_pow_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
z : ℤ
⊢ ‖x ^ z‖ ≤ ‖x‖

Tactic:
nnnorm_zpow_le x z

Premises used: IsUltrametricDist.nnnorm_zpow_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : Membership.mem (γ := Set S) (ball 1 r) x
hy : Membership.mem (γ := Set S) (ball 1 r) y
simp : ∀ (hx : ‖x‖ < r) (hy : ‖y‖ < r), ‖x * y‖ < r
⊢ Membership.mem (γ := Set S) (ball 1 r) (x * y)

Tactic:
simp only [Metric.mem_ball, dist_eq_norm_inv_mul', inv_one, one_mul] at hx hy ⊢

Premises used: inv_one, Metric.mem_ball, dist_eq_norm_inv_mul', one_mul
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : ‖x‖ < r
hy : ‖y‖ < r
⊢ ‖x * y‖ < r

Tactic:
(norm_mul_le_max x y).trans_lt (max_lt hx hy)

Premises used: max_lt, IsUltrametricDist.norm_mul_le_max, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : ‖x‖ < r
hy : ‖y‖ < r
⊢ ‖x * y‖ < r

Tactic:
exact (norm_mul_le_max x y).trans_lt (max_lt hx hy)

Premises used: max_lt, IsUltrametricDist.norm_mul_le_max, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
⊢ ∀ {x : S}, Membership.mem (γ := Set S) (ball 1 r) x → Membership.mem (γ := Set S) (ball 1 r) x⁻¹

Tactic:
simp only [Metric.mem_ball, dist_one_right, norm_inv', imp_self, implies_true]

Premises used: norm_inv', Metric.mem_ball, imp_self, implies_true, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : Membership.mem (γ := Set S) (closedBall 1 r) x
hy : Membership.mem (γ := Set S) (closedBall 1 r) y
simp : ∀ (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r), ‖x * y‖ ≤ r
⊢ Membership.mem (γ := Set S) (closedBall 1 r) (x * y)

Tactic:
simp only [Metric.mem_closedBall, dist_eq_norm_inv_mul', inv_one, one_mul] at hx hy ⊢

Premises used: inv_one, dist_eq_norm_inv_mul', Metric.mem_closedBall, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
⊢ ‖x * y‖ ≤ r

Tactic:
(norm_mul_le_max x y).trans (max_le hx hy)

Premises used: max_le, IsUltrametricDist.norm_mul_le_max, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
⊢ ‖x * y‖ ≤ r

Tactic:
exact (norm_mul_le_max x y).trans (max_le hx hy)

Premises used: max_le, IsUltrametricDist.norm_mul_le_max, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
⊢ ∀ {x : S}, Membership.mem (γ := Set S) (closedBall 1 r) x → Membership.mem (γ := Set S) (closedBall 1 r) x⁻¹

Tactic:
simp only [mem_closedBall, dist_one_right, norm_inv', imp_self, implies_true]

Premises used: norm_inv', imp_self, Metric.mem_closedBall, implies_true, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
⊢ ∀ (U : Set M), Membership.mem (γ := Filter M) (nhds 1) U → ∃ (V : OpenSubgroup M), (↑V : Set M) ⊆ U

Tactic:
simpa only [Metric.mem_nhds_iff]
    using fun U ⟨ε, hεp, hεU⟩ ↦ ⟨ball_openSubgroup M hεp, hεU⟩

Premises used: Metric.mem_nhds_iff