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

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)

Tactic:
simp only [mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ

Tactic:
VectorBundleCore.inCoordinates_eq

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ (tangentBundleCore I' H').coordChange ((tangentBundleCore I' H').indexAt y) ((tangentBundleCore I' H').indexAt y₀)
        y ∘SL
      ϕ ∘SL
        (tangentBundleCore I H).coordChange ((tangentBundleCore I H).indexAt x₀) ((tangentBundleCore I H).indexAt x) x =
    ϕ

case hx
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ x ∈ (tangentBundleCore I H).baseSet ((tangentBundleCore I H).indexAt x₀)

case hy
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ y ∈ (tangentBundleCore I' H').baseSet ((tangentBundleCore I' H').indexAt y₀)
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ↑(extChartAt I x).symm (↑(extChartAt I x) x) ∈
    ⇑(Equiv.refl M) ⁻¹' (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M) x)).source

Tactic:
simp only [mfld_simps]

Goal state after:
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
hcomp : mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))

Tactic:
simpa using! hcomp

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

Goal state before:
pp: case refine_2
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst✝²] (E a)
hE : ⋃ i, E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
⊢ ∃ t ∈ 𝓝 (x, y), {i | ((fun z ↦ U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ t).Nonempty}.Finite

Tactic:
rcases hEf y with ⟨t, ht, htf⟩
      refine ⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩
      refine (htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_
      rintro ⟨b, a, ha⟩ ⟨⟨c, d⟩, ⟨-, hd : d ∈ E b⟩, -, hdt : d ∈ t⟩
      exact mem_iUnion₂.2 ⟨b, ⟨d, hd, hdt⟩, mem_range_self _⟩

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

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ tsupport ⇑(f c)
this : g c (↑(chartAt H c) x) = 0
⊢ (f c) x * g c (↑(chartAt H c) x) = 0

Tactic:
simp only [this, mul_zero]

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

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ tsupport ⇑(f c)
this : g c (↑(chartAt H c) x) = 0
⊢ (f c) x * g c (↑(chartAt H c) x) = 0

Tactic:
by simp only [this, mul_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝¹ : FiniteDimensional 𝕜 E
this✝ : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I✝ : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝
L'_cont : Continuous ⇑L'
A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm
I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))
μS : Measure ↥S := addHaar
μT : Measure ↥T := addHaar
c₀ : ℝ≥0∞
c₀_pos : c₀ ≠ 0
c₀_fin : c₀ ≠ ∞
h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT
J : map (⇑P) (μS.prod μT) = μS univ • μT
this : (map (⇑L') μT).IsAddHaarMeasure
⊢ ↑((map (⇑L') μT).addHaarScalarFactor ν) ≠ 0

Tactic:
simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μT.map L') ν).ne'

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun x ↦ ↑C * ‖v‖ * ‖g x‖) a

Tactic:
have t_pos : 0 < t := ht.1

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
t_pos : 0 < t
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun x ↦ ↑C * ‖v‖ * ‖g x‖) a
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ (n : ℕ), ‖d n‖ ≤ u n

Tactic:
by simpa [dist_eq_norm] using hvu

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

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ Tendsto ?m.14 (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using Tendsto.add hf hg

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

Goal state before:
pp: case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
f : ℝ → E
hf : ContDiffOn ℝ (↑0) f s
⊢ (fun x ↦ f x - taylorWithinEval f 0 s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ 0

Tactic:
simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]

Goal state after:
case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
f : ℝ → E
hf : ContDiffOn ℝ (↑0) f s
⊢ Filter.Tendsto (fun x ↦ f x - f x₀) (𝓝[s] x₀) (𝓝 0)
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
· exact (subsingleton_closedBall x hr).strictConvex

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Tactic:
have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx
    convert!
      (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
          mul_ne_zero two_ne_zero h₀).deriv using 1
    nth_rw 3 [← mul_self_sqrt hx.le]
    field

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

Goal state before:
pp: x y : ℂ
⊢ (∃ k, y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ∨ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2) ↔
    ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x

Tactic:
refine exists_congr fun k => or_congr ?_ ?_ <;> refine Eq.congr rfl ?_

Goal state after:
case refine_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x

case refine_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℝ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ k, ↑k * π = θ

Tactic:
revert hθ

Goal state after:
θ : ℝ
⊢ cos θ ≠ 0 → (tan θ = 0 ↔ ∃ k, ↑k * π = θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ arctan (-x) = -arctan x

Tactic:
by simp [arctan_eq_arcsin, neg_div]

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

Goal state before:
pp: case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

Tactic:
tan_zero

Goal state after:
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case e'_4
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ 1 / √(x ^ 2 + 1) = 1 / √((-x) ^ 2 + 1)

Tactic:
neg_sq

Goal state after:
case e'_4
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ 1 / √(x ^ 2 + 1) = 1 / √(x ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
exact k

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

Goal state before:
pp: x : ℝ
⊢ angle (cexp (↑x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|

Tactic:
by
  simpa using angle_exp_exp x 0

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

Goal state before:
pp: case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
have := @this (x / y) 1 (by simp only [norm_div, hx, hy, div_one]) norm_one rfl

Goal state after:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case ho.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
w : ℂ
hw : w ∈ {c}ᶜ
⊢ (fun x ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w = (fun z ↦ (z - c)⁻¹) w

Tactic:
mem_compl_singleton_iff,

Goal state after:
case ho.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
w : ℂ
hw : w ≠ c
⊢ (fun x ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w = (fun z ↦ (z - c)⁻¹) w
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
⊢ EqOn f (fun z ↦ f c + (z - c) • dslope f c z₀) (ball c R₁)

Tactic:
set e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
  set g := dslope (e ∘ f) c
  rintro z hz
  have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
  have hg' : g = e ∘ dslope f c := by
    ext w
    simp only [g]
    rw [e.dslope_comp, Function.comp_apply]
    rintro rfl
    exact hd.differentiableAt <| ball_mem_nhds _ h_R₁
  have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
    norm_dslope_le_div_of_mapsTo_ball (e.differentiable.comp_differentiableOn hd)
      (fun w hw ↦ by simpa [e] using h_maps hw) hz
  have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
    isMaxOn_iff.mpr fun z hz => by simpa [h_eq, hg', e] using g_le_div z hz
  have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
    (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr
      (e.differentiable.comp_differentiableOn hd)
  have heq : ‖dslope f c z‖ = ‖dslope f c z₀‖ := by
    simpa [hg', e] using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
      isOpen_ball g_diff h_z₀ g_max hz
  have heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖ := by
    simpa [hg', e, ← UniformSpace.Completion.coe_add]
      using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
        isOpen_ball (g_diff.add_const (g z₀)) h_z₀ g_max.norm_add_self hz
  have : dslope f c z = dslope f c z₀ := eq_of_norm_eq_of_norm_add_eq heq <| by
    simp only [heq, SameRay.rfl.norm_add, heq_add]
  simp [← this]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this :
  ∀ (n : ℕ),
    ∃ N,
      a ∈ N ∧
        IsOpen[inst✝] N ∧
          ∃ g',
            ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
              p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x✝ : ↑I × A → E
a✝ : ↑I
⊢ x✝ (a✝, a) = g (a✝, a) ↔ a✝ ≤ 1 → x✝ (a✝, a) = g (a✝, a)

Tactic:
· rw [imp_iff_right]; exact le_top

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

Goal state before:
pp: case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

pp: case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left✝ : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right✝ : f x = 0
⊢ AnalyticAt 𝕜 f x

Tactic:
· exact h

Goal state after:
case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left✝ : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right✝ : f x = 0
⊢ AnalyticAt 𝕜 f x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑(Exists.choose hf)) • g z

Tactic:
rw [eventually_nhdsWithin_iff]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ (↑m - ↑(Exists.choose hf)) • g x_1
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : ¬meromorphicOrderAt f x = 0
hn : n = 0
⊢ False

Tactic:
rw [hn] at this

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑0
h₃f : ¬meromorphicOrderAt f x = 0
hn : n = 0
⊢ False
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
⊢ 0 < ‖g x‖

Tactic:
by simp [gx]

Goal state after: