mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case sq
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial X₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))

Tactic:
· exact ⟨hX₂.hom_ext _ _⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : ¬IsType₂ x
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
simp only [IsType₂, not_forall, not_not] at hx
      obtain ⟨_ | d, hd, i, hx⟩ := hx
      · fin_cases i
        simp at hx
      · obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by rintro rfl; simp at hx)
        refine ⟨{ x := x, d := d, hd := hd, index := i, isIndex := hx }, Or.inl ?_⟩
        dsimp
        rw [S.ext_iff']
        exact ⟨hd, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card

Tactic:
have hSs (i : Fin (d + 1)) : i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss := by
        simp [Sδ, Ss, stdSimplex.δ_apply]

Goal state after:
case inr
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq)) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ≫ (G.map f₁.hom.op).app f₃'.right

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal without the `simp`. It is not yet clear whether this is due to defeq abuse in
      Mathlib or a problem in the new canonicalizer; a minimization would help. The original
      proof was: `by grind [sq.w, sq₁₃.isPullback.w]` -/
      simp [Arrow.mk_right]; grind [sq.w, sq₁₃.isPullback.w]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ i y, (ConcreteCategory.hom (SimplicialObject.σ X i)) y = x
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0

Tactic:
let X' := ((SimplicialObject.whiskering _ _).obj (sigmaConst.obj R)).obj X

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ i y, (ConcreteCategory.hom (SimplicialObject.σ X i)) y = x
X' : SimplicialObject C := ((SimplicialObject.whiskering (Type w) C).obj (sigmaConst.obj R)).obj X
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ i y, (ConcreteCategory.hom (SimplicialObject.σ X i)) y = x
X' : SimplicialObject C := ((SimplicialObject.whiskering (Type w) C).obj (sigmaConst.obj R)).obj X
⊢ X.ιChainComplex x ≫ PInfty.f (n + 1) = 0

Tactic:
obtain ⟨i, y, rfl⟩ := hx

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
X' : SimplicialObject C := ((SimplicialObject.whiskering (Type w) C).obj (sigmaConst.obj R)).obj X
i : Fin (n + 1)
y : X _⦋n⦌
⊢ X.ιChainComplex ((ConcreteCategory.hom (SimplicialObject.σ X i)) y) ≫ PInfty.f (n + 1) = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
⊢ ∀ {x y : (pairingCore k n).ι},
    (pairingCore k n).AncestralRel x y →
      (pairingCore k n).dim x = (pairingCore k n).dim y → (finset x.x ⋯).card < (finset y.x ⋯).card

Tactic:
intro ⟨s, d, hds, is, hs⟩ ⟨t, d', hdt, it, ht⟩ ⟨h₁, h₂⟩ h₃
    obtain ⟨ds, s, hs₁, hs₂, rfl⟩ := Subcomplex.N.mk_surjective s
    obtain ⟨dt, t, ht₁, ht₂, rfl⟩ := Subcomplex.N.mk_surjective t
    obtain rfl : d = d' := h₃
    obtain rfl : ds = d + 1 := hds
    obtain rfl : dt = d + 1 := hdt
    simp only [ne_eq, pairingCore_ι, Type₁.ext_iff] at h₁
    obtain ⟨f, hf, hδ⟩ := N.le_iff_exists_mono.1 h₂.le
    dsimp at f hf
    obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f
    obtain rfl | rfl := ht.eq_of_isType₂_δ hs.isType₂_δ i (by
      rw [S.ext_iff']
      exact ⟨rfl, hδ.symm⟩)
    · refine (h₁ (hs.δ_injective ht ?_)).elim
      rw [Subcomplex.N.ext_iff, N.ext_iff, S.ext_iff']
      exact ⟨rfl, hδ.symm⟩
    · let Ss := finset (Subcomplex.N.mk s hs₁ hs₂) rfl
      let St := finset (Subcomplex.N.mk t ht₁ ht₂) rfl
      let Sδ := finset hs.δ rfl
      replace hδ (i : Fin (d + 1)) :
          s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i) :=
        DFunLike.congr_fun (congr_arg Prod.fst hδ.symm) i
      have hSs (i : Fin (d + 1)) : i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss := by
        simp [Sδ, Ss, stdSimplex.δ_apply]
      have hSt (i : Fin (d + 1)) : i ∈ Sδ ↔ it.succ.succAbove i ∈ St := by
        simp [Sδ, St, stdSimplex.δ_apply, hδ]
      suffices Ss.card = Sδ.card ∧ St.card = Sδ.card + 1 by grind
      constructor
      · suffices Ss = Finset.image is.castSucc.succAbove Sδ by
          rw [this]
          exact Finset.card_image_of_injective _ Fin.succAbove_right_injective
        ext i
        obtain rfl | ⟨i, rfl⟩ := is.castSucc.eq_self_or_eq_succAbove i
        · have : is.castSucc ∉ Ss := fun h ↦ by
            have : s.1 is.castSucc ≤ k.castSucc := by
              simpa using (hs.simplex_fst_le_castSucc_iff is.castSucc).2 (by simp)
            simp_all [Ss]
          simpa
        · simp [hSs]
      · suffices St = Finset.image it.succ.succAbove Sδ ∪ {it.succ} by
          rw [this, Finset.card_union_of_disjoint (by simp),
            Finset.card_image_of_injective _ Fin.succAbove_right_injective,
            Finset.card_singleton]
        ext i
        obtain rfl | ⟨i, rfl⟩ := it.succ.eq_self_or_eq_succAbove i
        · have : it.succ ∈ St := by
            simpa [St, mem_finset_iff] using ht.simplex_fst_succ
          simp [hSt, this]
        · simp [hSt]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).2
      k

Tactic:
· rw [stdSimplex.σ_objMk₁_of_le _ _ (by simpa)]
      rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ i, f i
⊢ #ι * a ≤ ℵ₀ * a

Tactic:
by grw [mk_le_aleph0]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ {0}ᶜ
this : ‖y‖ ≠ 0
⊢ f y ∈ sphere x r

Tactic:
simp [f, norm_smul, abs_of_nonneg hr, mul_assoc, inv_mul_cancel₀ this]

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
hwa : 1 < w a
⊢ 0 < log (w a) / log (v a)

Tactic:
· exact div_pos (log_pos <| hwa) (log_pos (h.one_lt_iff.2 hwa))

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ 0 • f z) x

Tactic:
simpa only [pow_zero, one_smul]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ EqOn f 0 univ

Tactic:
apply eqOn_zero_of_preconnected_of_frequently_eq_zero (fun z _ ↦ hf z) isPreconnected_univ trivial

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] ?m.52, f z = 0

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ 𝕜
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨r, hr⟩ := hf

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
⊢ MeromorphicAt (f ∘ g) x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * ↑n.factorial = ↑n.factorial * (-1) ^ n

Tactic:
Nat.cast_comm

Goal state after:
n : ℕ
⊢ (-1) ^ n * ↑n.factorial = (-1) ^ n * ↑n.factorial
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ -((-↑y) ^ (r + 1) * cexp (↑π * I * r))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x

Tactic:
← neg_mul,

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ -(-↑y) ^ (r + 1) * cexp (↑π * I * r)) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)

Tactic:
Real.deriv_rpow_const t

Goal state after:
c : ℂ
t : ℝ
ht : 0 < t
⊢ c.re * t ^ (c.re - 1) = c.re * t ^ (c.re - 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a b : ℝ
⊢ HasFPowerSeriesOnBall (fun x ↦ (b - a) / (1 - x) + a / (1 - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) 0 1

Tactic:
convert!
    (one_div_one_sub_hasFPowerSeriesOnBall_zero.const_smul (c := b - a)).add
      (one_div_one_sub_sq_hasFPowerSeriesOnBall_zero.const_smul (c := a)) using 2
  · simp [div_eq_mul_inv]
  · ext; simp; ring

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

Tactic:
ext
  · simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]
    exact exists_exists_and_eq_and
  · simp only [mapBilipschitz_packingRadius, NNReal.coe_div, div_div]
  · simp only [mapBilipschitz_coveringRadius, NNReal.coe_mul, mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthInf u ≤ linearGrowthInf v

Tactic:
by
  apply (linearGrowthInf_eventually_monotone h).trans
  rcases eq_bot_or_bot_lt b with rfl | b_bot
  · simp only [add_bot, ← Pi.bot_def, linearGrowthInf_bot, bot_le]
  · apply (linearGrowthInf_add_le' _ _).trans_eq <;> rw [linearGrowthSup_const b_bot.ne' hb]
    · exact add_zero (linearGrowthInf v)
    · exact Or.inr EReal.zero_ne_top
    · exact Or.inr EReal.zero_ne_bot

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthSup u ≤ linearGrowthSup v

Tactic:
by
  apply (linearGrowthSup_eventually_monotone h).trans
  rcases eq_bot_or_bot_lt b with rfl | b_bot
  · simp only [add_bot, ← Pi.bot_def, linearGrowthSup_bot, bot_le]
  · apply (linearGrowthSup_add_le _ _).trans_eq <;> rw [linearGrowthSup_const b_bot.ne' hb]
    · exact add_zero (linearGrowthSup v)
    · exact Or.inr EReal.zero_ne_top
    · exact Or.inr EReal.zero_ne_bot

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
have v_0 := hv.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)
  -- WLOG, `u` is non-bot, and we can apply `mul_le_of_forall_lt_of_nonneg`.
  by_cases u_0 : u = ⊥
  · rw [u_0, linearGrowthSup_bot, mul_bot_of_pos v_0]; exact bot_le
  apply EReal.mul_le_of_forall_lt_of_nonneg v_0.le
    (linearGrowthSup_comp_nonneg h u_0 (tendsto_atTop_of_linearGrowthInf_natCast_pos hv))
  intro a ⟨a_0, a_v⟩ b ⟨b_0, b_u⟩
  apply Frequently.le_linearGrowthSup
  obtain ⟨a', a_a', a_v'⟩ := exists_between a_v
  -- We get an epsilon of room: if `m` is large enough, then `a * n < a' * n ≤ v n`.
  -- Using `b_u`, we can find arbitrarily large values `n` such that `b * n ≤ u n`.
  -- If such an `n` is large enough, then we can find an integer `k` such that
  -- `a'⁻¹ * n ≤ k ≤ a⁻¹ * n`, or, in other words, `a * k ≤ n ≤ a' * k`.
  -- Then `v k ≥ a' * k ≥ n`, so `u (v k) ≥ u n ≥ b * n ≥ b * a * k`.
  have a_top' := ne_top_of_lt a_v'
  have a_0' := a_0.trans a_a'
  have a_a_inv' : a'⁻¹ < a⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0) (Set.mem_Ioi.2 a_0') a_a'
  replace a_v' : ∀ᶠ n : ℕ in atTop, a' * n ≤ v n := by
    filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n a_vn' n_0
    exact (le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le
  suffices h : (∀ᶠ n : ℕ in atTop, a' * n ≤ v n) → ∃ᶠ n : ℕ in atTop, a * b * n ≤ (u ∘ v) n
    from h a_v'
  rw [← frequently_imp_distrib]
  replace b_u := ((frequently_mul_le b_u).and_eventually (eventually_gt_atTop 0)).and_eventually
    <| EReal.eventually_atTop_exists_nat_between a_a_inv' (inv_nonneg_of_nonneg a_0.le)
  refine frequently_atTop.2 fun M ↦ ?_
  obtain ⟨M', aM_M'⟩ := exists_nat_ge_mul a_top' M
  obtain ⟨n, n_M', ⟨bn_un, _⟩, k, an_k', k_an⟩ := frequently_atTop.1 b_u M'
  refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
  · rw [mul_comm a', ← le_div_iff_mul_le a_0' a_top', EReal.div_eq_inv_mul] at aM_M'
    apply Nat.cast_le.1 <| aM_M'.trans <| an_k'.trans' _
    gcongr
  · rw [comp_apply, mul_comm a b, mul_assoc b a]
    rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0' a_top'] at an_k'
    rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an
    have n_vk := Nat.cast_le.1 (an_k'.trans ak_vk')
    exact le_trans (by gcongr) <| bn_un.trans (h n_vk)

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

Goal state before:
pp: case neg.inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
a'A : b ∈ A
ha' : m / τ ≤ δ b
a'_ne_u : b ∉ u
ba'u : b ∈ insert b u
⊢ ∃ c_1 ∈ insert b u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

pp: case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
· refine ⟨b, mem_insert _ _, hcb, ?_⟩
        calc
          δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
          _ = τ * (m / τ) := by field
          _ ≤ τ * δ b := by gcongr

Goal state after:
case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
s t : Set α
ht : MeasurableSet t
⊢ d s = d (s \ t) + d (s ∩ t)

Tactic:
dsimp only [d]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
s t : Set α
ht : MeasurableSet t
⊢ ↑(μ s).toNNReal - ↑(ν s).toNNReal =
    ↑(μ (s \ t)).toNNReal - ↑(ν (s \ t)).toNNReal + (↑(μ (s ∩ t)).toNNReal - ↑(ν (s ∩ t)).toNNReal)