mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ < ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : x ∈ {x | (fun x ↦ ‖f x‖ ≤ c * ‖g' x‖) x}
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
ι : Sort u_18
p : ι → Prop
s : ι → Set α
h✝ : f =O[l] g'
hb : l.HasBasis p s
c : ℝ
h : c > 0 ∧ IsBigOWith c l f g'
⊢ c > 0 ∧ ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hc : 0 < c
⊢ IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
inst✝ : Subsingleton E'
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖g' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[l] g₁ ↔ f₂ =o[l] g₂

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ (fun n ↦ f (-n)) =O[cofinite] fun n ↦ g (-n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ c * ‖g x‖ ≤ c * (c' * ‖k x‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : IsBigOWith c' l g k
hc : 0 ≤ c
⊢ IsBigOWith (c * c') l f k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : f =o[l] g
hgk : IsBigOWith c l g k
hc : 0 < c
⊢ f =o[l] k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
⊢ f =o[l] k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
⊢ ¬f' =o[l] f'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x ↦ ‖g' x‖) ↔ IsBigOWith c l f g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x ↦ ‖g' x‖) ↔ f =O[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x ↦ ‖g' x‖) ↔ f =o[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x ↦ ‖f' x‖) g ↔ IsBigOWith c l f' g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x ↦ -g' x) ↔ IsBigOWith c l f g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x ↦ -g' x) ↔ f =O[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x ↦ -g' x) ↔ f =o[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x ↦ -f' x) g ↔ IsBigOWith c l f' g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ -f' x) =O[l] g ↔ f' =O[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ -f' x) =o[l] g ↔ f' =o[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ (fun x ↦ (f' x).1) =O[l] f'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ (fun x ↦ (f' x).2) =O[l] f'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x ↦ f (a, x)) =O[l'] fun x ↦ g (a, x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun x ↦ f (x, b)) =O[l] fun x ↦ g (x, b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
⊢ IsBigOWith c l (fun x ↦ (f' x, g' x)) k'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
c : ℝ
f'' : α → E''
g'' : α → F''
l : Filter α
h : IsBigOWith c l f'' g''
x : α
hx : ‖f'' x‖ ≤ c * ‖g'' x‖
hg : g'' x = 0
⊢ ‖f'' x‖ ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x ↦ f₁ x + f₂ x) g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
⊢ Injective fun f ↦ ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖₊ = ‖x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖ₑ = ‖x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e✝ : E ≃ₛₗᵢ[σ₁₂] E₂
e : E ≃ₛₗ[σ₁₂] E₂
h₁ : ∀ (x : E), ‖e x‖ ≤ ‖x‖
h₂ : ∀ (y : E₂), ‖e.symm y‖ ≤ ‖y‖
x : E
⊢ ‖x‖ ≤ ‖e x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖₊ = ‖x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖ₑ = ‖x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e = univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
⊢ ⇑(ofSurjective f hfr) = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
⊢ ∀ (x : E × E₂), ‖(LinearEquiv.prodComm R E E₂) x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
by

Goal state after: