mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional k ↥(vectorSpan k s)

Tactic:
refine IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
c : 𝕜
hp : ∞ ≠ 0
f : ↥(lp E ∞)
h✝ : IsEmpty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

pp: case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
c : 𝕜
hp : ∞ ≠ 0
f : ↥(lp E ∞)
h✝ : Nonempty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
· simp [lp.eq_zero' f]

Goal state after:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
c : 𝕜
hp : ∞ ≠ 0
f : ↥(lp E ∞)
h✝ : Nonempty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
⊢ ‖star f‖ = ‖f‖

Tactic:
rcases p.trichotomy with (rfl | rfl | h)
    · exfalso
      have := ENNReal.toReal_mono ENNReal.zero_ne_top hp.elim
      norm_num at this
    · simp only [lp.norm_eq_ciSup, lp.star_apply, norm_star]
    · simp only [lp.norm_eq_tsum_rpow h, lp.star_apply, norm_star]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν (n ∩ ?m.55)

pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ Set α

Tactic:
rw [ht (n ∩ t) inter_subset_right]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < μ (n ∩ t)
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ support (f.normed μ) = ball c f.rOut

Tactic:
by
  unfold ContDiffBump.normed
  rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ ≤ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ

Tactic:
apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)

Tactic:
have K_pos : 0 < K := by
    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
  have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
    gcongr
    · exact f.integral_pos.le
    · exact f.le_one
  apply this.trans
  rw [div_le_div_iff₀ f.integral_pos, one_mul, ← div_le_iff₀' (pow_pos K_pos _)]
  · exact f.measure_closedBall_div_le_integral μ K h
  · exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne'
      measure_closedBall_lt_top.ne

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ContDiff ℝ ∞ fun x ↦ (f x + f (-x)) / 2

Tactic:
exact (f_smooth.add (f_smooth.comp contDiff_neg)).div_const _

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A✝ : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A✝)
N_mem : N ∈ univ \ A✝
Inf_eq_N : sInf (univ \ A✝) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a b : Fin N.succ
a_ne_b : a ≠ b
G_le : G ↑a ≤ G ↑b
H : G ↑a = G ↑b
A : ↑a ≠ ↑b
⊢ G ↑a < G ↑b

Tactic:
← color_G a (Nat.lt_succ_iff.1 a.2),

Goal state after:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A✝ : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A✝)
N_mem : N ∈ univ \ A✝
Inf_eq_N : sInf (univ \ A✝) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a b : Fin N.succ
a_ne_b : a ≠ b
G_le : G ↑a ≤ G ↑b
H : G ↑a = G ↑b
A : p.color (G ↑a) ≠ ↑b
⊢ G ↑a < G ↑b
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a : Fin (N + 1)
ha : a < last N
I : ↑a < N
⊢ G N = i

Tactic:
simp only [G, if_true]

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

Goal state before:
pp: 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'
φ : ContDiffBump 0
inst✝³ : BorelSpace G
inst✝² : FiniteDimensional ℝ G
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), ((lsmul ℝ ℝ) (φ.normed μ t)) (g x₀) ∂μ = g x₀

Tactic:
exact integral_normed_smul φ μ (g x₀)

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

Goal state before:
pp: case a
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
s : Set G
h's : IsCompact (closure[inst✝⁸] s)
ν : Measure G := ⋯
⊢ μ'.haarScalarFactor μ • μ s ≤ μ' s

Tactic:
calc
    ν s ≤ ν ((toMeasurable μ' s) ∩ (closure s)) :=
      measure_mono <| subset_inter (subset_toMeasurable μ' s) subset_closure
    _ = μ' ((toMeasurable μ' s) ∩ (closure s)) := by
      apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm
      · exact (measurableSet_toMeasurable μ' s).inter isClosed_closure.measurableSet
      · exact h's.closure_of_subset inter_subset_right
    _ ≤ μ' (toMeasurable μ' s) := measure_mono inter_subset_left
    _ = μ' s := measure_toMeasurable s

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin N.succ), τ⁻¹ ≤ a.r k
H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
⊢ τ⁻¹ ≤ a.r j

Tactic:
exact hτ' j

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

Goal state before:
pp: α : 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))
C : HasSum (fun x ↦ μ (o ∩ closedBall (↑↑x) (r ↑↑x))) (μ (o ∩ v i))
this : μ s / (↑N + 1) < μ (o ∩ v i)
⊢ ∃ w, μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))

Tactic:
exact ((tendsto_order.1 C).1 _ this).exists

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

Goal state before:
pp: case inl
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 : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ a ∈ Ioo a b

Tactic:
refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)

Goal state after:
case inl
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 : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ HasFDerivWithinAt (fun x ↦ |f x|) (-f') s x

Tactic:
convert! (hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf using 1
  simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : 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
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
hi : i ∈ Finset.univ
⊢ ‖f (v i)‖ ≤ ‖f‖ * ‖v i‖

Tactic:
apply f.le_opNorm

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

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 : ℕ
f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
hf : ∀ (x y : E), (f x) y = (f y) x
⊢ alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f) = 0

Tactic:
ext v
  simp [alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, hf]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
ν : Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ ∃ t,
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p ↦ closedBall p.1 p.2

Tactic:
rcases exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux ν f s hf with
    ⟨t, t_count, ts, tr, tν, tdisj⟩

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
ν : Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
t : Set (α × ℝ)
t_count : t.Countable
ts : ∀ p ∈ t, p.1 ∈ s
tr : ∀ p ∈ t, p.2 ∈ f p.1
tν : ν (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0
tdisj : t.PairwiseDisjoint fun p ↦ closedBall p.1 p.2
⊢ ∃ t,
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p ↦ closedBall p.1 p.2
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 t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
intro v w

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
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v
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 t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ IsSymmSndFDerivWithinAt 𝕜 f t x

Tactic:
intro v w

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
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap

Goal state before:
pp: 𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap fun x_1 ↦ g x_1 x) x

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

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
t : ℝ
ht : t ∈ Icc 0 1
this : x + h • v ∈ interior s
⊢ x + h • v + (t * h) • w ∈ interior s

Tactic:
← smul_smul

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
t : ℝ
ht : t ∈ Icc 0 1
this : x + h • v ∈ interior s
⊢ x + h • v + t • h • w ∈ interior s
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
h : ‖L.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 n f s x)‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
← L.iteratedFDerivWithin_comp_left hf hs hx hn

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
h : ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

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 : ℕ
ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hs : ω₁ =ᶠ[𝓝[insert x s] x] ω₂
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
apply Filter.EventuallyEq.extDerivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
  exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Goal state after: