mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e * ↑↑e.symm) x✝ = 1 x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e * ↑↑e.symm) x✝ = 1 x✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e.symm * ↑↑e) x✝ = 1 x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e.symm * ↑↑e) x✝ = 1 x✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
x✝ : H
⊢ (let __src := ↑(u * v);
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star (u * v)), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝ =
    ((let __src := ↑u;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) *
        let __src := ↑v;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star v), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
x✝ : H
⊢ (let __src := ↑(u * v);
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star (u * v)), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝ =
    ((let __src := ↑u;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) *
        let __src := ↑v;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star v), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Tactic:
;

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent k fun i ↦ (if ↑i = i₀ then s.centroid else s.points ↑i) -ᵥ if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x // x ≠ i₀ } :=
  have h := ⋯;
  fun x ↦ ⟨↑x, ⋯⟩
x y : ↥{i₀}ᶜ
hxy : f x = f y
⊢ x = y

Tactic:
;

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent k fun i ↦ (if ↑i = i₀ then s.centroid else s.points ↑i) -ᵥ if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x // x ≠ i₀ } :=
  have h := ⋯;
  fun x ↦ ⟨↑x, ⋯⟩
x y : ↥{i₀}ᶜ
hxy : f x = f y
⊢ x = y
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ s
⊢ p ∈ range fun p ↦ (lineMap q ↑p) ↑(w p)

Tactic:
;

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ s
⊢ p ∈ range fun p ↦ (lineMap q ↑p) ↑(w p)
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := ⋯
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := ⋯
p : P
hp : p ∈ s
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, ⋯⟩ = p

Tactic:
;

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := ⋯
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := ⋯
p : P
hp : p ∈ s
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, ⋯⟩ = p
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₄} ⊆ {p₄, p₅}

Tactic:
;

Goal state after:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₄} ⊆ {p₄, p₅}
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₃} ⊆ {p₃, p₄}

Tactic:
;

Goal state after:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₃} ⊆ {p₃, p₄}
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
;

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
i✝ : α
⊢ 0 ≤ ‖f i✝‖ ^ p.toReal

Tactic:
;

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
i✝ : α
⊢ 0 ≤ ‖f i✝‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
val✝ : Fintype α
⊢ Memℓp f p

Tactic:
;

Goal state after:
case inr.inr.intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
val✝ : Fintype α
⊢ Memℓp f p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
b✝ : α
⊢ 0 ≤ ‖(f + g) b✝‖ ^ p.toReal

Tactic:
;

Goal state after:
case inr.inr.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
b✝ : α
⊢ 0 ≤ ‖(f + g) b✝‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + -g) p

Tactic:
;

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + -g) p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
;

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n ↦ f n x₀
x : E
⊢ ∑' (n : α), f n x = 0 x

Tactic:
;

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n ↦ f n x₀
x : E
⊢ ∑' (n : α), f n x = 0 x
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x✝ : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x✝, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x✝) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x✝)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) 0 (l ×ˢ l) (𝓝 x✝) ∧
    TendstoUniformlyOnFilter (fun n x ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ f x.1.1 x✝ - f x.1.2 x✝ - (f x.1.1 x.2 - f x.1.2 x.2) + (f x.1.2 x✝ - f x.1.1 x✝) = -f x.1.1 x.2 + f x.1.2 x.2

Tactic:
;

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x✝ : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x✝, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x✝) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x✝)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) 0 (l ×ˢ l) (𝓝 x✝) ∧
    TendstoUniformlyOnFilter (fun n x ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ f x.1.1 x✝ - f x.1.2 x✝ - (f x.1.1 x.2 - f x.1.2 x.2) + (f x.1.2 x✝ - f x.1.1 x✝) = -f x.1.1 x.2 + f x.1.2 x.2
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h₁
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp✝ : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
hp : 0 < p.toReal
s : Finset α
i : α
a✝ : i ∈ s
⊢ ‖↑x i‖ ≤ ‖↑y i‖

Tactic:
;

Goal state after:
case h₁
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp✝ : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
hp : 0 < p.toReal
s : Finset α
i : α
a✝ : i ∈ s
⊢ ‖↑x i‖ ≤ ‖↑y i‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i ↦ ‖1 i‖) i ≤ 1

Tactic:
;

Goal state after:
I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i ↦ ‖1 i‖) i ≤ 1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
inst✝¹ : NormedRing 𝕜
inst✝ : DecidableEq α
i x✝ : α
⊢ ↑(zeroBasis i) x✝ = ↑(lp.single 0 i 1) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
α : Type u_3
inst✝¹ : NormedRing 𝕜
inst✝ : DecidableEq α
i x✝ : α
⊢ ↑(zeroBasis i) x✝ = ↑(lp.single 0 i 1) x✝
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
this : (fun x ↦ ∑' (i : α), f i x) = (fun x ↦ ∑ i ∈ T, f i x) + fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
hi : i ∉ T
x : E
hk : ↑k ≤ ↑m
⊢ ‖iteratedFDeriv 𝕜 k (f ↑⟨i, hi⟩) x‖ ≤ (v k ∘ Subtype.val) ⟨i, hi⟩

Tactic:
simp only [t, T, Finite.mem_toFinset, mem_ofPred_eq, Finset.mem_range, not_forall, not_le,
    exists_prop, not_exists, not_and, not_lt] at hi

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
this : (fun x ↦ ∑' (i : α), f i x) = (fun x ↦ ∑ i ∈ T, f i x) + fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
hi✝ : i ∉ T
x : E
hk : ↑k ≤ ↑m
hi : ∀ x < m + 1, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 x (f i) x_1‖ ≤ v x i
⊢ ‖iteratedFDeriv 𝕜 k (f ↑⟨i, hi✝⟩) x‖ ≤ (v k ∘ Subtype.val) ⟨i, hi✝⟩
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph).source =
    univ

Tactic:
;

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph).source =
    univ
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univUnitBall.trans' (unitBallBall c r hr) ⋯).target = ball c r

Tactic:
;

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univUnitBall.trans' (unitBallBall c r hr) ⋯).target = ball c r
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph)
      0 =
    c

Tactic:
;

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph)
      0 =
    c
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖↑f b‖ ^ p.toReal| < ε ^ p.toReal
H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal

Tactic:
rw [← H] at hs

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal
H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q✝ : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x✝² x✝¹ : ↥(lp E p)
x✝ : α
⊢ ↑⟨↑(x✝² + x✝¹), ⋯⟩ x✝ = ↑(⟨↑x✝², ⋯⟩ + ⟨↑x✝¹, ⋯⟩) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q✝ : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x✝² x✝¹ : ↥(lp E p)
x✝ : α
⊢ ↑⟨↑(x✝² + x✝¹), ⋯⟩ x✝ = ↑(⟨↑x✝², ⋯⟩ + ⟨↑x✝¹, ⋯⟩) x✝