mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : DivisionSemiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : (𝓝[≠] 0).NeBot
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (I.pi s) x

Tactic:
rw [← Set.univ_pi_piecewise_univ]
  refine UniqueDiffWithinAt.univ_pi fun i => ?_
  by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]

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

Goal state before:
pp: case iUnion
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst✝²] s → ∫ (x : β) in s, f x ∂μ = 0
A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0
s : Set β
g : ℕ → Set β
g_disj : Pairwise (Function.onFun Disjoint g)
g_meas : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), ∫ (x : β) in g i, f x ∂μ = 0
⊢ ∫ (x : β) in ⋃ i, g i, f x ∂μ = 0

Tactic:
simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
v : E
hvs : v ∈ s
hv : dist x v < (1 / (2 * ‖c‖)) ^ n
⊢ ∃ d, x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
use v - x

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
v : E
hvs : v ∈ s
hv : dist x v < (1 / (2 * ‖c‖)) ^ n
⊢ x + (v - x) ∈ s ∧ ‖v - x‖ < (1 / (2 * ‖c‖)) ^ n
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
⊢ (fun x ↦ deriv p x - deriv q x) =ᵐ[volume.restrict (uIoc a b)] deriv (p - q)

Tactic:
Filter.EventuallyEq,

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 : ℝ) ∂volume.restrict (uIoc a b), deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_2.x.e_f
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
t : ℝ
⊢ ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -((deriv (fun x_1 ↦ (x - x_1) ^ (n + 1)) t / ↑(n.succ * n !)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)

Tactic:
deriv_fun_pow (by fun_prop),

Goal state after:
case e'_2.x.e_f
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
t : ℝ
⊢ ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -((↑(n + 1) * (x - t) ^ (n + 1 - 1) * deriv (HSub.hSub x) t / ↑(n.succ * n !)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] t)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, ↑x ∈ stolzSet M

Tactic:
simp only [eventually_iff, mem_nhdsWithin]

Goal state after:
M : ℝ
hM : 1 < M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x | ↑x ∈ stolzSet M}
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ a ∈ Finset.range p.1, (edist (f (↑p.2 (a + 1))) (f (↑p.2 a))).toReal =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))

Tactic:
simp_rw [← dist_edist]

Goal state after:
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ x_1 ∈ Finset.range p.1, dist (f (↑p.2 (x_1 + 1))) (f (↑p.2 x_1)) =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hv'.h
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
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] =ᵐ[MeasureTheory.volume.restrict (Ι x₀ x)]
    deriv fun t ↦ iteratedDerivWithin k f [[x₀, x]] t

Tactic:
Filter.EventuallyEq,

Goal state after:
case inr.hv'.h
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
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Ι x₀ x),
    iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
rcases h with ⟨hx, hy, hne⟩

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Convex

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
⊢ 4 - ε ^ 2 < 2 ^ 2

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 - (2 - √(4 - ε ^ 2))

Tactic:
· norm_num
      exact pow_pos hε _

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 - (2 - √(4 - ε ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

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

Tactic:
contrapose!

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

Goal state before:
pp: θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π

Tactic:
contrapose!

Goal state after:
θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑π / 2 ≠ θ

Tactic:
contrapose!

Goal state after:
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑π / 2 ≠ θ

Tactic:
by
  contrapose!; exact tan_eq_zero_iff

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

Goal state before:
pp: x y : ℂ
⊢ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ sin ((x + y) / 2) = 0 ∨ sin ((x - y) / 2) = 0

Tactic:
simp [(by simp : (2 : ℂ) ≠ 0)]

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

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ sin (a / 2) * ∑ i ∈ Finset.range n, sin (a * ↑i + b) = sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
by
  apply mul_left_cancel₀ (show (-2 : ℂ) ≠ 0 by simp)
  simp_rw [← mul_assoc, mul_sum]
  calc
    ∑ i ∈ range n, -2 * sin (a / 2) * sin (a * i + b)
      = ∑ x ∈ range n, (cos (a * (↑(x + 1) - 1 / 2) + b) - cos (-(a * (x - 1 / 2) + b))) := by
      congr! 1 with x hx
      rw [cos_sub_cos]
      push_cast
      ring_nf
    _ = -2 * sin (n * a / 2) * sin ((n - 1) * a / 2 + b) := by
      simp_rw [cos_neg, sum_range_sub (fun i ↦ cos (a * (i - 1 / 2) + b)), cos_sub_cos]
      ring_nf

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

Goal state before:
pp: case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C

Tactic:
calc
    ‖f z‖ = ‖f (e 0)‖ := by simp only [e, lineMap_apply_zero]
    _ ≤ ‖f (e ζ)‖ := hζ (subset_closure h₀)
    _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
⊢ BddBelow (slope f x '' {y | y ∈ s ∧ x < y})

Tactic:
refine bddBelow_iff_subset_Ici.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ x < y}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ x < y}
hz' : slope f x z = y'
⊢ y' ∈ Ici (slope f x y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖

Tactic:
rw [Complex.norm_exp_I_mul_ofReal_sub_one]

Goal state after:
x : ℝ
⊢ ‖2 * sin (x / 2)‖ ≤ ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ 2 * |x / 2| = ‖x‖

Tactic:
rw [abs_div, Nat.abs_ofNat, Real.norm_eq_abs]; ring

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
⊢ arccos (c * (c * ⟪x, y⟫) / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
← mul_assoc c c,

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 * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ DifferentiableOn ℂ (fun {z} ↦ f z / (2 * ↑M - f z)) (ball 0 R)

Tactic:
apply hf.div (hf.const_sub _) fun x hx h ↦ ?_

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
x : ℂ
hx : x ∈ ball 0 R
h : 2 * ↑M - f x = 0
⊢ False
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 = π

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

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ AntitoneOn (derivWithin f S) S

Tactic:
by
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with rfl | hxy'
  · rfl
  exact (hfc.derivWithin_le_slope hx hy hxy' (hfd y hy)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd x hx))

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = 1 ↔ angle x y = 0

Tactic:
rw [← cos_zero]
  exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (left_mem_Icc.2 pi_pos.le)

Goal state after:
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₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ ‖dslope f c z‖ = ‖dslope f c z₀‖

Tactic:
simpa [hg', e] using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
      isOpen_ball g_diff h_z₀ g_max hz

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

Goal state before:
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
h' : ¬AnalyticAt 𝕜 f x
⊢ False

Tactic:
exact lt_irrefl 0 (lt_of_le_of_lt h₂f h₃f)

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

Goal state before:
pp: 𝕜 : 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
y : 𝕜
h₁y : (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0

Tactic:
← sub_eq_zero,

Goal state after:
𝕜 : 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
y : 𝕜
h₁y : (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y - (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y = 0
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
← zpow_neg,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ g y = ((y - x) ^ (-(meromorphicOrderAt f x).untop₀) * (y - x) ^ (meromorphicOrderAt f x).untop₀) • g y
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 : 𝕜 → E
h₁ : ¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Tactic:
· aesop

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.refine_4
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
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
ta : ↑I × A
x✝ :
  ta ∈
    Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source)) ∩
      closure[instTopologicalSpaceProd] {a | a.1 ≤ t n}
hta : ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun y ↦ (t n, y)) ⁻¹' (q e).source))
ht : ta ∈ {b | b.1 ≤ t n}
⊢ ta ∈ Set.Icc 0 (t n) ×ˢ N

Tactic:
exact ⟨⟨hta.1.1, ht⟩, hta.2.2.1⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
⊢ MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U = D

Tactic:
ext z
  by_cases hz : z ∈ U
  <;> simp [(meromorphicNFOn D U).meromorphicOn, hz, meromorphicOrderAt_eq D hD]

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

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w -
      (meromorphicOrderAt (fun z ↦ ↑R) w + meromorphicOrderAt (fun z ↦ z - w) w) =
    -1

Tactic:
have : meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w = 0 := by
    refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
    · apply AnalyticAt.meromorphicNFAt
      fun_prop
    · rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
      rw [mem_ball_iff_norm, sub_zero] at h
      grind

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
this : meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w = 0
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w -
      (meromorphicOrderAt (fun z ↦ ↑R) w + meromorphicOrderAt (fun z ↦ z - w) w) =
    -1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖

Tactic:
rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖∏ i ∈ Finite.toFinset h, (x - i) ^ update d x 0 i‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖