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

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ ContinuousOn (fun i ↦ ((i - c + (w - c)) / (i - c - (w - c))).re) (sphere c |R|)

Tactic:
apply (continuousOn_herglotz_riesz hw).mono
    grind [mem_ball, dist_eq_norm, mem_sphere_iff_norm, (pos_of_mem_ball hw)]

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

Goal state before:
pp: 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
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x ↦ ‖Complex.exp (↑π * Complex.I * r)‖) (Ioo c 0) μ

Tactic:
rw [integrableOn_const_iff]

Goal state after:
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
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ‖‖Complex.exp (↑π * Complex.I * r)‖‖ₑ = 0 ∨ μ (Ioo c 0) < ⊤
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1

Tactic:
apply IntervalIntegrable.neg

Goal state after:
case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (-log) volume 0 1
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
x : ℂ
⊢ AEStronglyMeasurable (fun θ ↦ herglotzRieszKernel 0 x (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))

Tactic:
simp only [herglotzRieszKernel_def, sub_zero]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
x : ℂ
⊢ AEStronglyMeasurable (fun θ ↦ (circleMap 0 R θ + x) / (circleMap 0 R θ - x)) (volume.restrict (uIoc 0 (2 * π)))
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
⊢ max 0 (log x) - max 0 (log x⁻¹) = log x

Tactic:
log_inv

Goal state after:
x : ℝ
⊢ max 0 (log x) - max 0 (-log x) = log x
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
hx : x = 0
y : ℝ
hy : y ∈ Metric.ball x 1
⊢ |y| ≤ 1

Tactic:
simp_all [le_of_lt]

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

Goal state before:
pp: a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Tactic:
rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
      (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]

Goal state after:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 / (r + 1)) + (↑b ^ (r + 1) / (r + 1) - 0 / (r + 1)) =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) =
    ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1)))

Tactic:
convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)

Goal state after:
case e'_2
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t

case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑?convert_2 ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑?convert_1 ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))

case convert_1
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_2
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case convert_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -1

Tactic:
rw [← ofReal_one, ← ofReal_neg, Ne, ofReal_inj]
    exact ht

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

Goal state before:
pp: case h₁
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)

Tactic:
simp only [herglotzRieszKernel_def, sub_zero]

Goal state after:
case h₁
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
induction n with

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
· left
    -- If g is eventually constant along every direction, then it is eventually constant
    refine eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_
    refine (eq_or_ne z z₀).casesOn (congr_arg g) fun h' => ?_
    replace h' : ‖z - z₀‖ ≠ 0 := by simpa only [Ne, norm_eq_zero, sub_eq_zero]
    let w : E := ‖z - z₀‖⁻¹ • (z - z₀)
    have h3 : ∀ t ∈ ball (0 : ℂ) r, gray w t = g z₀ := by
      have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
      have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
      specialize h1 w e2
      apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
      simpa [ray, gray] using! h w e2
    have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using! mem_ball.mp hz
    replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by simpa
    simpa only [ray, gray, w, smul_smul, mul_inv_cancel₀ h', one_smul, add_sub_cancel,
      Function.comp_apply, coe_smul] using! h3 (↑‖z - z₀‖) h4

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) = π * ∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
induction n with

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ ∃ f, MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
use fun z ↦ ε / (f z - x)

Goal state after:
case h
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ MapsTo (fun z ↦ ↑ε / (f z - x)) U (ball 0 1) ∧
    InjOn (fun z ↦ ↑ε / (f z - x)) U ∧ ∀ z ∈ U, deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case pos
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this : ∀ {g : ℂ → ℝ}, (Function.support fun u ↦ ↑(D u) * g u) ⊆ ↑(Finite.toFinset hD)
x : ℂ
hx : x ∈ Finite.toFinset hD ∧ x ≠ c
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * (log R + log ‖c - x‖⁻¹)

Tactic:
log_inv

Goal state after:
case pos
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this : ∀ {g : ℂ → ℝ}, (Function.support fun u ↦ ↑(D u) * g u) ⊆ ↑(Finite.toFinset hD)
x : ℂ
hx : x ∈ Finite.toFinset hD ∧ x ≠ c
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * (log R + -log ‖c - x‖)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * (log R + log ‖c - x‖⁻¹)

Tactic:
log_inv

Goal state after:
case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * (log R + -log ‖c - x‖)
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 : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R + log ‖g c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R +
      (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log ‖c - u‖)

Tactic:
by
      have t₀ : c ∈ CB := by simp [CB]
      have t₁ : AccPt c (𝓟 CB) := by
        apply accPt_iff_frequently_nhdsNE.mpr
        apply compl_notMem
        apply mem_nhdsWithin.mpr
        use ball c |R|
        simpa [hR] using! fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h
      simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles h₃f t₀ t₁
        (h₁f c t₀) (h₁g c t₀) (h₂g ⟨c, t₀⟩) h₃g]

Goal state after:
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 : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R - ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log ‖c - u‖ +
      log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
by
      rw [← finsum_sub_distrib]
      · simp_rw [← mul_sub]
      repeat apply h₃f.subset (fun _ ↦ (by simp_all))

Goal state after:
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * f x ≤ b

Tactic:
nlinarith [(hf01 x).2]

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

Goal state before:
pp: case refine_1
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
x : E
hx : x ∈ frontier (Metric.closedBall 0 1)
⊢ id x = g x

pp: case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
· replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
    simp [g, hx]

Goal state after:
case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: ⊢ TietzeExtension ↑I

Tactic:
rw [unitInterval.eq_closedBall]

Goal state after:
⊢ TietzeExtension ↑(Metric.closedBall 2⁻¹ 2⁻¹)
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
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ Subgroup.center (GL n R) ≤ f.ker

Tactic:
GeneralLinearGroup.center_eq_range_scalar,

Goal state after:
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ (GeneralLinearGroup.scalar n).range ≤ f.ker
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
induction n with

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

Goal state before:
pp: case mp.f
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = 1
⊢ ∃ x, x ≠ 0 ∧ ↑g = ↑(upperRightHom x)

Tactic:
refine ⟨g 0 1, hg01, ?_⟩
      rw [g.val.eta_fin_two]
      simp_all

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
x : X
⊢ (⇑(const Y ((a + b) / 2) + g) ∘ e) x = f x

Tactic:
have : g (e x) = f x - (a + b) / 2 := congr_fun hge x

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
x : X
this : g (e x) = f x - (a + b) / 2
⊢ (⇑(const Y ((a + b) / 2) + g) ∘ e) x = f x
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
⊢ (evalRingHom 0) (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det

Tactic:
RingHom.map_det,

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
⊢ ((evalRingHom 0).mapMatrix (f.polyToMatrix (cornerAddX M k).det)).det = (f M.det).det
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
⊢ (evalRingHom 0) ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix)).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det

Tactic:
RingHom.map_det,

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
⊢ ((evalRingHom 0).mapMatrix ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix))).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det
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
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((Matrix.comp { a // (a ≠ k) = True } { a // (a ≠ k) = True } n n R)
            (((auxMat M k).toSquareBlock (fun x ↦ x ≠ k) True).map ⇑f)).det *
        ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R)
            (((auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False).map ⇑f)).det)

Tactic:
auxMat_toSquareBlock_eq,

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
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((Matrix.comp { a // (a ≠ k) = True } { a // (a ≠ k) = True } n n R)
            (((auxMat M k).toSquareBlock (fun x ↦ x ≠ k) True).map ⇑f)).det *
        ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R) (Matrix.map 1 ⇑f)).det)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0

Tactic:
rw [mdifferentiable_iff] at hf

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
have hgG : ∀ {y a}, g y = a ↔ G y = h a := @fun y a =>
    h.toEquiv.symm_apply_eq.trans Subtype.ext_iff

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ sinh x - x) (Ici 0)

Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_

Goal state after:
case refine_1
⊢ ContinuousOn (fun x ↦ sinh x - x) (Ici 0)

case refine_2
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x ↦ sinh x - x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sinh = sinh

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cosh = cosh

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
A : Ultrafilter α
⊢ connectedComponent A = {A}

Tactic:
simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and]

Goal state after:
α : Type u
A : Ultrafilter α
⊢ ∀ x ∈ connectedComponent A, x = A
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange fun x ↦ ⟦preStoneCechUnit x⟧

Tactic:
have : Function.Surjective (T2Quotient.mk : PreStoneCech α → StoneCech α) := by
    exact Quot.mk_surjective

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
this : Function.Surjective T2Quotient.mk
⊢ DenseRange fun x ↦ ⟦preStoneCechUnit x⟧