mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case refine_2
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
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
hr : r < μ K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst✝⁷] L
⊢ r < μ L

Tactic:
convert! hr using 1

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
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
hr : r < μ K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst✝⁷] L
⊢ μ L = μ K
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
⊢ p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep

Tactic:
conv_rhs => rw [← one_mul (p.R p.lastStep)]

Goal state after:
α : 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
⊢ p.τ⁻¹ * p.R p.lastStep < 1 * p.R p.lastStep
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
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

Tactic:
have : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ hc
  obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)
  apply NNReal.coe_injective
  calc
    c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
      rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
    _ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
    _ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) := by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
    _ = μ'.haarScalarFactor μ :=
      (haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm

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

Goal state before:
pp: case pos.h'f
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ HasCompactSupport (f ∘ ⇑φ.toHomeomorph)

pp: case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0

Tactic:
· exact hf.1.comp_homeomorph φ.toHomeomorph

Goal state after:
case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0
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
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
n : ℕ
⊢ ENNReal.toNNReal 0 = 0

pp: case x_out
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
n : ℕ
⊢ 0 ∉ Metric.thickening (u n) {1}

Tactic:
· simp only [ENNReal.toNNReal_zero]

Goal state after:
case x_out
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
n : ℕ
⊢ 0 ∉ Metric.thickening (u n) {1}
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
δ : ℝ
hδ : 0 < δ
hδ' : δ < 1
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖
s_card : multiplicity E < s.card
⊢ N ≤ s.card

Tactic:
exact s_card

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), F (u n) ∈ closedBall 0 2
f : Fin N → E
fmem : f ∈ closedBall 0 2
φ : ℕ → ℕ
φ_mono : StrictMono φ
hf : Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f)
i : Fin N
⊢ ‖f i‖ ≤ 2

pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), F (u n) ∈ closedBall 0 2
f : Fin N → E
fmem : f ∈ closedBall 0 2
φ : ℕ → ℕ
φ_mono : StrictMono φ
hf : Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f)
i j : Fin N
hij : i ≠ j
⊢ (fun i j ↦ 1 ≤ ‖f i - f j‖) i j

Tactic:
· simp only [pi_norm_le_iff_of_nonneg zero_le_two, mem_closedBall, dist_zero_right] at fmem
      exact fmem i

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), F (u n) ∈ closedBall 0 2
f : Fin N → E
fmem : f ∈ closedBall 0 2
φ : ℕ → ℕ
φ_mono : StrictMono φ
hf : Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f)
i j : Fin N
hij : i ≠ j
⊢ (fun i j ↦ 1 ≤ ‖f i - f j‖) i j
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
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
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
⊢ y ∈ ⋃ x ∈ m, x • (k * k⁻¹)

Tactic:
have ym : y ∈ m := m_max.mem_of_prop_insert (by simpa using h'y)

Goal state after:
case pos
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
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
ym : y ∈ m
⊢ y ∈ ⋃ x ∈ m, x • (k * k⁻¹)
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 Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
⊢ c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K

Tactic:
conv_rhs => rw [μeq]

Goal state after:
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 Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
⊢ c ^ 2 * μ ↑K = 1 ^ 2 * (c ^ 2 • μ) ↑K
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 Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
⊢ c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K

Tactic:
conv_rhs => rw [μeq]

Goal state after:
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 Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
⊢ c ^ 2 * μ ↑K = 1 ^ 2 * (c ^ 2 • μ) ↑K
Module: Mathlib.Analysis.Calculus.Darboux

Goal state before:
pp: a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ segment ℝ b a ⊆ Icc a b

Tactic:
segment_symm,

Goal state after:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ segment ℝ a b ⊆ Icc a b
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
s t : Set E
x : E
ht : t ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x

Tactic:
by
  simp [lieBracketWithin, fderivWithin_inter, ht]

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

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✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
val✝ : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
exact hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivWithinAt
    |>.differentiableWithinAt

Goal state after:
Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 2)), DifferentiableAt 𝕜 (V i) x
⊢ ((extDeriv ω x) fun x_1 ↦ V x_1 x) =
    ∑ i, (-1) ^ ↑i • (fderiv 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) x) (V i x) -
      ∑ i,
        ∑ j ≥ i,
          (-1) ^ (↑i + ↑j) •
            (ω x)
              (Matrix.vecCons (lieBracket 𝕜 (V i.castSucc) (V j.succ) x)
                (j.removeNth (i.castSucc.removeNth fun x_1 ↦ V x_1 x)))

Tactic:
simp only [← differentiableWithinAt_univ, ← extDerivWithin_univ, ← fderivWithin_univ,
    ← lieBracketWithin_univ] at *

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
⊢ ((extDerivWithin ω Set.univ x) fun x_1 ↦ V x_1 x) =
    ∑ x_1, (-1) ^ ↑x_1 • (fderivWithin 𝕜 (fun x ↦ (ω x) (x_1.removeNth fun x_2 ↦ V x_2 x)) Set.univ x) (V x_1 x) -
      ∑ x_1,
        ∑ x_2 ≥ x_1,
          (-1) ^ (↑x_1 + ↑x_2) •
            (ω x)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V x_1.castSucc) (V x_2.succ) Set.univ x)
                (x_2.removeNth (x_1.castSucc.removeNth fun x_3 ↦ V x_3 x)))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x
this : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ fun y ↦ ↑(N y)) s x
⊢ ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x

Tactic:
convert! this with y

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x
this : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ fun y ↦ ↑(N y)) s x
y : E
⊢ ↑(N y).symm = (ContinuousLinearMap.inverse ∘ fun y ↦ ↑(N y)) y
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✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖

Tactic:
refine norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_
  filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
⊢ (∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0) →
    (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
      ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
fsubset

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
⊢ (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
    ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x
| HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x
| t⁻¹ • t • x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x
| HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x
| t⁻¹ • t • x
Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:
pp: 𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (fun x ↦
      match x with
      | (v, w) => f v.1 w.2 - f w.1 w.2 - (↿f₁ u) (v.1 - w.1)) =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2]
    fun x ↦
    match x with
    | (v, w) => v.1 - w.1

Tactic:
have h := tendsto_snd.prodMk <| tendsto_snd.comp <| tendsto_snd.comp <|
              tendsto_fst (f := (𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)) (g := 𝓝 u.1)
            let : NormedSpace ℝ E₁ := RestrictScalars.normedSpace ℝ 𝕜 E₁
            apply isLittleO_sub_sub_fderiv (α := (E₁ × E₂) × (E₁ × E₂))
              (f := fun (v, w) x => f x w.2) (f' := fun (v, w) x => f₁ x w.2)
              (tendsto_fst.comp tendsto_fst) (tendsto_fst.comp tendsto_snd)
            · simpa using! h.eventually df₁
            · simpa using! cf₁.comp h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasFDerivAt g ((toDual 𝕜 𝕜) g') u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u

Tactic:
hasFDerivAt_iff_hasDerivAt

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g (((toDual 𝕜 𝕜) g') 1) u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasFDerivAt g ((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) u

Tactic:
hasFDerivAt_iff_hasDerivAt

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasDerivAt g (((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1) u