mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) ((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) f)) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
x✝ : (i : ι) → E i
⊢ ((↑((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯)
              ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l))).compMultilinearMap
        (tprod 𝕜))
      x✝ =
    ((↑l).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ (tprodL 𝕜).toMultilinearMap x✝ = (tprod 𝕜) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ g i ∘SL f i)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(mapL g ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
x✝ : (i : ι) → E i
⊢ ((↑((liftIsometry 𝕜 E' F) h ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ ContinuousLinearMap.id 𝕜 (E i))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsHomeomorph ⇑(quotientKerEquivRange f)

Tactic:
simp_rw [isHomeomorph_iff_isStrictMap_bijective, EquivLike.bijective, and_true,
    (isQuotientMap_mk _).isStrictMap_iff, IsEmbedding.subtypeVal.isStrictMap_iff]
  rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m₁✝ m₂✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (m₁✝ + m₂✝) n✝) x✝ = ↑(holder r B hBK m₁✝ n✝ + holder r B hBK m₂✝ n✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (c✝ • m✝) n✝) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m✝ : ↥(lp E p)
n₁✝ n₂✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (n₁✝ + n₂✝)) x✝ = ↑(holder r B hBK m✝ n₁✝ + holder r B hBK m✝ n₂✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (c✝ • n✝)) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝² : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ ∞)
hpqr : ∞.HolderTriple ∞ ∞
i : ι
⊢ ∞ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
s : Finset ι
⊢ ∞ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∞ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : Group α
inst✝ : GroupSeminormClass F α ℝ
f : F
x✝ : α
⊢ f (x✝⁻¹ * x✝) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
u_fred : u.IsFredholm
dom₁ : Submodule 𝕜 E
codom₀ : Submodule 𝕜 F
h_dom : IsTopCompl (↑u).ker dom₁
h_codom : IsTopCompl (↑u).range codom₀
⊢ u =
    { X₀ := codom₀, X₁ := (↑u).range, isTopCompl := h_codom, finite_X₀ := ⋯ }.X₁.subtypeL ∘SL
      ↑(((↑u).ker.quotientEquivOfIsTopCompl dom₁ h_dom).symm.trans (ContinuousLinearEquiv.quotKerEquivRange ⋯)) ∘SL
        { X₀ := (↑u).ker, X₁ := dom₁, isTopCompl := ⋯, finite_X₀ := ⋯ }.proj

Tactic:
refine LinearMap.ext_on_codisjoint h_dom.isCompl.codisjoint ?_ ?_
    · intro x (hx : u x = 0)
      simp [hx, projection_apply_of_mem_right]
    · intro x (hx : x ∈ dom₁)
      simp [hx, projection_apply_of_mem_left, ContinuousLinearEquiv.quotKerEquivRange]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteProd

Goal state before:
pp: case inl
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
f : α → β → R
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 n ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
by
  refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
  · grw [dist_self_sub_left, ← const_def, pi_norm_const_le]
    apply le_of_eq
    simp [abs_of_nonneg, hδ.le]
    ring
  obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
  refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
  rw [mem_closedBall, dist_eq_norm'] at hz
  rw [dist_eq_norm] at hxy
  replace hxy := (norm_le_pi_norm _ i).trans hxy.le
  replace hz := (norm_le_pi_norm _ i).trans hz
  dsimp at hxy hz
  rw [abs_sub_le_iff] at hxy hz
  linarith

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

Goal state before:
pp: case e_6
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x x✝ : V
⊢ (smulRight v (A x)) x✝ = (A * smulRight v x) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : V →L[𝕜] V) (x : V), T (A x) = (f A) (T x)
d : StrongDual 𝕜 W
hd : d ((f (smulRight v u)) z) = 1
w : W
⊢ T ((f.symm (smulRight d w)) u) = w

Tactic:
by simp [T, this, hd]

Goal state after:
Module: Mathlib.Analysis.ODE.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t
h : IsIntegralCurveOn γ v s
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y

Tactic:
obtain ⟨s', h₁, h₂, h₃⟩ := hs

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = ↑y ∘SL adjoint x ∘SL ↑y.symm
x : V →L[𝕜] V
⊢ adjoint (↑y ∘SL x ∘SL ↑y.symm ∘SL ↑y) = adjoint (↑y ∘SL x)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint ↑y ∘SL ↑y ∘SL adjoint x ∘SL ↑y.symm = adjoint x ∘SL adjoint ↑y
x : V →L[𝕜] V
⊢ adjoint ↑y ∘SL ↑y ∘SL x ∘SL ↑y.symm ∘SL ↑y = adjoint ↑y ∘SL ↑y ∘SL x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: case base
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n : ℕ
⊢ u n₀ ≤ u n₀ * ∏ i ∈ Ico n₀ n₀, c i + ∑ k ∈ Ico n₀ n₀, b k * ∏ i ∈ Ico (k + 1) n₀, c i

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ -(1 / 2) ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K ε x a : ℝ
⊢ HasDerivAt (fun y ↦ gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x

Tactic:
convert! (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1

Goal state after:
case e'_9
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
t₀ : ℝ
x₀ : E
⊢ picard f t₀ x₀ α t₀ = x₀

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_1.e'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ univ = -dt +ᵥ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
⊢ (next hf hx α).toFun t₀ = x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -t ∈ Ioc a b
⊢ LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))

Tactic:
← one_mul K

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -t ∈ Ioc a b
⊢ LipschitzOnWith (1 * K) (Neg.neg ∘ v (-t)) (s (-t))
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
this : EqOn f g (Neg.neg '' Icc (-b) (-a))
⊢ Icc a b = Neg.neg '' Icc (-b) (-a)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
t : ℝ
ht : t ∈ Ico (-b) (-a)
⊢ (Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t) = (ContinuousLinearMap.toSpanSingleton ℝ (v (-t) (f (-t)))) (-1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
t : ℝ
ht : t ∈ Ico (-b) (-a)
⊢ (Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t) = (ContinuousLinearMap.toSpanSingleton ℝ (v (-t) (g (-t)))) (-1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * ↑p.natDegree
⊢ 1 ≤ p.cauchyBound

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ eval x✝ P = ((fun x ↦ eval x (P.comp (-X))) ∘ Neg.neg) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
x✝ : 𝕜
⊢ |eval x✝ P| = ((fun x ↦ |eval x (P.comp (-X))|) ∘ Neg.neg) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : ‖a‖₊ < 1
⊢ 1 ≤ p.cauchyBound

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ 0 ≤ p.cauchyBound - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
    (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊

Tactic:
simp

Goal state after: