mathlib-initiative/mathlib-tactics huggingface dataset:
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 D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
B :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
S1 : ∀ (t : ℝ), ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ
A :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
⊢ ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ

Tactic:
exact tendsto_nhds_unique A B

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

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
simp [Finset.mul_sum, dist_smul₀]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ Ioc (min a b) (max a b)
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
mem_Ioc

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
⊢ ∑ i ∈ Finset.range n, ↑K * dist (I i).1 (I i).2 = ↑K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2

Tactic:
symm

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
⊢ ↑K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 = ∑ i ∈ Finset.range n, ↑K * dist (I i).1 (I i).2
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: a b : ℝ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
⊢ 1 ≠ 0

Tactic:
decide

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
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
H : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [H] with x hx xs
    have : f = (A.symm ∘ A) ∘ f := by
      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
    rw [this]
    exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : E → F
x y : E
t : 𝕜
n : ℕ
hf : ContDiffAt 𝕜 (↑n + 1) f (x + t • y)
⊢ deriv (fun s ↦ (iteratedFDeriv 𝕜 n f (x + s • y)) fun x ↦ y) t = (iteratedFDeriv 𝕜 (n + 1) f (x + t • y)) fun x ↦ y

Tactic:
have hf' : DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 n f) (x + t • y) := by
    apply hf.differentiableAt_iteratedFDeriv
    norm_cast
    exact lt_add_one n

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : E → F
x y : E
t : 𝕜
n : ℕ
hf : ContDiffAt 𝕜 (↑n + 1) f (x + t • y)
hf' : DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 n f) (x + t • y)
⊢ deriv (fun s ↦ (iteratedFDeriv 𝕜 n f (x + s • y)) fun x ↦ y) t = (iteratedFDeriv 𝕜 (n + 1) f (x + t • y)) fun x ↦ y
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
this : ↑p.2 p.1 - ↑p.2 0 < δ
⊢ ∑ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
      dist ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 <
    δ

Tactic:
by
          convert! this
          rw [← Finset.sum_range_sub]
          congr; ext i
          rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]
          linarith [@hp₁ i (i + 1) (by lia)]

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

Goal state before:
pp: case inr.hvv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ HasDerivAt (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) (deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) t) t

Tactic:
refine DifferentiableOn.hasDerivAt (s := uIoo x₀ x) ?_ (by grind [Ioo_mem_nhds, uIoo])

Goal state after:
case inr.hvv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ DifferentiableOn ℝ (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) (uIoo x₀ x)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k : Tendsto (fun x ↦ (1 - z) * ∑ x ∈ range x, ∑ i ∈ range x, f x * z ^ i) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

Tactic:
range_eq_Ico,

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k : Tendsto (fun x ↦ (1 - z) * ∑ x ∈ Ico 0 x, ∑ x_1 ∈ Ico 0 x, f x * z ^ x_1) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even 2

Tactic:
decide

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

Goal state before:
pp: θ : ℂ
⊢ cexp (θ * I) + cexp (-θ * I) = 0 ↔ cexp (2 * θ * I) = -1

Tactic:
add_eq_zero_iff_eq_neg,

Goal state after:
θ : ℂ
⊢ cexp (θ * I) = -cexp (-θ * I) ↔ cexp (2 * θ * I) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) = sin (a * (↑(x + 1) - 1 / 2) + b) - sin (a * (↑x - 1 / 2) + b)

Tactic:
sin_sub_sin

Goal state after:
case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) =
    2 * sin ((a * (↑(x + 1) - 1 / 2) + b - (a * (↑x - 1 / 2) + b)) / 2) *
      cos ((a * (↑(x + 1) - 1 / 2) + b + (a * (↑x - 1 / 2) + b)) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ sin (a * (↑n - 1 / 2) + b) - sin (a * (↑0 - 1 / 2) + b) = 2 * sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)

Tactic:
sin_sub_sin

Goal state after:
n : ℕ
a b : ℂ
⊢ 2 * sin ((a * (↑n - 1 / 2) + b - (a * (↑0 - 1 / 2) + b)) / 2) *
      cos ((a * (↑n - 1 / 2) + b + (a * (↑0 - 1 / 2) + b)) / 2) =
    2 * sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
rcases le_or_gt x 1 with hxπ | hxπ

Goal state after:
case inl
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ sin x ^ 2 < x ^ 2

case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 1 + 2 / π * x ≤ cos x

Tactic:
simpa using one_sub_mul_le_cos (x := -x) (by linarith) (by linarith)

Goal state after:
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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
y : ℝ
hyS : y ∈ S
hxy : x < y
z : ℝ
hxz : x < z
hzy : z < min b y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

Tactic:
exact ⟨z, ⟨hxz, hzy.trans_le (min_le_left _ _)⟩, hzy.le.trans (min_le_right _ _)⟩

Goal state after:
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
⊢ angle (c • x) (c • y) = angle x y

Tactic:
angle,

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 • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
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 • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y

Tactic:
angle,

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 • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ angle (f u) (f v) = angle u v

Tactic:
angle,

Goal state after:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ arccos (⟪f u, f v⟫ / (‖f u‖ * ‖f v‖)) = angle u v
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ arccos (⟪f u, f v⟫ / (‖f u‖ * ‖f v‖)) = angle u v

Tactic:
angle,

Goal state after:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ arccos (⟪f u, f v⟫ / (‖f u‖ * ‖f v‖)) = arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
angle,

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
angle,

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = π

Tactic:
angle,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ 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
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0

Tactic:
angle,

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Tactic:
by
  refine ⟨fun h => ?_, inner_eq_mul_norm_of_angle_eq_zero⟩
  have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
  rw [angle, h, div_self h₁, Real.arccos_one]

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ‖↑z‖ ≠ ‖1‖

Tactic:
simp [z.norm_ne_one]

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

Goal state before:
pp: case refine_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
n : ℕ
x✝ :
  ∃ 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
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
⊢ ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)

Tactic:
have : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ f ⁻¹' (q e).target := by
    rintro ⟨t0, a'⟩ ⟨ht, ha⟩
    rw [Set.mem_singleton_iff] at ha; dsimp only at ha
    rw [← g_lifts, hpq e, ha]
    exact (q e).map_source (h_sub ht)

Goal state after:
case refine_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
n : ℕ
x✝ :
  ∃ 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
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
⊢ ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)
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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
⊢ f =ᶠ[𝓝 x] g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE h
      let h₁f := cs
      rw [hf.meromorphicOrderAt_eq_zero_iff] at h₁f
      let h₁g := cs
      rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g
      simp only [not_not] at *
      rw [h₁f, h₁g]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f / g) x

Tactic:
rw [div_eq_mul_inv]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₂

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₁]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ ∀ (a : 𝕜), f₁ a = 0 → (f₁ + f₂) a = f₂ a
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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • g z
⊢ g =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with y hy using by simp [hy]

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

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
this✝ : 0 = (x - x) ^ n • g x
this : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x
⊢ (fun z ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with y hy using by simp [hy]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ meromorphicOrderAt (fun x_1 ↦ x_1 - x) x = 1

Tactic:
rw [← WithTop.coe_one, ← meromorphicOrderAt_zpow_id_sub_const (𝕜 := 𝕜), zpow_one]

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

Goal state before:
pp: case left
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ a ∈ ball 0 R

Tactic:
(by_contra; aesop)

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

Goal state before:
pp: case right
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ b ∈ ball 0 R

Tactic:
(by_contra; aesop)

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ g ↑⟨u, hu⟩ ≠ 0

Tactic:
← (hg hu).meromorphicOrderAt_eq_zero_iff,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ meromorphicOrderAt g u = 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
x✝ : ↑I × ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) x✝ = ((↑γ).comp ContinuousMap.prodSwap) x✝

Tactic:
apply Γ_lifts

Goal state after: