mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ cfcₙ (fun r ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfcₙ (f x) a ∂μ

Tactic:
have : ∀ᵐ (x : X) ∂(μ.restrict s), ContinuousOn (f x) (quasispectrum 𝕜 a) :=
    ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ cfcₙ (fun r ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfcₙ (f x) a ∂μ
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
⊢ (f.leftMulMapPreGNS (x✝¹ + x✝)).completion = (f.leftMulMapPreGNS x✝¹).completion + (f.leftMulMapPreGNS x✝).completion

Tactic:
ext c
    induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp [add_mul, Completion.coe_add]

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 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ RCLike.re ((U * Uᴴ) i i) = 1

Tactic:
simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]

Goal state after:
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: z : Circle
⊢ (starRingEnd ℂ) ↑z * ↑1 = (starRingEnd ℂ) ↑z

Tactic:
ofReal_one,

Goal state after:
z : Circle
⊢ (starRingEnd ℂ) ↑z * 1 = (starRingEnd ℂ) ↑z
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case inr
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
⊢ ∃ e, Icc a b ⊆ e.baseSet

Tactic:
have hsc : IsLUB s c := isLUB_csSup sne sbd

Goal state after:
case inr
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
⊢ ∃ e, Icc a b ⊆ e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1

Tactic:
← e.coe_coe,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e.toPartialEquiv (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm ((↑e x).1, (↑e x).2) = x

Tactic:
← e.coe_coe,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm ((↑e.toPartialEquiv x).1, (↑e.toPartialEquiv x).2) = x
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (⟨proj ↑z, ⋯⟩, (↑e ↑z).2) ∈ Prod.map Subtype.val id ⁻¹' e.target

Tactic:
by
    simpa only [Prod.map_apply, ← e.proj_toFun _ hz] using! e.map_source' hz

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e ↦ e.toPretrivialization) e = (fun e ↦ e.toPretrivialization) e'
⊢ e = e'

Tactic:
ext1
  exacts [OpenPartialHomeomorph.toPartialEquiv_injective congr(Pretrivialization.toPartialEquiv $h),
    congr(Pretrivialization.baseSet $h)]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map Prod.fst (map (↑e) (𝓝 x)) = 𝓝 (↑e x).1

Tactic:
← e.coe_coe,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map Prod.fst (map (↑e.toOpenPartialHomeomorph) (𝓝 x)) = 𝓝 (↑e.toOpenPartialHomeomorph x).1
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b✝ : B
y : E b✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype] fun ex ↦ ⟨T.lift ↑ex.1 ↑ex.2, ⋯⟩

Tactic:
by
    apply Continuous.subtype_mk
    refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])
    refine .prodMk (by fun_prop) (.snd ?_)
    exact T.continuousOn_toFun.comp_continuous (by fun_prop) (by simp)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case e'_3
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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = ⇑(fs.orderEmbOfFin h).toEmbedding '' ↑univ

Tactic:
Finset.coe_univ,

Goal state after:
case e'_3
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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = ⇑(fs.orderEmbOfFin h).toEmbedding '' Set.univ
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 : (↑univ).indicator (centroidWeightsIndicator k fs₁) = (↑univ).indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂

Tactic:
Finset.coe_univ,

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 : Set.univ.indicator (centroidWeightsIndicator k fs₁) = Set.univ.indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂
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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face ⋯
⊢ (affineCombination k {i}ᶜ s.points) (centroidWeights k {i}ᶜ) = (affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹

Tactic:
centroidWeights_eq_const,

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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face ⋯
⊢ (affineCombination k {i}ᶜ s.points) (Function.const (Fin (n + 1)) (↑(#{i}ᶜ))⁻¹) =
    (affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹
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 ι
inhabited_h : Inhabited ι
⊢ Finite ι

Tactic:
affineIndependent_iff_linearIndependent_vsub k p default

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
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i ↦ p ↑i -ᵥ p default
⊢ Finite ι
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ Set.finrank k (Set.range fun i ↦ p ↑i -ᵥ p i₁) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
vectorSpan_range_eq_span_range_vsub_right_ne k p i₁,

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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ Set.finrank k (Set.range fun i ↦ p ↑i -ᵥ p i₁) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr
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
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ FiniteDimensional k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction

Tactic:
· rw [affineSpan_coe, direction_affineSpan_insert hp₀]
    infer_instance

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

Goal state before:
pp: case inr
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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
rw [collinear_iff_of_mem hp₁]

Goal state after:
case inr
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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ 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 : f.rOut ≤ dist x c
⊢ ¬dist x c < f.rOut

Tactic:
not_lt

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
⊢ f.rOut ≤ dist x c
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
⊢ AffineIndependent k ![p₁, p₂, p]

Tactic:
by
  rw [affineIndependent_iff_not_collinear_set]
  by_contra h
  have h1 : Collinear k {p₁, p₃, p₂, p} := by
    apply collinear_insert_insert_of_mem_affineSpan_pair
    · apply Collinear.mem_affineSpan_of_mem_of_ne h (by simp) (by simp) (by simp) hne
    · apply Collinear.mem_affineSpan_of_mem_of_ne hcol (by simp) (by simp) (by simp) hne
  have h2 : Collinear k {p₁, p₂, p₃} := h1.subset (by grind)
  rw [affineIndependent_iff_not_collinear_set] at ha
  exact ha h2

Goal state after:
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
⊢ (iteratedFDeriv 𝕜 (k + 1) fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x

Tactic:
| succ k IH =>

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
x : G
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun t ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

Tactic:
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)

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

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : ‖y‖ ^ 2 < 1 ^ 2
⊢ 0 < 1 - ‖y‖ ^ 2

Tactic:
one_pow,

Goal state after:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : ‖y‖ ^ 2 < 1
⊢ 0 < 1 - ‖y‖ ^ 2
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1
𝕜 : 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✝⁵ : AddGroup G
inst✝⁴ : MeasurableAdd₂ G
inst✝³ : MeasurableNeg G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddRightInvariant
inst✝ : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas : AEStronglyMeasurable (fun p ↦ (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y ↦ ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
⊢ Integrable (fun t ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν

pp: case refine_2
𝕜 : 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✝⁵ : AddGroup G
inst✝⁴ : MeasurableAdd₂ G
inst✝³ : MeasurableNeg G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddRightInvariant
inst✝ : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas : AEStronglyMeasurable (fun p ↦ (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y ↦ ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
t : G
⊢ ‖∫ (x : G), ‖(L (f t)) (g (x - t))‖ ∂μ‖ ≤ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ

Tactic:
· simp only [integral_sub_right_eq_self (‖g ·‖)]
    fun_prop

Goal state after:
case refine_2
𝕜 : 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✝⁵ : AddGroup G
inst✝⁴ : MeasurableAdd₂ G
inst✝³ : MeasurableNeg G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddRightInvariant
inst✝ : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas : AEStronglyMeasurable (fun p ↦ (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y ↦ ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
t : G
⊢ ‖∫ (x : G), ‖(L (f t)) (g (x - t))‖ ∂μ‖ ≤ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ 0 < μ (u ∩ s)

Tactic:
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ 0 < μ (u ∩ s)

Tactic:
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
⊢ IsGδ k

Tactic:
suffices ⋂ n, V n * k ⊆ k by
    replace : k = ⋂ n, V n * k := by
      apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this
      exact subset_mul_right k (by simp [V, mem_W])
    rw [this]
    refine .iInter_of_isOpen fun n ↦ ?_
    exact .mul_right (isOpen_biInter_finset (fun i _hi ↦ W_open i))

Goal state after:
G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
⊢ ⋂ n, V n * k ⊆ k
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
⊢ ∫ (t : ℝ) in 0..x, (L (f t)) (g (x - t)) ∂ν = ∫ (t : ℝ), (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) ∂ν

Tactic:
intervalIntegral.integral_of_le (le_of_lt h),

Goal state after:
case pos
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
⊢ ∫ (x_1 : ℝ) in Ioc 0 x, (L (f x_1)) (g (x - x_1)) ∂ν =
    ∫ (t : ℝ), (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) ∂ν
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : HasContDiffBump E
inst✝⁷ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝⁶ : BorelSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : IsLocallyFiniteMeasure μ
inst✝³ : μ.IsOpenPosMeasure
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : CompleteSpace X
z : X
⊢ ∫ (x : E), f.normed μ x • z ∂μ = z

Tactic:
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]

Goal state after: