mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist

Goal state before:
pp: F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun x ↦ Euclidean.dist (f x) (g x)

Tactic:
simp only [Euclidean.dist]

Goal state after:
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun x ↦ Dist.dist (toEuclidean (f x)) (toEuclidean (g x))
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: case pos.inl.inl
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
⊢ μ.real univ • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ

Tactic:
have : Subsingleton E := finrank_zero_iff.1 hE
      have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
      conv_rhs => rw [this]
      simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const]

Goal state after:
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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∉ K
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport H]

Goal state after:
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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst✝⁹] M
H : x ∉ L
⊢ f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport H]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
y : β
hy1 : p.c y ∉ p.iUnionUpTo p.lastStep
hy2 : p.τ⁻¹ * p.R p.lastStep < p.r y
Hy : p.c y ∈ p.iUnionUpTo p.lastStep
⊢ False

Tactic:
exact hy1 Hy

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: 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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

Tactic:
obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)

Goal state after:
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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
g : C(G, ℝ)
hg : HasCompactSupport ⇑g ∧ 0 ≤ ⇑g ∧ g 1 ≠ 0
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: 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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

Tactic:
obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)

Goal state after:
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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg : HasCompactSupport ⇑g ∧ 0 ≤ ⇑g ∧ g 1 ≠ 0
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos
G : Type u_1
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
hG : LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1

Tactic:
obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)

Goal state after:
case pos
G : Type u_1
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg : HasCompactSupport ⇑g ∧ 0 ≤ ⇑g ∧ g 1 ≠ 0
⊢ μ.haarScalarFactor μ = 1
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's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ≤ multiplicity E

Tactic:
apply le_csSup

Goal state after:
case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ BddAbove {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}

case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ BddAbove {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}

pp: case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}

Tactic:
· refine ⟨5 ^ finrank ℝ E, ?_⟩
    rintro _ ⟨s, ⟨rfl, h⟩⟩
    exact Besicovitch.card_le_of_separated s h.1 h.2

Goal state after:
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.Regular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this : map ((fun a ↦ a⁻¹) ∘ fun a ↦ a⁻¹) μ = c ^ 2 • μ
⊢ μ = c ^ 2 • μ

Tactic:
simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.InnerRegular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this : map ((fun a ↦ a⁻¹) ∘ fun a ↦ a⁻¹) μ = c ^ 2 • μ
⊢ μ = c ^ 2 • μ

Tactic:
simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case hm
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i, μ s / ↑N ≤ ∑ i, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
⊢ ∀ b ∈ w, MeasurableSet (o ∩ closedBall (↑↑b) (r ↑↑b))

Tactic:
· intro b _
          apply omeas.inter measurableSet_closedBall

Goal state after:
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑(d ^ ↑r)

Tactic:
ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x ↦ |x|) (↑(SignType.sign x)) x

Tactic:
simpa [hx] using hasStrictDerivAt_abs_neg hx

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt (fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) +
      fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G))
    fg

Tactic:
← hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff

Goal state after:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) +
        fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G)))
    fg
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
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
⊢ m = ∞ → m = ω

Tactic:
by simp [m_ne]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
c : 𝕜
⊢ HasGradientAtFilter (fun x ↦ c) 0 x L

Tactic:
rw [HasGradientAtFilter, map_zero]; exact hasFDerivAtFilter_const c _

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

Goal state before:
pp: l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), l ≤ b → b ∈ s
hl' : Ioi l ⊆ s
⊢ Tendsto (fun x ↦ f x / g x) atTop l✝

Tactic:
refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv <;> grind

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✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
⊢ ∃ t A,
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ n, t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
by
  rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with
    ⟨t, A, t_closed, st, t_approx, ht⟩
  refine
    ⟨disjointed t, A, disjoint_disjointed _,
      MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩
  · rw [iUnion_disjointed]; exact st
  · intro n; exact (t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)

Tactic:
have :
      ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧
        ∀ (t : Set E), ApproximatesLinearOn f A t δ →
          μ (f '' t) ≤ (Real.toNNReal |A.det| + ε : ℝ≥0) * μ t := by
    intro A
    let m : ℝ≥0 := Real.toNNReal |A.det| + ε
    have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
    rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
    exact ⟨δ, h', fun t ht => h t f ht⟩

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
this :
  ∀ (A : E →L[ℝ] E),
    ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ NullMeasurableSet (f '' s) μ

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
  have A : f '' s =ᵐ[μ] f '' t := by
    have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
    rw [this, image_union]
    refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
    apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _
      (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2
    exact (hf' x hx.1).differentiableWithinAt.mono sdiff_subset
  apply NullMeasurableSet.congr _ A.symm
  apply MeasurableSet.nullMeasurableSet
  apply measurable_image_of_fderivWithin ht _ (hf.mono ts) (f' := f')
  intro x hx
  exact (hf' x (ts hx)).mono ts

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

Goal state before:
pp: H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
N O : StructureGroupoid H
h : (fun s ↦ s.members) N = (fun s ↦ s.members) O
⊢ N = O

Tactic:
cases N

Goal state after:
case mk
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
O : StructureGroupoid H
members✝ : Set (OpenPartialHomeomorph H H)
trans'✝ : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members✝ → e' ∈ members✝ → e ≫ₕ e' ∈ members✝
symm'✝ : ∀ e ∈ members✝, e.symm ∈ members✝
id_mem'✝ : OpenPartialHomeomorph.refl H ∈ members✝
locality'✝ :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ members✝) → e ∈ members✝
mem_of_eqOnSource'✝ : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members✝ → e' ≈ e → e' ∈ members✝
h :
  (fun s ↦ s.members)
      { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
        mem_of_eqOnSource' := mem_of_eqOnSource'✝ } =
    (fun s ↦ s.members) O
⊢ { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
      mem_of_eqOnSource' := mem_of_eqOnSource'✝ } =
    O
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
⊢ SecondCountableTopology M

Tactic:
by
  have : ∀ x : M, SecondCountableTopology (chartAt H x).source :=
    fun x ↦ (chartAt (H := H) x).secondCountableTopology_source
  have := hsc.toEncodable
  rw [biUnion_eq_iUnion] at hs
  exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

Goal state after:
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
hs : e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
⊢ x ∈ e.source ∩ interior s

Tactic:
open_s.interior_eq

Goal state after:
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
hs : e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
⊢ x ∈ e.source ∩ s
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
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen[inst✝²] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ e.symm ≫ₕ ofSet f.source ⋯ ≫ₕ e' ≈ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e'

Tactic:
by rw [trans_assoc]

Goal state after:
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'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ ChartedSpace.atlas
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he

Goal state after:
case inl
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'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e ↦ e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

case inr
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'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e ↦ e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯