mathlib-initiative/mathlib-tactics huggingface dataset:
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)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g

Tactic:
trans (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ
      · unfold φ
        rw [finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀]
        · filter_upwards [codiscreteWithin_mono (by tauto) η₀.compl_mem_codiscrete,
            self_mem_codiscreteWithin (closedBall 0 R)] with a ha h₂a
          simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply]
          rw [← smul_assoc, ← Finset.prod_smul, Finset.prod_eq_one, one_smul]
          intro x hx
          rw [smul_eq_mul, ← zpow_add', neg_add_cancel, zpow_zero]
          simp_all only [ne_eq, Subtype.forall, mem_closedBall, dist_zero_right,
            locallyFinsuppWithin.support_neg, mem_compl_iff, mem_support, Decidable.not_not,
            Finite.mem_toFinset, neg_add_cancel, not_true_eq_false, neg_eq_zero, and_self, or_self,
            or_false]
          apply canonicalFactor_ne_zero _ (by simp_all) (by grind)
          by_contra h
          simp_all
      · rw [finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀]
        filter_upwards [toMeromorphicNFOn_eqOn_codiscrete hφ] using by simp_all [g]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ ℓ ((↑a.re + ↑a.im • I) • (↑b.re + ↑b.im • I)) = (↑a.re + ↑a.im • I) • ℓ (↑b.re + ↑b.im • I)

Tactic:
simp only [add_smul, smul_add, ℓ.map_add, t₀, t₁]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ ℓ (↑a.re • ↑b.re) + ℓ (↑(a.im * b.re) • I) + (ℓ (↑a.re • ↑b.im • I) + ℓ (↑(-a.im * b.im) • 1)) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • ℓ (↑b.im • I) + (↑a.im • I) • ℓ (↑b.im • I))
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u, meromorphicOrderAt f ↑u ≠ ⊤) → ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
intro h₂f

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, meromorphicOrderAt f ↑u ≠ ⊤
⊢ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) → ∃ u, meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
intro h₂f

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
⊢ ∃ u, meromorphicOrderAt f ↑u ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
⊢ ENat.map Nat.cast 0 = 0

Tactic:
ENat.map_zero,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
⊢ ↑↑0 = 0
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ y ∈ ball z r₁

Tactic:
rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]

Goal state after:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ |y.re - z.re| < r₁
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
⊢ y ∈ insert x s → (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y

Tactic:
h₃y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
⊢ y ∈ insert x s → (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
h₃y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: case hf
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
⊢ Differentiable ℂ fun z ↦ cexp (F z)

pp: case hb
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
⊢ IsBounded (range fun z ↦ cexp (F z))

Tactic:
· apply (differentiable_exp.comp (fun x ↦ (hF_diff x (mem_univ x)).differentiableAt))

Goal state after:
case hb
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
⊢ IsBounded (range fun z ↦ cexp (F z))
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c R = f w

Tactic:
by_cases hR : |R| ≤ 0

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : |R| ≤ 0
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c R = f w

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c R = f w
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

Tactic:
by_cases hR : R ≤ 0
  · simp [ball_eq_empty.2 hR]
  let g := ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)
  have hg : DifferentiableOn ℂ g (ball z R) :=
    fun x hx ↦ (HarmonicAt.differentiableAt_complex_partial (hf x hx)).differentiableWithinAt
  obtain ⟨F, hF⟩ := hg.isExactOn_ball.with_val_at z (f z)
  have h₁F : DifferentiableOn ℂ F (ball z R) :=
    fun x hx ↦ (hF.2 x hx).differentiableAt.differentiableWithinAt
  have h₂F : DifferentiableOn ℝ F (ball z R) := h₁F.restrictScalars (𝕜 := ℝ) (𝕜' := ℂ)
  use F, h₁F.analyticOnNhd isOpen_ball
  rw [(by aesop : (fun z ↦ (F z).re) = Complex.reCLM ∘ F)]
  intro x hx
  apply (convex_ball z R).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := z)
  · exact reCLM.differentiable.comp_differentiableOn h₂F
  · exact fun y hy ↦ (ContDiffAt.differentiableAt (hf y hy).1 two_ne_zero).differentiableWithinAt
  · exact isOpen_ball.uniqueDiffOn
  · intro y hy
    have h₄F := (hF.2 y hy).differentiableAt
    have h₅F := h₄F.restrictScalars (𝕜 := ℝ) (𝕜' := ℂ)
    rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hy)
      (reCLM.differentiableAt.comp y h₅F), fderivWithin_eq_fderiv
      (isOpen_ball.uniqueDiffWithinAt hy) ((hf y hy).1.differentiableAt two_ne_zero), fderiv_comp y
      (by fun_prop) h₅F, ContinuousLinearMap.fderiv, h₄F.fderiv_restrictScalars (𝕜 := ℝ)]
    ext a
    nth_rw 2 [(by simp : a = a.re • (1 : ℂ) + a.im • (I : ℂ))]
    rw [map_add, map_smul, map_smul]
    simp [HasDerivAt.deriv (hF.2 y hy), g]
  all_goals simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)

Tactic:
apply intervalIntegral.integral_sub hf₁ hf₂

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

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ‖-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))‖ ≤ R * r

Tactic:
by simp [abs_of_pos, h₁, h₁.trans h₂]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
x : ℂ
h : ‖x‖ ≤ R
⊢ ‖↑q * x‖ = q * ‖x‖

Tactic:
simp [abs_of_pos h₁q]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ False
h2 : ¬0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b

Tactic:
or_false

Goal state after:
case neg
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : 0 < log x
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
right
    have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
    simp only [this, and_true, ge_iff_le]
    linarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
i : ℝ
⊢ IntervalIntegrable (fun x ↦ log ‖x‖) volume (a - i) (b - i)

Tactic:
simp [norm_eq_abs, log_abs]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ * cos x✝ = 1 - sin x✝ * sin x✝

Tactic:
← sq,

Goal state after:
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ ^ 2 = 1 - sin x✝ * sin x✝
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ ^ 2 = 1 - sin x✝ * sin x✝

Tactic:
← sq,

Goal state after:
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ ^ 2 = 1 - sin x✝ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝

Tactic:
← sq,

Goal state after:
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ ^ 2 = 1 - cos x✝ * cos x✝
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ ^ 2 = 1 - cos x✝ * cos x✝

Tactic:
← sq,

Goal state after:
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ ^ 2 = 1 - cos x✝ ^ 2
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n (fun z ↦ f (-z)) (-c)

Tactic:
· simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
← re_add_im a

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ + ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).im then 1 else -1) *
            ↑√((‖(map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)‖ - ((map 𝕜 ℂ) (↑(re a) + ↑(im a) * I)).re) / 2) *
          Complex.I) =
    ↑√((‖↑(re a) + ↑(im a) * I‖ + re (↑(re a) + ↑(im a) * I)) / 2) +
      (if 0 ≤ im (↑(re a) + ↑(im a) * I) then 1 else -1) *
          ↑√((‖↑(re a) + ↑(im a) * I‖ - re (↑(re a) + ↑(im a) * I)) / 2) *
        I
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
⊢ ↑(GeneralLinearGroup.det h) * u.im / Complex.normSq (denom h u) ≠ 0

Tactic:
exact div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ ¬(↑g).trace = 0

Tactic:
← sq_eq_zero_iff,

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ ¬(↑g).trace ^ 2 = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
simp only [atImInfty_basis.mem_iff, true_and]; rfl

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑g 1 0 = 0
⊢ Tendsto (fun τ ↦ g • τ) atImInfty atImInfty

Tactic:
suffices Tendsto (fun τ ↦ |g 0 0 / g 1 1| * τ.im) atImInfty atTop by
    simpa [atImInfty, Function.comp_def, im_smul, num, denom, hg, abs_div, abs_mul,
      abs_of_pos (UpperHalfPlane.im_pos _), mul_div_right_comm]
  apply tendsto_comap.const_mul_atTop
  simpa [Matrix.det_fin_two, hg] using g.det_ne_zero

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f M.det).det * (f (M k k ^ (Fintype.card m - 1))).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
← det_mul,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f M.det * f (M k k ^ (Fintype.card m - 1))).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R * R / R ^ 2) ^ 2 • (x -ᵥ c) +ᵥ c = x

Tactic:
← sq,

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R ^ 2 / R ^ 2) ^ 2 • (x -ᵥ c) +ᵥ c = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
dist_eq_iff_dist_coe_center_eq,

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center (dist (log z.im) (log w.im))) = w.im * Real.sinh (dist (log z.im) (log w.im))
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]

Tactic:
refine continuous_matrix fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case right
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]

Tactic:
refine continuous_matrix fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
x : GL n A
x✝ : ∃ y, ↑y = ↑x
y : SL n A
hy : ↑y = ↑x
⊢ (↑x).det = 1

Tactic:
by simp [← hy]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
ext w; constructor
  · rintro ⟨w, hw, rfl⟩
    exact dist_le_iff_dist_coe_center_le.1 hw
  · intro hw
    lift w to ℍ using im_pos_of_dist_center_le hw
    exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A

Tactic:
intro s hs

Goal state after:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ ↑b

Tactic:
intro s hs

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ dist { coe := (-↑y₁)⁻¹, coe_im_pos := ⋯ } { coe := (-↑y₂)⁻¹, coe_im_pos := ⋯ } = dist y₁ y₂

Tactic:
inv_neg,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ dist { coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ } { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ } = dist y₁ y₂
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
⊢ ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)) → IsClosed[inst✝³] s

Tactic:
intro s hs

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ IsClosed[inst✝³] s
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ a * |logCounting (single e 1) ℓ| ≤ a * |logCounting D ℓ|

Tactic:
gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
⊢ 0 ≤ logCounting f r

Tactic:
have h₃r : 0 < r := by linarith

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
⊢ 0 ≤ logCounting f r