mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm : ∀ (x y : E), (h x) y = (h y) x
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
⊢ alternatizeUncurryFin (f.fderivCompContinuousLinearMap g ∘SL h) = 0

Tactic:
fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,

Goal state after:
case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm : ∀ (x y : E), (h x) y = (h y) x
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
⊢ alternatizeUncurryFin
      ((alternatizeUncurryFinCLM 𝕜 E G ∘SL
          ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft)) ∘SL
        h) =
    0
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x v w : E
hf : IsSymmSndFDerivAt 𝕜 f x
⊢ (iteratedFDeriv 𝕜 2 f x) ![v, w] = (iteratedFDeriv 𝕜 2 f x) ![w, v]

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ] at *

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
⊢ (iteratedFDerivWithin 𝕜 2 f univ x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f univ x) ![w, v]
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : ℕ∞ω
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x

Tactic:
by
  rw [← contDiffWithinAt_univ] at hV hW ⊢
  simp_rw [← lieBracketWithin_univ]
  exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x : E
⊢ HasLineDerivAt 𝕜 f 0 x 0

Tactic:
simp [HasLineDerivAt, hasDerivAt_const]

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) 0
this : Nontrivial E
⊢ False

Tactic:
exact not_differentiableAt_norm_zero E <| h.differentiableAt hn

Goal state after:
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (L' ×ˢ pure u)
⊢ HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

Tactic:
by
  have : ContinuousLinearMap.smulRight (1 : 𝕜 →L[𝕜] 𝕜) g' = (toDual 𝕜 𝕜) (conj g') := by
    ext; simp
  rwa [HasGradientAtFilter, ← this]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : E
a✝¹ : φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
a✝ : φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ φ.leftFun x = φ.leftFun φ.pt → φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x

Tactic:
exact fun h => by rwa [← h]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : E
a✝¹ : φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
a✝ : φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x → φ.leftFun x = φ.leftFun φ.pt

Tactic:
exact fun h => by rwa [← h]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
x : E
xs : x ∈ s
z : ↑s
zT : z ∈ T
hz : f' x ∈ ball (f' ↑z) ↑(r (f' ↑z))
⊢ ∃ ε, 0 < ε ∧ ‖f' x - f' ↑z‖ + ε ≤ ↑(r (f' ↑z))

Tactic:
by
      refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩
      simpa only [sub_pos] using! mem_ball_iff_norm.mp hz

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst✝ : NoMaxOrder α
⊢ ∀ᵐ (x : α) ∂μ.restrict (Ici B), ∀ᶠ (i : ι) in l, x ∈ Ico B (d i)

Tactic:
refine (ae_restrict_mem measurableSet_Ici).mono fun _x hx ↦ ?_

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst✝ : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ↑‖f a‖₊

Tactic:
ENNReal.ofReal_coe_nnreal

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ↑‖f a‖₊
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ ∀ (a : ℝ≥0),
    Subsingleton E ∨ a < ‖↑B.symm‖₊⁻¹ →
      ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - a)⁻¹ * a < δ₀ →
        ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → ↑m * μ s ≤ μ (f '' s)

Tactic:
intro δ h1δ h2δ s f hf

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
h2δ : ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ↑m * μ s ≤ μ (f '' s)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ IntegrableOn (fun x ↦ f' x • g (f x)) (Ioo a b) volume ↔ IntegrableOn g (f '' Ioo a b) volume

Tactic:
integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ IntegrableOn (fun x ↦ f' x • g (f x)) (Ioo a b) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) (Ioo a b) volume

case hf'
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ AntitoneOn f (Ioo a b)
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'
  · rw [eq_C_of_derivative_eq_zero hp']
    simp
  have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
  refine Finset.card_le_sdiff_of_interleaved fun x hx y hy hxy hxy' => ?_
  rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
  obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
  refine ⟨z, ?_, hz1⟩
  rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
⊢ v ∈ uniformity α →
    ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun N b ↦ ∏ i ∈ Finset.range N, f i b) n y) ∈ v

Tactic:
hv

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun N b ↦ ∏ i ∈ Finset.range N, f i b) n y) ∈ v
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') (Ioi a) volume
hu'v : IntegrableOn (u' * v) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Tactic:
rw [Pi.mul_def] at huv' hu'v

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 (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v 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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (u * v') (Iic a) volume
hu'v : IntegrableOn (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Tactic:
rw [Pi.mul_def] at huv' hu'v

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 (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s ∈ {OpenPartialHomeomorph.refl H}
⊢ e.restr s = OpenPartialHomeomorph.refl H

Tactic:
simpa only using! hs

Goal state after:
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
hs'' : IsOpen[inst✝³] (↑e' '' (e'.source ∩ s))
ht : IsOpen[inst✝³] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ e'.symm ≫ₕ e.restr s ∈ G

Tactic:
exact G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').2 ht) (e.symm_trans_restr e' hs)

Goal state after:
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ofSet e.target ⋯ ∈ G

Tactic:
have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)

Goal state after:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
hle : idRestrGroupoid ≤ G
⊢ ofSet e.target ⋯ ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: case left
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✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ (c.symm ≫ₕ f₁).source

Tactic:
simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]

Goal state after:
case left
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✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ c.symm.source
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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
⊢ v ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • u + b • v ∈ s

Tactic:
hv

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
hv : v ∈ s
⊢ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • u + b • v ∈ s
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case pos
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W :
  ∀ ⦃x : E⦄, x ∈ range ↑I → ∀ ⦃y : E⦄, y ∈ range ↑I → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range ↑I
u : E
hu : u ∈ range ↑I
v : E
⊢ v ∈ range ↑I → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • u + b • v ∈ range ↑I

Tactic:
hv

Goal state after:
case pos
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W :
  ∀ ⦃x : E⦄, x ∈ range ↑I → ∀ ⦃y : E⦄, y ∈ range ↑I → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range ↑I
u : E
hu : u ∈ range ↑I
v : E
hv : v ∈ range ↑I
⊢ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • u + b • v ∈ range ↑I
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (e.extend I).symm.source ∩ ↑(e.extend I).symm ⁻¹' (e'.extend I).source = ↑I '' (e.symm ≫ₕ e').source

Tactic:
I.image_eq,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (e.extend I).symm.source ∩ ↑(e.extend I).symm ⁻¹' (e'.extend I).source = ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I