awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSeminormedRing α
x₁ x₂ : αᵐᵒᵖ
y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop

Premises used: dist_eq_norm, mul_sub, HSub.hSub, mul_comm, MulOpposite.unop, norm_mul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂

Tactic:
simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)

Premises used: dist_eq_norm, HSub.hSub, smul_sub
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0

Tactic:
simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b

Premises used: dist_eq_norm, HSub.hSub, sub_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ
⊢ ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simpa [enorm_eq_nnnorm, ← ENNReal.coe_mul, ENNReal.coe_le_coe] using h

Premises used: ENNReal.coe_le_coe, enorm_eq_nnnorm, ENNReal.coe_mul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊
⊢ IsBoundedSMul α β

Tactic:
.of_norm_smul_le h

Premises used: IsBoundedSMul.of_norm_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : Norm α
inst_1 : Norm β
inst_2 : SMul α β
inst_3 : NormSMulClass α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
NormSMulClass.norm_smul r x

Premises used: NormSMulClass.norm_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : ENorm α
inst_1 : ENorm β
inst_2 : SMul α β
inst_3 : ENormSMulClass α β
r : α
x : β
⊢ ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Tactic:
ENormSMulClass.enorm_smul r x

Premises used: ENormSMulClass.enorm_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddGroup β
inst_2 : SMul α β
inst_3 : NormSMulClass α β
r : α
x : β
⊢ ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊

Tactic:
NNReal.eq <| norm_smul r x

Premises used: norm_smul, NNReal.eq
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddGroup β
inst_2 : SMul α β
inst_3 : NormSMulClass α β
r : α
x : β
⊢ ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Tactic:
simp [enorm, nnnorm_smul]

Premises used: nnnorm_smul, ENorm.enorm
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β_1 : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddGroup β_1
inst_2 : SMul α β_1
inst_3 : NormSMulClass α β_1
ι : Type u_3
β : ι → Type u_4
inst_4 : Fintype ι
inst_5 : (i : ι) → SeminormedAddGroup (β i)
inst_6 : (i : ι) → SMul.{u_1, u_4} α (β i)
inst_7 : ∀ (i : ι), NormSMulClass.{u_1, u_4} α (β i)
r : α
x : (i : ι) → β i
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
simp [nnnorm_def, ← coe_nnnorm, nnnorm_smul, ← NNReal.coe_mul, NNReal.mul_finset_sup]

Premises used: nnnorm_smul, NNReal.mul_finset_sup, coe_nnnorm, Pi.nnnorm_def, NNReal.coe_mul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddGroup β
inst_2 : SMul α β
inst_3 : NormSMulClass α β
γ : Type u_3
inst_4 : SeminormedAddGroup γ
inst_5 : SMul α γ
inst_6 : NormSMulClass α γ
r : α
x : β × γ
v₁ : β
v₂ : γ
⊢ ‖r • (v₁, v₂)‖ = ‖r‖ * ‖(v₁, v₂)‖

Tactic:
simp only [smul_def, ← coe_nnnorm, nnnorm_def,
    nnnorm_smul r, ← NNReal.coe_mul, NNReal.mul_sup]

Premises used: nnnorm_smul, Prod.nnnorm_def, NNReal.mul_sup, Prod.smul_def, coe_nnnorm, NNReal.coe_mul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
x y : β
simp_rw : ‖s • x - s • y‖ = ‖s‖ * ‖x - y‖
simp_rw₁ : ‖s • x - s • y‖ = ‖s • (x - y)‖
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]

Premises used: dist_eq_norm, norm_smul, HSub.hSub, smul_sub, Eq.symm
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
x y : β
⊢ nndist (s • x) (s • y) = ‖s‖₊ * nndist x y

Tactic:
NNReal.eq <| dist_smul₀ s x y

Premises used: NNReal.eq, dist_smul₀
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y

Tactic:
simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]

Premises used: ENNReal.smul_def, nndist_smul₀, ENNReal.coe_mul, smul_eq_mul, edist_nndist
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
⊢ IsBoundedSMul α β

Tactic:
.of_norm_smul_le fun r x ↦ (norm_smul r x).le

Premises used: norm_smul, Eq.le, IsBoundedSMul.of_norm_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
pos : ∀ (h : r = 0), ‖r • x‖ = ‖r‖ * ‖x‖
neg : ∀ (h : ¬r = 0), ‖r • x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
by_cases h : r = 0
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
simp [h, zero_smul α x]

Premises used: zero_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
le_antisymm (norm_smul_le r x) ?_

Premises used: norm_smul_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
neg : ‖r‖ * ‖x‖ ≤ ‖r • x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
refine le_antisymm (norm_smul_le r x) ?_

Premises used: norm_smul_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
rw rw₁ : ‖r‖ * ‖x‖ = ‖r‖ * ‖x‖
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖

Tactic:
rw [inv_smul_smul₀ h]

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
hbc : ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖

Tactic:
apply norm_smul_le

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
rw : ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖
rw₁ : ‖r‖ * ‖r‖⁻¹ * ‖r • x‖ = ‖r • x‖
rw₂ : 1 * ‖r • x‖ = ‖r • x‖
rw₃ rw₄ : ‖r • x‖ = ‖r • x‖
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖

Tactic:
rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Premises used: norm_eq_zero, mul_inv_cancel₀, mul_assoc, mt, norm_inv, Iff.mp, one_mul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
r₁ : ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
r₂ : ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
r₃ : ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖

Tactic:
calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Premises used: Norm.norm, HMul.hMul, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
h : ∀ (p : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ s • x) '' ball x ε) p ↔ p ∈ ball (s • x) (‖s‖ * ε)
⊢ (fun (x : β) ↦ s • x) '' ball x ε = ball (s • x) (‖s‖ * ε)

Tactic:
ext p
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) → dist p (s • x) < ‖s‖ * ε
h₁ : dist p (s • x) < ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p
⊢ (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) ↔ dist p (s • x) < ‖s‖ * ε

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x < ε
⊢ dist (s • y) (s • x) < ‖s‖ * ε

Tactic:
simpa [dist_smul₀] using mul_lt_mul_of_pos_left h1 (norm_pos_iff.mpr hs)

Premises used: Iff.mpr, norm_pos_iff, mul_lt_mul_of_pos_left, dist_smul₀
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ s • s⁻¹ • p = p

Tactic:
simp [smul_smul, hs]

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : ∀ (h : dist p (s • x) < ‖s‖ * ε), dist (s⁻¹ • p) x < ε
⊢ dist p (s • x) < ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p

Tactic:
refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s⁻¹ • p) x < ε

Tactic:
lt_of_mul_lt_mul_of_nonneg_left ?_ (norm_nonneg s)

Premises used: lt_of_mul_lt_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
h₁ : ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε
⊢ dist (s⁻¹ • p) x < ε

Tactic:
refine lt_of_mul_lt_mul_of_nonneg_left ?_ (norm_nonneg s)

Premises used: lt_of_mul_lt_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
h₁ : dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε

Tactic:
rw [← dist_smul₀]

Premises used: dist_smul₀
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε

Tactic:
simpa [smul_smul, hs] using h

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
h :
  ∀ (p : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ s • x) '' closedBall x ε) p ↔ p ∈ closedBall (s • x) (‖s‖ * ε)
⊢ (fun (x : β) ↦ s • x) '' closedBall x ε = closedBall (s • x) (‖s‖ * ε)

Tactic:
ext p
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) → dist p (s • x) ≤ ‖s‖ * ε
h₁ : dist p (s • x) ≤ ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p
⊢ (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) ↔ dist p (s • x) ≤ ‖s‖ * ε

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x ≤ ε
⊢ dist (s • y) (s • x) ≤ ‖s‖ * ε

Tactic:
simpa [dist_smul₀] using mul_le_mul_of_nonneg_left h1 (norm_nonneg s)

Premises used: dist_smul₀, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ s • s⁻¹ • p = p

Tactic:
simp [smul_smul, hs]

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : ∀ (h : dist p (s • x) ≤ ‖s‖ * ε), dist (s⁻¹ • p) x ≤ ε
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p

Tactic:
refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist (s⁻¹ • p) x ≤ ε

Tactic:
le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)

Premises used: Iff.mpr, norm_pos_iff, le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
h₁ : ‖s‖ * dist (s⁻¹ • p) x ≤ ‖s‖ * ε
⊢ dist (s⁻¹ • p) x ≤ ε

Tactic:
refine le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)

Premises used: Iff.mpr, norm_pos_iff, le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
h₁ : dist (s • s⁻¹ • p) (s • x) ≤ ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x ≤ ‖s‖ * ε

Tactic:
rw [← dist_smul₀]

Premises used: dist_smul₀
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) ≤ ‖s‖ * ε

Tactic:
simpa [smul_smul, hs] using h

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
simp_rw : (fun (x : β) ↦ s • x) '' (closedBall x ε \ ball x ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
simp_rw₁ :
  (fun (x : β) ↦ s • x) '' closedBall x ε \ (fun (x : β) ↦ s • x) '' ball x ε =
    closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
simp_rw₂ :
  (fun (x : β) ↦ s • x) '' closedBall x ε \ ball (s • x) (‖s‖ * ε) =
    closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
⊢ (fun (x : β) ↦ s • x) '' sphere x ε = sphere (s • x) (‖s‖ * ε)

Tactic:
simp_rw [← Metric.closedBall_diff_ball, Set.image_diff (smul_right_injective β hs),
    smul_image_ball hs, smul_image_closedBall hs]

Premises used: Set.image_diff, smul_right_injective, Metric.smul_image_ball, Metric.closedBall_diff_ball, Metric.smul_image_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
l : Filter E
⊢ IsBigOWith.{u_4, u_5, u_4} (E := F) (F := E) ‖f‖ l (⇑f : (a : E) → F) fun (x : E) ↦ x

Tactic:
isBigOWith_of_le' _ f.le_opNorm

Premises used: ContinuousLinearMap.le_opNorm, Asymptotics.isBigOWith_of_le'
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
l : Filter E
⊢ IsBigO.{u_4, u_5, u_4} (E := F) (F := E) l (⇑f : (a : E) → F) fun (x : E) ↦ x

Tactic:
(f.isBigOWith_id l).isBigO

Premises used: ContinuousLinearMap.isBigOWith_id, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_6
inst : SeminormedAddCommGroup F
inst_1 : SeminormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_6 : RingHomIsometric σ₂₃
α : Type u_7
g : F →SL[σ₂₃] G
f : α → F
l : Filter α
⊢ IsBigOWith.{u_7, u_6, u_5} (E := G) ‖g‖ l (fun (x' : α) ↦ (g : (a : F) → G) (f x')) f

Tactic:
(g.isBigOWith_id ⊤).comp_tendsto le_top

Premises used: ContinuousLinearMap.isBigOWith_id, le_top, Asymptotics.IsBigOWith.comp_tendsto, Top.top
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_6
inst : SeminormedAddCommGroup F
inst_1 : SeminormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_6 : RingHomIsometric σ₂₃
α : Type u_7
g : F →SL[σ₂₃] G
f : α → F
l : Filter α
⊢ IsBigO.{u_7, u_6, u_5} (E := G) l (fun (x' : α) ↦ (g : (a : F) → G) (f x')) f

Tactic:
(g.isBigOWith_comp f l).isBigO

Premises used: ContinuousLinearMap.isBigOWith_comp, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
l : Filter E
x : E
⊢ IsBigOWith.{u_4, u_5, u_4} (E := F) (F := E) ‖f‖ l (fun (x' : E) ↦ (f : (a : E) → F) (x' - x)) fun (x' : E) ↦ x' - x

Tactic:
f.isBigOWith_comp _ l

Premises used: ContinuousLinearMap.isBigOWith_comp
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
l : Filter E
x : E
⊢ IsBigO.{u_4, u_5, u_4} (E := F) (F := E) l (fun (x' : E) ↦ (f : (a : E) → F) (x' - x)) fun (x' : E) ↦ x' - x

Tactic:
f.isBigO_comp _ l

Premises used: ContinuousLinearMap.isBigO_comp
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e : E ≃SL[σ₁₂] F
inst_8 : RingHomIsometric σ₁₂
α : Type u_7
f : α → E
l : Filter α
⊢ IsBigO.{u_7, u_5, u_4} (E := F) l (fun (x' : α) ↦ (e : (a : E) → F) (f x')) f

Tactic:
(e : E →SL[σ₁₂] F).isBigO_comp f l

Premises used: ContinuousLinearMap.isBigO_comp, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e : E ≃SL[σ₁₂] F
inst_8 : RingHomIsometric σ₁₂
l : Filter E
x : E
⊢ IsBigO.{u_4, u_5, u_4} (E := F) (F := E) l (fun (x' : E) ↦ (e : (a : E) → F) (x' - x)) fun (x' : E) ↦ x' - x

Tactic:
(e : E →SL[σ₁₂] F).isBigO_sub l x

Premises used: ContinuousLinearMap.isBigO_sub, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e : E ≃SL[σ₁₂] F
inst_8 : RingHomIsometric σ₂₁
α : Type u_7
f : α → E
l : Filter α
⊢ IsBigO.{u_7, u_4, u_5} (F := F) l f fun (x' : α) ↦ (e : (a : E) → F) (f x')

Tactic:
(e.symm.isBigO_comp _ l).congr_left fun _ => e.symm_apply_apply _

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.isBigO_comp, Asymptotics.IsBigO.congr_left, ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.Normed.Operator.Asymptotics
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e : E ≃SL[σ₁₂] F
inst_8 : RingHomIsometric σ₂₁
l : Filter E
x : E
⊢ IsBigO.{u_4, u_4, u_5} (E := E) (F := F) l (fun (x' : E) ↦ x' - x) fun (x' : E) ↦ (e : (a : E) → F) (x' - x)

Tactic:
e.isBigO_comp_rev _ _

Premises used: ContinuousLinearEquiv.isBigO_comp_rev
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
fsymm : f.NonlinearRightInverse
y : F
⊢ (f : (a : E) → F) (fsymm.toFun y) = y

Tactic:
fsymm.right_inv' y

Premises used: ContinuousLinearMap.NonlinearRightInverse.right_inv'