mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
⊢ ∀ s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots, r = s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : ↑{0}ᶜ
⊢ 0 < ‖↑x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree =
    (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots.prod

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : ↑{0}ᶜ
this : 0 < ‖↑x‖
⊢ r • ‖↑x‖⁻¹ • ↑x ∈ sphere 0 r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : ↑{0}ᶜ
this : 0 < ‖↑x‖
⊢ ‖↑x‖ / r ∈ Ioi 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ {0}ᶜ
⊢ 0 < ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ {0}ᶜ
⊢ (fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩)
      ((fun x ↦
          have this := ⋯;
          (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
        ⟨x, hx⟩) =
    ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
⊢ ↑f.symm ∘SL ↑f = ContinuousLinearMap.id R E

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
y : F
⊢ ⋯.leftInverse y = ⋯.leftInverse (f (f.symm y))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
⊢ ⋯.leftInverse = ↑f.symm

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
hf : f.IsInvertible
⊢ f.HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ sphere 0 r
d : ℝ
hd : d ∈ Ioi 0
⊢ (fun x ↦
        have this := ⋯;
        (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
      ((fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx⟩, ⟨d, hd⟩)) =
    (⟨x, hx⟩, ⟨d, hd⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasLeftInverse
hg : g.HasLeftInverse
⊢ (f.prodMap g).HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hg : g.HasLeftInverse
hf : f.HasLeftInverse
⊢ (g ∘SL f).HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hfg : (g ∘SL f).HasLeftInverse
⊢ f.HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (inl R F G).HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (inr R F G).HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Injective ⇑f
⊢ f.HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
⊢ ∀ (x : F), (f ∘SL hf.leftInverse) x ∈ (↑f).range

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
⊢ (↑f).range.ClosedComplemented

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun x ↦
    have this := ⋯;
    (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩)

Tactic:
simp only

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun x ↦ (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
⊢ spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / ↑(minpoly K x).natDegree)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed (range ⇑f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
hf'' : (↑f).range.ClosedComplemented
⊢ (↑f.rangeRestrict).ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
this : (↑f.rangeRestrict).ker = ⊥
p : F →L[R] ↥(↑f).range
hp : ∀ (x : ↥(↑f).range), p ↑x = x
x : E
⊢ f x ∈ (↑f).range

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
hf'' : (↑f).range.ClosedComplemented
⊢ f.HasLeftInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
⊢ ↑f ∘SL ↑f.symm = ContinuousLinearMap.id R F

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
y : F
⊢ f (⋯.rightInverse y) = f (↑f.symm y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
⊢ ⋯.rightInverse = ↑f.symm

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
hf : f.IsInvertible
⊢ f.HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasRightInverse
hg : g.HasRightInverse
⊢ (f.prodMap g).HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hg : g.HasRightInverse
hf : f.HasRightInverse
⊢ (g ∘SL f).HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
fginv : G →L[R] E
hfginv : RightInverse ⇑fginv ⇑(g ∘SL f)
y : G
⊢ g ((f ∘SL fginv) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hfg : (g ∘SL f).HasRightInverse
⊢ g.HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun x ↦
    have this := ⋯;
    (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (fst R F G).HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (snd R F G).HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Surjective ⇑f
⊢ f.HasRightInverse

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖↑(inclusionInDoubleDual 𝕜 E) x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : RCLike 𝕜
X : Type u_4
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (⇑(toWeakSpace 𝕜 X) ⁻¹' S)
hrange : closure (⇑(inclusionInDoubleDualWeak 𝕜 X) '' S) ⊆ Set.range ⇑(inclusionInDoubleDualWeak 𝕜 X)
⊢ IsCompact (closure S)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
this : ∀ {U : Set ℝ}, IsOpen U → 0 ∉ U → ∀ x ∈ U, 0 < x → U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)
hx₀ : ¬0 < x
⊢ 0 < -x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ (P * R) • x = (R * P * R) • x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Field

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : SeminormedCommRing E
inst✝¹ : NormMulClass E
inst✝ : NormOneClass E
f : α → E
x : E
hfx : HasProd f x
⊢ HasProd (fun x ↦ ‖f x‖) ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
⊢ P * R = R * P * R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P - Q * P * Q = P * (1 - Q) - (1 - Q) * P * (1 - Q)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P - Q * P * Q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P = Q * P * Q

Tactic:
by

Goal state after: