mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
⊢ IsExtreme 𝕜 A (⋂ i, F i)

Tactic:
inhabit ι

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
⊢ IsExtreme 𝕜 A (⋂ i, F i)
Module: Mathlib.Analysis.CStarAlgebra.Projection

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
h : p ≤ q
⊢ Commute p q

Tactic:
rw [commute_iff_eq, hp.le_iff_mul_eq_right hq |>.mp h, hp.le_iff_mul_eq_left hq |>.mp h]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ‖U‖ ≤ 1

Tactic:
simp_rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intros
  exact entry_norm_bound_of_unitary hU _ _

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast ⋯ b) = { proj := x, snd := b }

Tactic:
subst h; rfl

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

Tactic:
(ofSet s hs).trans_ofSet hs'

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ x ∈ Z.baseSet j ∩ Z.baseSet i ∩ Z.baseSet j

Tactic:
· simp [hx]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.source ∩ ↑f ⁻¹' f.target ∩ ↑f ⁻¹' ↑f.symm ⁻¹' U = f.source ∩ U

Tactic:
Set.inter_eq_self_of_subset_left
        f.source_preimage_target,

Goal state after:
case refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.source ∩ ↑f ⁻¹' ↑f.symm ⁻¹' U = f.source ∩ U
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ ∃ t, f e ∈ t.baseSet

Tactic:
refine ⟨hf.trivializationOfSMulDisjoint hfG (interior U) isOpen_interior
    fun g hg ↦ ?_, e, mem_interior_iff_mem_nhds.mpr heU, rfl⟩

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ g = 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
⊢ exp f = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ }

Tactic:
ext a
  simp_rw [NormedSpace.exp_eq_expSeries_sum (𝔸 := C(α, 𝕜)) 𝕜, FormalMultilinearSeries.sum]
  have h_sum := NormedSpace.expSeries_summable (𝕂 := 𝕜) f
  simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]
  simp [NormedSpace.exp_eq_tsum 𝕜]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : x = 0
⊢ normalize (normalize x) = normalize x

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize (normalize x) = normalize x

Tactic:
· simp [hx]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize (normalize x) = normalize x
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ ℜ ↑(unitarySelfAddISMul a ha_norm) = a

Tactic:
simp [IsSelfAdjoint.imaginaryPart (x := CFC.sqrt (1 - a ^ 2 : A)) (by cfc_tac)]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜

Tactic:
← adjoint_inner_right

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪x, (adjoint A) (A x)⟫_𝕜
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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(#fs₁))⁻¹) x =
      (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(#fs₂))⁻¹) x
⊢ fs₁ = fs₂

Tactic:
h₁,

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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) x =
      (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(#fs₂))⁻¹) x
⊢ fs₁ = fs₂
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
S : F →ₗ[𝕜] E
⊢ (adjoint S ∘ₗ T ∘ₗ S).IsSymmetric

Tactic:
by
  simpa using hT.conj_adjoint S.adjoint

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
⊢ Finite ι

Tactic:
inhabit ι

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
⊢ Finite ι
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
⊢ ¬Collinear k ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ ∅))) ↔ ¬Collinear k {p₁, p₂, p₃}

Tactic:
Set.singleton_union,

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
p₁ p₂ p₃ : P
⊢ ¬Collinear k (insert p₁ (insert p₂ (insert p₃ ∅))) ↔ ¬Collinear k {p₁, p₂, p₃}
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ ↑f x = 1

Tactic:
by
  apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn
  simpa only [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
    div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t ↦ f (g / t)) μ
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹

Tactic:
div_inv_eq_mul,

Goal state after:
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t ↦ f (g / t)) μ
x✝ : G
⊢ x✝ = g * (g⁻¹ * x✝)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr
α : 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
⊢ Summable fun i ↦ ‖f i‖ ^ p.toReal

Tactic:
have hf' := hfq.summable hq

Goal state after:
case inr.inr.inr.inr.inr
α : 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
⊢ Summable fun i ↦ ‖f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case neg
α : 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)
i : α
h : ¬p.toReal < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simp only [not_lt] at h

Goal state after:
case neg
α : 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)
i : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ p.toReal
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case right
α : 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
h'm : ↑(m + 1) ≤ N
A : ∀ (n : α) (x : E), HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
n : α
x : E
⊢ ‖iteratedFDeriv 𝕜 (m + 1) (f n) x‖ ≤ v (m + 1) n

Tactic:
exact h'f _ _ _ h'm

Goal state after:
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
⊢ ContDiff 𝕜 (↑m) ((fun x ↦ ∑ i ∈ T, f i x) + fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x)

Tactic:
apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add

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 α := ⋯
ht : t.Finite
T : Finset α := ⋯
this : (fun x ↦ ∑' (i : α), f i x) = (fun x ↦ ∑ i ∈ T, f i x) + fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x
⊢ ContDiff 𝕜 ↑m fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (f x).ofLp i) t

Tactic:
← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableOn_iff,

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ DifferentiableOn 𝕜 (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (f x).ofLp i) t
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr
ι : 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' : UniformCauchySeqOn f' l (Metric.ball x 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 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero

Goal state after:
case inr
ι : 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' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
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✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
x : G
⊢ (g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x

Tactic:
simp_rw [convolution_def]

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✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
x : G
⊢ ∫ (t : G), (L.flip (g t)) (f (x - t)) ∂μ = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z ↦ ContinuousLinearMap.smulRight 1 (g' z)
⊢ HasDerivAt g (g' x) x

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf ⊢

Goal state after:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z ↦ ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
⊢ HasFDerivAt g (ContinuousLinearMap.toSpanSingleton 𝕜 (g' x)) x
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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
simp_rw [convolution_def]

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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist (∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Module: Mathlib.MeasureTheory.Measure.EverywherePos

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

Tactic:
rw [isOpen_iff_mem_nhds]

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

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst✝²⁶ : NormedAddCommGroup E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x ↦ ‖g x‖) (fun x ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk : ConvolutionExistsAt (fun x ↦ ‖f x‖) ((fun x ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
h_meas : AEStronglyMeasurable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y ↦ ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν
h3 : Measure.map (fun z ↦ (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν
this :
  Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x))))
    (Measure.map (fun z ↦ (z.1 - z.2, z.2)) (μ.prod ν))
x y : G
⊢ uncurry (fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (x, y) =
    ((uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) ∘ fun z ↦ (z.1 - z.2, z.2)) (x, y)

Tactic:
simp +unfoldPartialApp only [uncurry, Function.comp_apply,
      sub_sub_sub_cancel_right]

Goal state after: