mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ (z / ↑(u - l)).re - l / (u - l) = (z.re - l) / (u - l)

Tactic:
rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re, Complex.ofReal_im, mul_div_assoc,
    div_mul_eq_div_div_swap, div_self (by norm_cast; linarith),
    ← div_eq_mul_one_div]

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
⊢ HarmonicAt f₁ x ↔ HarmonicAt f₂ x

Tactic:
constructor

Goal state after:
case mp
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
⊢ HarmonicAt f₁ x → HarmonicAt f₂ x

case mpr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
⊢ HarmonicAt f₂ x → HarmonicAt f₁ x
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ + f₂) x

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ ContDiffAt ℝ 2 (f₁ + f₂) x

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ - f₂) x

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ ContDiffAt ℝ 2 (f₁ - f₂) x

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ HarmonicAt (-f) x

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ ContDiffAt ℝ 2 (-f) x

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ Δ (-f) =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
c : ℝ
h : HarmonicAt f x
⊢ HarmonicAt (c • f) x

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
c : ℝ
h : HarmonicAt f x
⊢ ContDiffAt ℝ 2 (c • f) x

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
c : ℝ
h : HarmonicAt f x
⊢ Δ (c • f) =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ ContDiffAt ℝ 2 (⇑l ∘ f) x

case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ Δ (⇑l ∘ f) =ᶠ[𝓝 x] 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x ↔ HarmonicAt f x

Tactic:
constructor

Goal state after:
case mp
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x → HarmonicAt f x

case mpr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt f x → HarmonicAt (⇑l ∘ f) x
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I

Tactic:
ext

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
x✝ : ℂ
⊢ ↑((fderiv ℝ f x✝) 1) - I * ↑((fderiv ℝ f x✝) I) =
    ((⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x✝
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.cos z.im

case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.sin z.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ Set.range UpperHalfPlane.coe = ℍₒ

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ x✝ ∈ Set.range UpperHalfPlane.coe ↔ x✝ ∈ ℍₒ
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x ↦ x * log x) 0 = 0

Tactic:
exact deriv_zero_of_not_differentiableAt
      (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: f : ℂ → ℂ
z✝ : ℂ
h₁f : AnalyticAt ℂ f z✝
h₂f : f z✝ ≠ 0
z : ℂ
⊢ Real.log ‖f z‖ = (2⁻¹ • Real.log ∘ ⇑normSq ∘ f) z

Tactic:
simp only [Pi.smul_apply, Function.comp_apply, smul_eq_mul]

Goal state after:
f : ℂ → ℂ
z✝ : ℂ
h₁f : AnalyticAt ℂ f z✝
h₂f : f z✝ ≠ 0
z : ℂ
⊢ Real.log ‖f z‖ = 2⁻¹ * Real.log (normSq (f z))
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0

Tactic:
constructor

Goal state after:
case mp
x : ℝ
⊢ DifferentiableAt ℝ negMulLog x → x ≠ 0

case mpr
x : ℝ
⊢ x ≠ 0 → DifferentiableAt ℝ negMulLog x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: ⊢ sinc = dslope sin 0

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ sinc x✝ = dslope sin 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: ⊢ log = log ∘ Neg.neg

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ log x✝ = (log ∘ Neg.neg) x✝
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x ↦ ‖↑x ^ r‖) μ c 0

Tactic:
intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le

Goal state after:
case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) (Ioc c 0) μ
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) {0} μ ∧ IntegrableOn (fun x ↦ ‖↑x ^ r‖) (Ioo c 0) μ

Tactic:
constructor

Goal state after:
case neg.inr.refine_2.inr.left
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) {0} μ

case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) (Ioo c 0) μ
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_2
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume

pp: case refine_1
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume
⊢ -1 < s.re

Tactic:
· rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
    exact intervalIntegrable_cpow' h (a := 0) (b := t)

Goal state after:
case refine_1
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume
⊢ -1 < s.re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x

Tactic:
by simpa only [mul_right_comm] using! (hasDerivAt_sin x).pow (n + 1)

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots.toFinset.Nonempty

Tactic:
rw [Multiset.toFinset_nonempty]
      apply Splits.roots_ne_zero (IsAlgClosed.splits _)
      rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]

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

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

Tactic:
ext

Goal state after:
case e_f
a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin 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 : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x

Tactic:
congr; ext; ring

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
wlog hU₀ : 0 ∉ U

Goal state after:
case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ),
    0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0

Tactic:
apply Filter.codiscreteWithin_mono (U := CB) sphere_subset_closedBall

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ {x | (fun x ↦ (fun x ↦ log ‖f x‖) x = 0 x) x} ∈ codiscreteWithin CB
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
⊢ toPGL.ker = Subgroup.center (SpecialLinearGroup n R)

Tactic:
ext

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
x✝ : SpecialLinearGroup n R
⊢ x✝ ∈ toPGL.ker ↔ x✝ ∈ Subgroup.center (SpecialLinearGroup n R)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁹ : TopologicalSpace X₁
X : Type u
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormalSpace X
s : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TietzeExtension Y✝
Y : Type v
inst✝⁴ : TopologicalSpace Y
inst✝³ : Nonempty Y
inst✝² : Subsingleton Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
x✝¹ : Set X✝
x✝ : IsClosed[inst✝¹] x✝¹
f : C(↑x✝¹, Y)
y : Y
⊢ ContinuousMap.restrict x✝¹ (ContinuousMap.const X✝ y) = f

Tactic:
ext

Goal state after:
X₁ : Type u₁
inst✝⁹ : TopologicalSpace X₁
X : Type u
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormalSpace X
s : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TietzeExtension Y✝
Y : Type v
inst✝⁴ : TopologicalSpace Y
inst✝³ : Nonempty Y
inst✝² : Subsingleton Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
x✝¹ : Set X✝
x✝ : IsClosed[inst✝¹] x✝¹
f : C(↑x✝¹, Y)
y : Y
a✝ : ↑x✝¹
⊢ (ContinuousMap.restrict x✝¹ (ContinuousMap.const X✝ y)) a✝ = f a✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
h : (↑g).det < 0
⊢ (∃ z, g • z = z) ↔ (↑g).trace = 0

Tactic:
constructor

Goal state after:
case mp
g : GL (Fin 2) ℝ
h : (↑g).det < 0
⊢ (∃ z, g • z = z) → (↑g).trace = 0

case mpr
g : GL (Fin 2) ℝ
h : (↑g).det < 0
⊢ (↑g).trace = 0 → ∃ z, g • z = z
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ (-m).IsParabolic

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ -m ∉ Set.range ⇑(scalar (Fin 2))

case right
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ (-m).discr = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m ∈ Set.range ⇑(scalar (Fin 2)) ↔ m 0 1 = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m ∈ Set.range ⇑(scalar (Fin 2)) → m 0 1 = 0

case mpr
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m 0 1 = 0 → m ∈ Set.range ⇑(scalar (Fin 2))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
hz :
  ↑z = ↑((-(↑g 1 1 - ↑g 0 0) + √(↑g).discr) / (2 * ↑g 1 0)) ∨ ↑z = ↑((-(↑g 1 1 - ↑g 0 0) - √(↑g).discr) / (2 * ↑g 1 0))
⊢ False

Tactic:
simp only [z.ne_ofReal, false_or] at hz

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ fixedPt (-g) hg = fixedPt g ⋯

Tactic:
ext

Goal state after:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ ↑(fixedPt (-g) hg) = ↑(fixedPt g ⋯)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m.IsParabolic ↔ ∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m.IsParabolic → ∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0) → m.IsParabolic
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m.IsParabolic

Tactic:
constructor

Goal state after:
case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m ∉ Set.range ⇑(scalar (Fin 2))

case mpr.right
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ m.discr = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr / 4 = 0
⊢ m.discr = 0

Tactic:
div_eq_zero_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr = 0 ∨ 4 = 0
⊢ m.discr = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) ↔ g ∈ Subgroup.center (GL (Fin 2) ℝ)

Tactic:
constructor

Goal state after:
case mp
g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) → g ∈ Subgroup.center (GL (Fin 2) ℝ)

case mpr
g : GL (Fin 2) ℝ
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ) → ∀ (z : ℍ), g • z = z
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 → ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
⊢ smulAux (g * h) z = smulAux g (smulAux h z)

Tactic:
ext : 1
  simp only [smulAux, coe_mk, smulAux', map_div₀, σ_num, σ_denom, σ_mul]
  generalize hu : σ g (σ h z) = u
  have hu : u.im ≠ 0 := by simpa only [← hu, σ_im_ne_zero] using! z.im_ne_zero
  have hu' : (num h u / denom h u).im ≠ 0 := by
    rw [moebius_im]
    exact div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)
  rw [div_eq_div_iff (denom_ne_zero_of_im _ hu) (denom_ne_zero_of_im _ hu'),
    denom, mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), mul_div]
  conv_rhs => rw [num]
  rw [mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), div_mul_eq_mul_div]
  congr 1
  simp only [num, denom, Units.val_mul, mul_apply, Fin.sum_univ_succ,
    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
    Complex.ofReal_add, Complex.ofReal_mul]
  ring

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

Goal state before:
pp: z : ℍ
⊢ smulAux 1 z = z

Tactic:
simp [smulAux, smulAux', num, denom, σ]

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

Goal state before:
pp: A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
⊢ verticalStrip A B ⊆ verticalStrip A' B'

Tactic:
rintro z ⟨hzre, hzim⟩
  exact ⟨hzre.trans hA, hB.trans hzim⟩

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ g • z = { coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }

Tactic:
ext

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ ↑(g • z) = ↑{ coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }