mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: 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
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ) =
    (2 * π)⁻¹ • ((∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) + ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
congr

Goal state after:
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 θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: 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
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    (2 * π)⁻¹ • ((∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
congr

Goal state after:
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 θ)
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
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
by
  obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c R).exists_thickening_subset_open
    (isOpen_setOfPred_harmonicAt f) (by aesop)
  rw [thickening_closedBall h₁e (pos_of_mem_ball hw).le] at h₂e
  obtain ⟨F, h₁F, h₂F⟩ := HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e
  have h₃F : DifferentiableOn ℂ F (closure (ball c R)) := by
    intro x hx
    apply (h₁F x _).differentiableWithinAt
    grind [mem_ball, mem_closedBall.1 (closure_ball_subset_closedBall hx)]
  have 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) := by
    intro x hx
    simp [h₂F (sphere_subset_ball (lt_add_of_pos_left R h₁e) hx), herglotzRieszKernel_def]
  rw [← abs_of_pos (pos_of_mem_ball hw)] at h₄F
  rw [circleAverage_congr_sphere h₄F, reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage_re_herglotzRieszKernel_smul' hw]
  · apply h₂F
    grind [mem_ball]
  -- CircleIntegrable (fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
  apply (ContinuousOn.fun_smul _ _).circleIntegrable'
  · apply (continuousOn_herglotz_riesz hw).mono
    grind [mem_ball, dist_eq_norm, mem_sphere_iff_norm, (pos_of_mem_ball hw)]
  · apply (h₁F.mono _).continuousOn (𝕜 := ℂ)
    grind [mem_sphere, mem_ball, (pos_of_mem_ball hw)]

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

Goal state before:
pp: c w z : ℂ
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z

Tactic:
Function.comp_apply,

Goal state after:
c w z : ℂ
⊢ poissonKernel c w z = (herglotzRieszKernel c w z).re
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y | y ≠ 0})
⊢ reCLM (log ((starRingEnd ℂ) (g x) * g x)) = reCLM (log ((starRingEnd ℂ) (g x)) + log (g x))

Tactic:
congr

Goal state after:
case e_6
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y | y ≠ 0})
⊢ log ((starRingEnd ℂ) (g x) * g x) = log ((starRingEnd ℂ) (g x)) + log (g x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ sin x * x⁻¹ * -x ≤ 1

Tactic:
ring_nf
      rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]
      exact neg_one_le_sin x

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

Goal state before:
pp: case inl
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c

pp: case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c

Tactic:
· exact this c hc

Goal state after:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inl
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c

pp: case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c

Tactic:
· exact this c hc

Goal state after:
case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
rw [← neg_neg log]
    apply IntervalIntegrable.neg
    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
    · intro s ⟨hs, _⟩
      norm_num at *
      simpa using! (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)
    · intro s ⟨hs₁, hs₂⟩
      grind [Pi.neg_apply, log_nonpos_iff]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ici 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Set.Ici 0 → x ≤ b → log⁺ x ≤ log⁺ b

Tactic:
y

Goal state after:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
⊢ y ∈ Set.Ici 0 → x ≤ y → log⁺ x ≤ log⁺ y
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 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
⊢ ‖(2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)‖ ≤ 2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖

Tactic:
have h₁ : ‖(2 : ℂ)‖ = 2 := by norm_num

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 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : ‖2‖ = 2
⊢ ‖(2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)‖ ≤ 2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x

Tactic:
congr

Goal state after:
case f
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| fun y ↦ Complex.exp (c * ↑y) / c

case f'
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| Complex.exp (c * ↑x)

case x
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

Tactic:
by
  have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x := by
    intro x
    conv => congr
    rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
    apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
    simpa only [mul_one] using! ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
  rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
  · ring
  · fun_prop

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

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ log (Complex.normSq (circleMap 0 1 x - 1)) / 2 = log (4 * sin (x / 2) ^ 2) / 2

Tactic:
congr

Goal state after:
case e_a
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ Complex.normSq (circleMap 0 1 x - 1) = 4 * sin (x / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖↑R * z + c - a‖) 0 1 = circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1

Tactic:
congr

Goal state after:
case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (fun z ↦ log ‖↑R * z + c - a‖) = fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ log ‖↑R * z + c - a‖ = log ‖↑R * (z + ↑R⁻¹ * (c - a))‖

Tactic:
congr

Goal state after:
case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ ↑R * z + c - a = ↑R * (z + ↑R⁻¹ * (c - a))
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
let ray : E → ℂ → E := fun z t => z₀ + t • z
  let gray : E → ℂ → ℂ := fun z => g ∘ ray z
  obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg
  have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOnNhd ℂ (gray z) (ball 0 r) := by
    refine fun z hz t ht => AnalyticAt.comp ?_ ?_
    · exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using! ht)
    · exact analyticAt_const.add
        ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)
  by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
  · 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
  · right
    simp only [not_forall] at h
    -- Otherwise, it is open along at least one direction and that implies the result
    obtain ⟨z, hz, hrz⟩ := h
    specialize h1 z hz 0 (mem_ball_self hr)
    have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
    rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7
    refine h7.trans (map_mono ?_)
    have h10 : Continuous fun t : ℂ => z₀ + t • z := by fun_prop
    simpa using! h10.tendsto 0

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

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = ↑c₀ + ↑c * I

Tactic:
obtain ⟨cc, hcc⟩ := eq_const_of_re_eq_const h₁f h₂f h₁U h₂U
  use cc.im
  simp_rw [Complex.ext_iff]
  aesop

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : c ≤ z
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z

Tactic:
rw [← sub_nonneg] at hz₁

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z
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

Goal state after:
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
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
have hr_lt (n : ℕ) : r n < R := by
    simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]
    positivity

Goal state after:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ ↑(D u) • circleAverage (fun z ↦ log ‖z - u‖) c R = ↑(D u) • log R

Tactic:
congr

Goal state after:
case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ circleAverage (fun z ↦ log ‖z - u‖) c R = log R
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
⊢ ∀ ⦃b : α⦄, b ∈ s ∪ t → x < b → f x < f b

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
⊢ y ∈ s ∪ t → x < y → f x < f y
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
⊢ ∀ ⦃b : α⦄, b ∈ s ∪ t → x ≤ b → f x ≤ f b

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
⊢ y ∈ s ∪ t → x ≤ y → f x ≤ f y
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ ↑√((‖I‖ + I.re) / 2) + ↑√((‖I‖ - I.re) / 2) * I = ↑√2⁻¹ * (1 + I)

Tactic:
simp [mul_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
⊢ A.discr = A.trace ^ 2 - 4 * A.det

Tactic:
by
  nontriviality R
  rw [discr, Polynomial.discr_of_degree_eq_two (by simp; norm_cast)]
  simp [A.charpoly_of_card_eq_two hn]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simpa using isHyperbolic_conj_iff g⁻¹

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

Goal state before:
pp: ⊢ FaithfulSMul PGL(2, ℝ) ℍ

Tactic:
rw [faithfulSMul_iff]
  intro g
  cases g
  simp [forall_smul_eq_self_iff_mem_center]

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
⊢ auxMat M k i j = 0

Tactic:
auxMat,

Goal state after:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
⊢ of (fun i j ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) i j = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ ∑ j_1, M i j_1 * auxMat M k j_1 j = 0

Tactic:
auxMat,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ ∑ j_1,
      M i j_1 *
        of (fun i j ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0)
          j_1 j =
    0
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
⊢ (f ((evalRingHom 0).mapMatrix (cornerAddX M k)).det).det = (f M.det).det

Tactic:
congr

Goal state after:
case e_6
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 (cornerAddX M k) = M
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case refine_1
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt f τ
⊢ MDiffAt (f ∘ ↑ofComplex) ↑τ

Tactic:
exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)

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

Goal state before:
pp: case e'_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ f w = (f ∘ ↑ofComplex) ↑w

Tactic:
Function.comp_apply,

Goal state after:
case e'_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ f w = f (↑ofComplex ↑w)
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
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc x y
⊢ ↑(h z) ∈ t'

Tactic:
exact ⟨z, hs.out hx hy hz, rfl⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ inversion c (dist x c) x = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
⊢ inversion x (dist x x) x = x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: 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
⊢ inversion c R (inversion c R x) = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x

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
⊢ inversion c R (inversion c R x) = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Tactic:
rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs,
    Real.norm_eq_abs, mul_left_comm]

Goal state after:
case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ (Ultrafilter.extend g ∘ pure) a = (Ultrafilter.extend g ∘ pure) b

Tactic:
Function.comp_apply,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = (Ultrafilter.extend g ∘ pure) b
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ (T2Quotient.lift ⋯ ∘ stoneCechUnit) x = g x

Tactic:
Function.comp_apply,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ T2Quotient.lift ⋯ (stoneCechUnit x) = g x
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
z : OnePoint X
⊢ IsClosed[instTopologicalSpace] {z}

Tactic:
induction z using OnePoint.rec

Goal state after:
case infty
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
⊢ IsClosed[instTopologicalSpace] {∞}

case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[instTopologicalSpace] {↑x✝}