mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ Collinear k {p₁, p₃, p₂, p}

Tactic:
apply collinear_insert_insert_of_mem_affineSpan_pair

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
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₁ ∈ line[k, p₂, p]

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
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₃ ∈ line[k, p₂, p]
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
s : AffineSubspace k P
p : P
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
by
  by_cases hf : FiniteDimensional k s.direction; swap
  · have hf' : ¬FiniteDimensional k (vectorSpan k (insert p (s : Set P))) := by
      intro h
      have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)
      exact hf (Submodule.finiteDimensional_of_le h')
    rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]
    exact zero_le_one
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
  rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
  · rw [coe_eq_bot_iff] at hs
    rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot,
      zero_add]
    convert! zero_le_one' ℕ
    rw [← finrank_bot k V]
    convert! rfl <;> simp
  · rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]
    refine (Submodule.finrank_add_le_finrank_add_finrank _ _).trans ?_
    gcongr
    refine finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_
    have h := v.property
    rw [Submodule.mem_span_singleton] at h
    rcases h with ⟨c, hc⟩
    refine ⟨c, ?_⟩
    ext
    exact hc

Goal state after:
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:
by intro; positivity

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ ∀ i ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0

Tactic:
intro i

Goal state after:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
⊢ i ∉ ⋯.toFinset → ‖f i‖ ^ p.toReal = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ ∀ (i : α), ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖

Tactic:
intro i

Goal state after:
case inr.inr.inr.inr.inr.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
i : α
⊢ ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p) →
        (∀ i ∈ insert a s, Memℓp (f i) p) → Memℓp (fun a_3 ↦ ∑ i ∈ insert a s, f i a_3) p

Tactic:
intro i

Goal state after:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
⊢ ∀ (s : Finset ι),
    i ∉ s →
      ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p) →
        (∀ i_1 ∈ insert i s, Memℓp (f i_1) p) → Memℓp (fun a ↦ ∑ i ∈ insert i s, f i a) p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
⊢ ∀ (b : α), ‖c • f b‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f b‖₊) ^ p.toReal

Tactic:
intro i

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
i : α
⊢ ‖c • f i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f i‖₊) ^ 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)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (∑' (i : α), ‖↑f i‖ ^ p.toReal)

Tactic:
exact ((lp.memℓp f).summable hp).hasSum

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

Goal state before:
pp: case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : IsEmpty α
⊢ f = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ∀ (i : α), ‖↑(f + g) i‖ ^ p.toReal ≤ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal

Tactic:
intro i

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
i : α
⊢ ‖↑(f + g) i‖ ^ p.toReal ≤ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case succ
α : 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 : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fun x ↦
      ∑' (n : α), fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 k (f n) x) x) =
    fun x ↦
    ∑' (n : α), (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x

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 : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ ∀ (n : α) (x : E), ‖fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 k (f n) x) x‖ ≤ v (k + 1) n

Tactic:
· ext1 x
      exact (continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum

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 : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ ∀ (n : α) (x : E), ‖fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 k (f n) x) x‖ ≤ v (k + 1) n
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case left.refine_1
α : 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 : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ ∀ (i : α), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))

Tactic:
intro i

Goal state after:
case left.refine_1
α : 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 : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
i : α
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))
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}
⊢ ∀ i ∈ Finset.range (m + 1), ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x

Tactic:
intro i

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}
i : ℕ
⊢ i ∈ Finset.range (m + 1) → ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x
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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
i : α
hi : i ∉ s
⊢ ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0

Tactic:
by
    simp [if_neg hi, Real.zero_rpow hp.ne']

Goal state after:
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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
⊢ ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal

Tactic:
intro i

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
i : α
⊢ i ∈ s → ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ 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)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
⊢ ∀ i ∉ s, F i = 0

Tactic:
intro i

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
i : α
⊢ i ∉ s → F i = 0
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
⊢ ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal

Tactic:
intro i

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
i : α
⊢ i ∈ s → F i = ‖↑f i‖ ^ p.toReal
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.left
ι : 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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε

Tactic:
refine lt_of_le_of_lt mvt ?_

Goal state after:
case inr.left
ι : 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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
⊢ q * ‖y - 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩

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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case mpr.hCf
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∀ (i : ι), ‖↑(f x - f y) i‖ ≤ ↑K * dist x y

Tactic:
intro i

Goal state after:
case mpr.hCf
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
i : ι
⊢ ‖↑(f x - f y) i‖ ≤ ↑K * dist x y
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case e'_9
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt (((fun x ↦ Polynomial.eval x p) * fun x ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x =
    (Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹

Tactic:
simp [expNegInvGlue, hx.not_ge]
      ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: n : ℕ∞
⊢ ContDiff ℝ (↑n) expNegInvGlue

Tactic:
by
  simpa using contDiff_polynomial_eval_inv_mul 1

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : x ∉ support g + support f
⊢ (f ⋆[L, μ] g) x = 0

Tactic:
simp_rw [Set.mem_add, ← exists_and_left, not_exists, not_and_or, notMem_support] at hx

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
⊢ (f ⋆[L, μ] g) x = 0
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedSpace 𝕜 E'
inst✝¹⁰ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : AddCommGroup G
inst✝⁶ : μ.IsAddLeftInvariant
inst✝⁵ : μ.IsNegInvariant
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E
hbf : BddAbove (range fun x ↦ ‖f x‖)
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Integrable g μ
⊢ Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
by
  rw [← convolution_flip]
  exact hbf.continuous_convolution_right_of_integrable L.flip hg hf

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ x ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} → {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
⟨n, ns, hx⟩

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : x ∈ s
⊢ ∃ n, x ∈ support (g n)

Tactic:
rw [← hT] at hx
    obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by
      simpa only [mem_iUnion, exists_prop] using! hx
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `obtain` on the next line. It is not yet clear whether this is due to defeq
    abuse in Mathlib or a problem in the new canonicalizer; a minimization would help. -/
    obtain ⟨n, hn⟩ := hg ▸ iT
    grind

Goal state after: