mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm y =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
rw [← mfderiv_comp_mfderivWithin]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ mfderiv[range ↑I] (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ MDiffAt ↑(extChartAt I x) (↑(extChartAt I x).symm y)

case hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ MDiffAt[range ↑I] ↑(extChartAt I x).symm y

case hxs
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ UniqueMDiffAt[range ↑I] y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))] id

Tactic:
let t := I.symm ⁻¹' (chartAt H x).target ∩ range I
      have : EqOn (writtenInExtChartAt I I (Sum.inr x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inr,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inl_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)
      apply Filter.eventually_of_mem ?_ this
      rw [Filter.inter_mem_iff]
      refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
      exact (chartAt H x).open_target.mem_nhds (by simp)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α := ⋯
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
n : ℕ
hn : eball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
h : ∀ (n : ℕ) (i : ι), x ∉ D n i
⊢ x ∈ D n (ind x)

Tactic:
exact memD.2 ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_eball_self (pow_pos _)⟩

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), (f i) x = 1
⊢ ∃ i, 0 < (f i) x

Tactic:
contrapose! H

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), (f i) x ≤ 0
⊢ ∑ᶠ (i : ι), (f i) x ≠ 1
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
have : Nonempty (PartialRefinement u s ⊤) :=
    ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩

Goal state after:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this : Nonempty (PartialRefinement u s ⊤)
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
ht : IsSeparable t
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ f =ᵐ[μ] 0

Tactic:
rcases ht with ⟨d, d_count, hd⟩
  have : Encodable d := d_count.toEncodable
  have : ∀ x : d, ∃ g : StrongDual 𝕜 E, ‖g‖ ≤ 1 ∧ g x = ‖(x : E)‖ :=
    fun x => exists_dual_vector'' 𝕜 (x : E)
  choose s hs using this
  have A : ∀ a : E, a ∈ t → (∀ x, ⟪a, s x⟫ = (0 : 𝕜)) → a = 0 := by
    intro a hat ha
    contrapose! ha
    have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]
    have a_mem : a ∈ closure d := hd hat
    obtain ⟨x, hx⟩ : ∃ x : d, dist a x < ‖a‖ / 2 := by
      rcases Metric.mem_closure_iff.1 a_mem (‖a‖ / 2) (half_pos a_pos) with ⟨x, h'x, hx⟩
      exact ⟨⟨x, h'x⟩, hx⟩
    use x
    have I : ‖a‖ / 2 < ‖(x : E)‖ := by
      have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
      have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at hx
      linarith
    intro h
    apply lt_irrefl ‖s x x‖
    calc
      ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, map_sub]
      _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
      _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
      _ < ‖(x : E)‖ := I
      _ = ‖s x x‖ := by simp [(hs x).2]
  have hfs : ∀ y : d, ∀ᵐ x ∂μ, ⟪f x, s y⟫ = (0 : 𝕜) := fun y => hf (s y)
  have hf' : ∀ᵐ x ∂μ, ∀ y : d, ⟪f x, s y⟫ = (0 : 𝕜) := by rwa [ae_all_iff]
  filter_upwards [hf', h't] with x hx h'x
  exact A (f x) h'x hx

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • w) - f x - ρ • L w‖ =
    ‖f (x + ρ • w) - f (x + ρ • y) + (ρ • L y - ρ • L w) + (f (x + ρ • y) - f x - ρ • L y)‖

Tactic:
by congr; abel

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ 1 / 2 * ‖x + y‖ ≠ 1

Tactic:
one_div,

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ 2⁻¹ * ‖x + y‖ ≠ 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ univ fun x ↦ x ^ n

Tactic:
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)

Goal state after:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a ↦ a ^ n)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx : x ≠ 0
⊢ log x / (2 * √x) + (√x)⁻¹ = 1 / (2 * √x) * log x + 1 / √x

Tactic:
one_div,

Goal state after:
case e'_9
x : ℝ
hx : x ≠ 0
⊢ log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + 1 / √x
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx : x ≠ 0
⊢ log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + 1 / √x

Tactic:
one_div,

Goal state after:
case e'_9
x : ℝ
hx : x ≠ 0
⊢ log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + (√x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 := by
    rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul,
      add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
    ring_nf

Goal state after:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ θ = ↑(k + 1) * ↑π

Tactic:
simp [eq_add_of_sub_eq hk]

Goal state after:
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π / 2 + ↑π / 2 = (↑k + 1) * ↑π
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
hdVW : Disjoint V W
⊢ U ⊆ V

Tactic:
have hUVW : U ⊆ V ∪ W := fun x hx =>
    (eq_or_ne ‖f x‖ ‖f c‖).imp (fun h => ⟨hx, fun y hy => (hm hy).out.trans_eq h.symm⟩)
      (And.intro hx)

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
hdVW : Disjoint V W
hUVW : U ⊆ V ∪ W
⊢ U ⊆ V
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
have hc : IsCompact (closure U) := hb.isCompact_closure

Goal state after:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)

Tactic:
one_div,

Goal state after:
x : ℝ
⊢ cos (arctan x) ^ 2 = (1 + x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) = 1 / √(1 + x ^ 2)

Tactic:
one_div,

Goal state after:
x : ℝ
⊢ cos (arctan x) = (√(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h

Goal state after:
case inr
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
y : ℝ
hyS : y ∈ S
hyx : y < x
z : ℝ
hyz : max a y < z
hzx : z < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

Tactic:
exact ⟨z, ⟨(le_max_left _ _).trans_lt hyz, hzx⟩, (le_max_right _ _).trans hyz.le⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
have hxs' := hxs
  rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'
  obtain ⟨a, b, hxab, habs⟩ := hxs'
  simp_rw [hasDerivWithinAt_iff_tendsto_slope]
  simp only [mem_Iio, lt_self_iff_false, not_false_eq_true, sdiff_singleton_eq_self]
  have h : Ioo a x ⊆ {y | y ∈ S ∧ y < x} := fun z hz ↦ ⟨habs ⟨hz.1, hz.2.trans hxab.2⟩, hz.2⟩
  have h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x))) :=
    ((monotoneOn_slope_lt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_left
      (by simpa using hxab.1) ((bddAbove_slope_gt_of_mem_interior hfc hxs).mono (image_mono h))
  suffices sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y ∈ S | y < x}) by rwa [← this]
  apply (monotoneOn_slope_lt hfc (habs hxab)).csSup_eq_of_subset_of_forall_exists_le
    (bddAbove_slope_gt_of_mem_interior hfc hxs) h ?_
  rintro y ⟨hyS, hyx⟩
  obtain ⟨z, hyz, hzx⟩ := exists_between (max_lt hxab.1 hyx)
  exact ⟨z, ⟨(le_max_left _ _).trans_lt hyz, hzx⟩, (le_max_right _ _).trans hyz.le⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2))

Tactic:
by
  rw [two_mul, arctan_add (by nlinarith)]; congr 1; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y ^ 2 + 1 < 1 / (1 + tan y ^ 2)⁻¹

Tactic:
one_div,

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y ^ 2 + 1 < (1 + tan y ^ 2)⁻¹⁻¹
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
Real.norm_eq_abs,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ arccos (r * ⟪x, y⟫ / (‖x‖ * (‖r‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
Real.norm_eq_abs,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ arccos (r * ⟪x, y⟫ / (‖x‖ * (|r| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)),
    ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 ↔ ⟪x, y⟫ = 0
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
p : 𝕜[X]
⊢ IsCoveringMapOn (fun x ↦ eval x p) ((fun x ↦ eval x p) '' {k | eval k (derivative p) = 0})ᶜ

Tactic:
refine p.isClosedMap_eval.isCoveringMapOn_of_isLocalHomeomorphOn (fun x hx ↦ ?_)
    fun x hx ↦ ⟨_, ((p.hasStrictDerivAt x).hasStrictFDerivAt_equiv
      fun h ↦ hx ⟨x, h, rfl⟩).mem_toOpenPartialHomeomorph_source, by simp⟩
  obtain rfl | ne := eq_or_ne p (C x)
  · simp at hx
  · simpa only [preimage_eval_singleton ne] using rootSet_finite ..

Goal state after:
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → 𝔻
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ+
⊢ 0 ∉ UnitDisc.coe ∘ g '' U

Tactic:
by simpa using hU₀

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0

Tactic:
simp [hf, Pi.zero_def]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
⊢ divisor f₁ U = divisor f₂ U

Tactic:
ext z
  by_cases hz : z ∉ U
  · simp_all
  rw [not_not] at hz
  rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz]
  congr 1
  apply meromorphicOrderAt_congr
  apply (hf₁ z hz).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
    (hf₂ z hz) hz hU h

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : ¬n = 0
hz : z ∈ U
⊢ (divisor (f ^ n) U) z = (n • divisor f U) z

Tactic:
simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]

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

Goal state before:
pp: case right.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
⊢ (g • g_f) x ≠ 0

Tactic:
simp [smul_ne_zero h₂g h₂g_f]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (ball (c - c) R)) z = (divisor f (ball 0 R)) z

Tactic:
sub_self

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (ball 0 R)) z = (divisor f (ball 0 R)) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (closedBall (c - c) R)) z = (divisor f (closedBall 0 R)) z

Tactic:
sub_self

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (closedBall 0 R)) z = (divisor f (closedBall 0 R)) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (sphere (c - c) R)) z = (divisor f (sphere 0 R)) z

Tactic:
sub_self

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (sphere 0 R)) z = (divisor f (sphere 0 R)) z
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
⊢ ⋯.choose =ᶠ[𝓝 x] g

Tactic:
rw [← h'₁.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₁g.continuousAt]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
⊢ ⋯.choose =ᶠ[𝓝[≠] x] g