mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
⊢ AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in c..x, f v) a b

Tactic:
let s := fun E : ℕ × (ℕ → ℝ × ℝ) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
  have : Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0) :=
    tendsto_setLIntegral_zero
    (ne_of_lt <| intervalIntegrable_iff.mp h |>.hasFiniteIntegral)
    (tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero _ _)
  -- Step 2: Use the lintegral in Step 1 to bound the sum of the distances between
  -- `∫ v in c..(E.2 i).2, f v` and `∫ v in c..(E.2 i).2, f v` that occurs in the definition
  -- of absolutely continuous.
  have := ENNReal.toReal_zero ▸ (ENNReal.continuousAt_toReal (by simp)).tendsto.comp this
  refine squeeze_zero' ?_ ?_ this
  · filter_upwards with (n, I)
    exact Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)
  simp only [comp_apply, s]
  have : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
      E ∈ disjWithin a b :=
    eventually_inf_principal.mpr (by simp)
  filter_upwards [this] with (n, I) hnI
  obtain ⟨hnI1, hnI2⟩ := mem_ofPred_eq ▸ hnI
  simp only
  rw [← integral_norm_eq_lintegral_enorm (h.aestronglyMeasurable_restrict_uIoc.restrict),
      integral_biUnion_finset _ (by simp +contextual [uIoc]) hnI2]
  · refine Finset.sum_le_sum (fun i hi ↦ ?_)
    rw [Real.dist_eq,
        intervalIntegral.integral_interval_sub_left
          (by apply IntervalIntegrable.mono_set' h; grind [uIoc, uIcc])
          (by apply IntervalIntegrable.mono_set' h; grind [uIoc, uIcc]),
        Measure.restrict_restrict_of_subset
          (uIoc_subset_of_mem_disjWithin hnI (Finset.mem_range.mp hi)),
        intervalIntegral.integral_symm, abs_neg,
        intervalIntegral.abs_intervalIntegral_eq]
    exact abs_integral_le_integral_abs
  · intro i hi
    unfold IntegrableOn
    have h_subset := uIoc_subset_of_mem_disjWithin hnI (Finset.mem_range.mp hi)
    rw [Measure.restrict_restrict_of_subset h_subset]
    exact IntegrableOn.mono_set h.def'.norm h_subset |>.integrable

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

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

Tactic:
by
  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
  rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]
  refine exists_congr fun x => ?_
  refine (iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)
  ring

Goal state after:
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
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U

Tactic:
by
  set V := U ∩ {z | IsMaxOn (norm ∘ f) U z}
  have hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖ := fun x hx => le_antisymm (hm hx.1) (hx.2 hcU)
  suffices U ⊆ V from fun x hx => hV x (this hx)
  have hVo : IsOpen V := by
    simpa only [ho.mem_nhds_iff, ofPred_and, ofPred_mem_eq]
      using isOpen_setOfPred_mem_nhds_and_isMaxOn_norm hd
  have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, hm⟩
  set W := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
  have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
  have hdVW : Disjoint V W := disjoint_left.mpr fun x hxV hxW => hxW.2 (hV x hxV)
  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)
  exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c

Tactic:
have h1 : ∀ᶠ z in 𝓝 c, f z ≠ 0 := hf.self_of_nhds.continuousAt.eventually_ne h

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
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
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hwU : w ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
closure_eq_interior_union_frontier,

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)
w : E
hwU : w ∈ interior U ∪ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
h : cos x ≠ -1
| cos x

Tactic:
← mul_div_cancel₀ x two_ne_zero,

Goal state after:
x : ℂ
h : cos x ≠ -1
| cos (2 * (x / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
| sin x

Tactic:
← mul_div_cancel₀ x two_ne_zero,

Goal state after:
x : ℂ
| sin (2 * (x / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case neg
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + tan (x / 2) ^ 2)

Tactic:
rw [div_eq_mul_inv (2 * tan (x / 2)) (1 + tan (x / 2) ^ 2), inv_one_add_tan_sq h,
      ← tan_mul_cos h]
    ring

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

Goal state before:
pp: x : ℂ
| tan x

Tactic:
← mul_div_cancel₀ x two_ne_zero,

Goal state after:
x : ℂ
| tan (2 * (x / 2))
Module: Mathlib.Analysis.Complex.Angle

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

Tactic:
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
this : ‖x - y‖ / 1 ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

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
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0

Tactic:
div_one,

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‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

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 (1 * y)) (angle x (1 * y))
⊢ y ≠ 0
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
    rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul]
      at this
    rintro rfl
    simp at hy

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ IsMinOn f S x

Tactic:
by
  refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_
  exact hf_ld.symm.le.trans (hf.leftDeriv_le_rightDeriv_of_mem_interior hx)

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

Goal state before:
pp: case refine_2
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 : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

Tactic:
by_cases hz : z ∈ U
    · simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]
    · simp [hz, ← cpow_mul_nat, hn]

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

Goal state before:
pp: z : 𝕔𝔻
⊢ ‖↑z‖ ≤ 1

Tactic:
exact z.norm_le_one

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
hf : ¬MeromorphicOn f U
⊢ (divisor f U) z = 0

Tactic:
by
  unfold divisor
  aesop

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 : 𝕜
⊢ E

Tactic:
by_cases h₁ : MeromorphicAt f x
  · by_cases h₂ : meromorphicOrderAt f x = ⊤
    · exact 0
    · exact ((meromorphicOrderAt_ne_top_iff h₁).1 h₂).choose x
  · exact 0

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : z ∈ univ
⊢ AnalyticAt 𝕜 (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d z 0 u) z ∧
    (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d z 0 u) z ≠ 0 ∧
      (fun x ↦ x - z) ^ d z * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d z 0 u =ᶠ[nhds z]
        (fun x ↦ x - z) ^ d z • ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d z 0 u

Tactic:
simp [analyticAt, ne_zero]

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

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
⊢ AnalyticAt 𝕜 f x

Tactic:
have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
    apply this.congr
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h']
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] with y hy using by simp [hy]

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

Goal state before:
pp: case inl
R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ MeromorphicNFAt (canonicalFactor R z) z

pp: case inr
R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
hz : z ∈ univ
h₁ : z ≠ w
⊢ MeromorphicNFAt (canonicalFactor R w) z

Tactic:
· rw [meromorphicNFAt_iff_analyticAt_or]
    right
    refine ⟨meromorphic_canonicalFactor R z z, ?_, by simp⟩
    simpa [meromorphicOrderAt_canonicalFactor h] using WithTop.coe_lt_zero.mpr (by lia : -1 < 0)

Goal state after:
case inr
R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
hz : z ∈ univ
h₁ : z ≠ w
⊢ MeromorphicNFAt (canonicalFactor R w) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ i ∈ η₀.toFinset, divisor (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)

Tactic:
divisor_zpow (fun z hz ↦ meromorphic_canonicalFactor R _ z)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ x ∈ η₀.toFinset, (divisor f (ball 0 R)) x • divisor (canonicalFactor R x) (ball 0 R) = -divisor f (ball 0 R)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ η₀.toFinset
x : ℂ
hx : x ∈ ball 0 R
⊢ meromorphicOrderAt (canonicalFactor R z ^ (divisor f (ball 0 R)) z) x ≠ ⊤

Tactic:
meromorphicOrderAt_zpow (meromorphic_canonicalFactor R z x)

Goal state after:
case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ η₀.toFinset
x : ℂ
hx : x ∈ ball 0 R
⊢ ↑((divisor f (ball 0 R)) z) * meromorphicOrderAt (canonicalFactor R z) x ≠ ⊤
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C(↑I, A)) → γ 0 = a₀ → C(↑I, E)
Γ_0 : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), (Γ γ a) 0 = e₀
F : A → E := fun a ↦ (Γ (somePath a₀ a).toContinuousMap ⋯) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph ↑p
he : ↑p e₀ = f a₀
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → ↑p ∘ ⇑Γ = ⇑(f.comp γ) → ↑p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
Γ_lifts : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), ↑p ∘ ⇑(Γ γ a) = ⇑(f.comp γ)
this : ∀ (a : A), ↑p (F a) = f a
hfap : f a ∈ p.target
U : Set A
haU : U ∈ 𝓝 a
U_conn : IsPathConnected U
hUp : id U ⊆ ⇑f ⁻¹' p.target
x : A
hxU : x ∈ U
γ : Path a x
hγ : ∀ (t : ↑I), γ t ∈ U
⊢ x ∈ {x | (fun x ↦ (↑p.symm ∘ ⇑f) x = F x) x}

Tactic:
let Γ' : Path e₀ ((p.symm ∘ f) a) :=
      ⟨Γ _ (somePath a₀ a).source, Γ_0 .., by simp [← this, hep, F]⟩

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C(↑I, A)) → γ 0 = a₀ → C(↑I, E)
Γ_0 : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), (Γ γ a) 0 = e₀
F : A → E := fun a ↦ (Γ (somePath a₀ a).toContinuousMap ⋯) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph ↑p
he : ↑p e₀ = f a₀
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → ↑p ∘ ⇑Γ = ⇑(f.comp γ) → ↑p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
Γ_lifts : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), ↑p ∘ ⇑(Γ γ a) = ⇑(f.comp γ)
this : ∀ (a : A), ↑p (F a) = f a
hfap : f a ∈ p.target
U : Set A
haU : U ∈ 𝓝 a
U_conn : IsPathConnected U
hUp : id U ⊆ ⇑f ⁻¹' p.target
x : A
hxU : x ∈ U
γ : Path a x
hγ : ∀ (t : ↑I), γ t ∈ U
Γ' : Path e₀ ((↑p.symm ∘ ⇑f) a) :=
  { toContinuousMap := Γ (somePath a₀ a).toContinuousMap ⋯, source' := ⋯, target' := ⋯ }
⊢ x ∈ {x | (fun x ↦ (↑p.symm ∘ ⇑f) x = F x) x}
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑(rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) i j

Tactic:
simp only [LinearMap.toMatrix_apply, coe_basisOneI, LinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toLinearEquiv, rotation_apply, coe_basisOneI_repr, mul_re, mul_im,
    Matrix.val_planeConformalMatrix, Matrix.of_apply, Matrix.cons_val', Matrix.empty_val',
    Matrix.cons_val_fin_one]

Goal state after:
a : Circle
i j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re] i =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i ↦ ![(↑a).im, (↑a).re] j) i
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry = li

Tactic:
by ext1; rfl

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

Goal state before:
pp: case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ↑w ∈ t' \ {↑z}

Tactic:
apply (mem_sdiff w).1
      exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
⊢ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx, h₁f] with a h₁a h'₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h₁a : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h'₁a : f a ≠ 0
⊢ a ∈ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 0 < 0.36787944116

Tactic:
· norm_num

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

Goal state before:
pp: ⊢ log 10 = log 2 + log 5

Tactic:
norm_num [← log_mul]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h✝ : ℂ → E
D : ECanonicalDecomp f h✝ R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h : x = w
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h✝ : ℂ → E
D : ECanonicalDecomp f h✝ R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h : ¬x = w
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x

Tactic:
· simp_all [meromorphicTrailingCoeffAt_id_sub_const, divisor_def]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h✝ : ℂ → E
D : ECanonicalDecomp f h✝ R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h : ¬x = w
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
⊢ (f.comp γ') 0 = p e₀

Tactic:
by simp [γ'_0, he]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h : meromorphicOrderAt f x = 0
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ 0 • g z
h₄ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt (logDeriv g) x

Tactic:
exact (h₁g.deriv.div h₁g h₂g).meromorphicOrderAt_nonneg

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
z : ℂ
⊢ z ∈ verticalClosedStrip 0 1 →
    ‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
      max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B

Tactic:
hset

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
    max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / 2 / b,
    ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
⊢ ‖f z‖ ≤ C

Tactic:
rcases hB with ⟨c, hc, B, hO⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re ∈ {1}
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
rw [mem_singleton_iff] at hz1
    simp only [hz1, one_mul, Real.rpow_zero, sub_self, Real.rpow_neg_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 1), mul_one]
    rw [← hz1]
    apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB)
    simp only [verticalClosedStrip, mem_preimage, zero_le_one, hz1, right_mem_Icc]

Goal state after: