mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
⊢ ContDiffOn 𝕜 (↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
let isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
⊢ ContDiffOn 𝕜 (↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩)

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)
x : E
hx : x ∈ s
⊢ δ + dist x 0 ≤ δ + 2

Tactic:
rw [dist_zero_right]; exact add_le_add le_rfl (hs x hx)

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution

Goal state before:
pp: case g_supp
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : x ∈ (fun y ↦ x₀ - y) ⁻¹' ball 0 (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut

Tactic:
simp only [mem_preimage, mem_ball, dist_zero_right] at hx

Goal state after:
case g_supp
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : ‖x₀ - x‖ < (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ∞
⊢ μ' s = ν s

Tactic:
have Hν : IsEverywherePos ν s :=
      h's.smul_measure_nnreal (haarScalarFactor_pos_of_isHaarMeasure _ _).ne'

Goal state after:
case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ∞
Hν : ν.IsEverywherePos s
⊢ μ' s = ν s
Module: Mathlib.Analysis.Calculus.ContDiff.Polynomial

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝² : CommSemiring R
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : Algebra R 𝕜
f : R[X]
n : WithTop ℕ∞
⊢ ContDiff 𝕜 n fun x ↦ (aeval x) f

Tactic:
induction f using Polynomial.induction_on' with

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars

Goal state before:
pp: case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n✝ : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ContDiffWithinAt 𝕜' (↑n) f s x →
    restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s
h : ContDiffWithinAt 𝕜' (↑(n + 1)) f s x
t₀ : ContDiffWithinAt 𝕜' (↑n) f s x
t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y
a : E
h₁a : restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] a] iteratedFDerivWithin 𝕜 n f s
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1)) f s a
h₄a : a ∈ s
m : Fin (n + 1) → E
⊢ DifferentiableWithinAt 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a

Tactic:
apply h₃a.differentiableWithinAt_iteratedFDerivWithin
      · rw [Nat.cast_lt]
        simp
      · have : UniqueDiffOn 𝕜' s := hs.mono_field
        simpa [s.insert_eq_of_mem h₄a]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap

Goal state before:
pp: case intro
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → F i →L[𝕜] G i
x : E
inst✝ : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val✝ : Fintype ι
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap fun x_1 ↦ g x_1 x) x

Tactic:
classical
  exact hf.hasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivAt) |>.differentiableAt

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ')).range = ⊤
fφ : E → F × ℝ := fun x ↦ (f x, φ x)
⊢ map Prod.snd (map fφ (𝓝 x₀ ⊓ 𝓟 (fφ ⁻¹' {p | p.1 = f x₀}))) = 𝓝 (φ x₀)

Tactic:
map_inf_principal_preimage,

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ')).range = ⊤
fφ : E → F × ℝ := fun x ↦ (f x, φ x)
⊢ map Prod.snd (map fφ (𝓝 x₀) ⊓ 𝓟 {p | p.1 = f x₀}) = 𝓝 (φ x₀)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
rw [eventually_iff_exists_mem] at *
  rcases hff' with ⟨s₁, hs₁, hff'⟩
  rcases hgg' with ⟨s₂, hs₂, hgg'⟩
  rcases hg' with ⟨s₃, hs₃, hg'⟩
  let s := s₁ ∩ s₂ ∩ s₃
  have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃
  rw [mem_nhdsGT_iff_exists_Ioo_subset] at hs
  rcases hs with ⟨u, hau, hu⟩
  refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv <;> grind

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

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
⊢ Tendsto f atTop (𝓝 0)

Tactic:
have B : limUnder atTop (F ∘ f) = F 0 := by
    have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
    apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
    intro s hs
    rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
    rw [← top_le_iff, ← volume_Ici (a := b)]
    exact measure_mono hb

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
B : atTop.limUnder (⇑F ∘ f) = F 0
⊢ Tendsto f atTop (𝓝 0)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: case pos.inr
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
⊢ ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν

Tactic:
have L_emb : MeasurableEmbedding L := L.toHomeomorph.measurableEmbedding

Goal state after:
case pos.inr
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
⊢ ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'

Tactic:
let f := Function.update (u * v) a a'

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
⊢ ∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : CommMonoid α
f : ι → β → α
s : Set β
inst✝ : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
hg hp : HasProdUniformlyOn f g s
⊢ HasProdUniformlyOn f (fun x ↦ ∏' (i : ι), f i x) s

Tactic:
rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at hg ⊢

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : CommMonoid α
f : ι → β → α
s : Set β
inst✝ : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
hg : TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
hp : HasProdUniformlyOn f g s
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) (fun x ↦ ∏' (i : ι), f i x) atTop s
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'

Tactic:
let f := Function.update (u * v) a a'

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inr
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.inr x ∈
    (Sum.elim (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯)
        (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯) (Sum.inr x)).source

Tactic:
Sum.elim_inr,

Goal state after:
case inr
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.inr x ∈ ((ChartedSpace.chartAt x).lift_openEmbedding ⋯).source
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y

Tactic:
ChartedSpace.sum_chartAt_inr

Goal state after:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inr y) = ↑(chartAt H x) y
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen[inst✝] s), {↑e ⁻¹' s ∩ e.source}

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Goal state after:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ i_1, IsOpen[inst✝] i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ i_1, IsOpen[inst✝] i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source

Tactic:
refine ⟨e, he, univ, isOpen_univ, ?_⟩

Goal state after:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source = ↑e ⁻¹' univ ∩ e.source
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := ⋯
s : Set H
s_open : IsOpen[inst✝] s
⊢ ↑e ⁻¹' s ∩ e.source ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen[inst✝] s), {↑e ⁻¹' s ∩ e.source}

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst✝] s
⊢ ∃ i ∈ c.atlas, ∃ i_1, IsOpen[inst✝] i_1 ∧ ↑e ⁻¹' s ∩ e.source = ↑i ⁻¹' i_1 ∩ i.source
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ LiftProp P f ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
LiftProp,

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ (∀ (x : M), LiftPropAt P f x) ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))

Tactic:
by
  by_cases h : IsRCLikeNormedField 𝕜
  · let := h.rclike 𝕜
    let := NormedSpace.restrictScalars ℝ 𝕜 E
    rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]
    · apply subset_closure
    · apply I.convex_range
    · apply I.nonempty_interior
  · simp [range_eq_univ_of_not_isRCLikeNormedField I h]

Goal state after: