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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ z.wedgeIntegral w f + w.wedgeIntegral z f =
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)

Tactic:
simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re,
    intervalIntegral.integral_symm z.im w.im, smul_neg]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ ((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) +
      ((-∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + -(I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I))) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
⊢ ∀ x ∈ s, HasDerivAt (fun z ↦ η z - η x₀ + y) (f x) x

Tactic:
by simpa using hη

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
set I₈ := I • ∫ y in c.im..z.im, f (w.re + y * I)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z ↦ f (↑l + z • (↑u - ↑l))) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.comp (s := verticalStrip l u) hd

Goal state after:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z ↦ ↑l + z • (↑u - ↑l)) (verticalStrip 0 1)

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ MapsTo (fun z ↦ ↑l + z • (↑u - ↑l)) (verticalStrip 0 1) (verticalStrip l u)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ ↑l + z • (↑u - ↑l) ∈ verticalStrip l u

Tactic:
exact scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz

Goal state after:
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
h₁ : ContDiffAt ℝ 2 f₁ x✝
h₂ : ContDiffAt ℝ 2 f₂ x✝
x : E
h₁x : ContDiffAt ℝ 2 f₁ x
h₂x : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) x = (Δ f₁ + Δ f₂) x

Tactic:
exact h₁x.laplacian_add h₂x

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ (fun w ↦ f w - f z) =o[𝓝 z] fun x ↦ 1

Tactic:
Asymptotics.isLittleO_one_iff,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ Filter.Tendsto (fun w ↦ f w - f z) (𝓝 z) (𝓝 0)
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 : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
⊢ circleAverage f c R = f c

Tactic:
by_cases hR : R = 0
  · simp [hR]
  · rw [← circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable hs h₁f h₂f (by aesop)]
    apply circleAverage_congr_sphere fun z hz ↦ ?_
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    simp_all

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ CircleIntegrable F c R

Tactic:
apply (h₁F.continuousOn.mono (fun _ _ ↦ by simp_all [dist_eq_norm])).circleIntegrable'

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

Goal state before:
pp: case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x ↦ log x * x) (𝓝[Set.Iio 0 ∪ Set.Ioi 0] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)

Tactic:
nhdsWithin_union

Goal state after:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x ↦ log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)
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
⊢ 1 * R = ‖W‖

Tactic:
by simp [W, abs_of_pos hR]

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

Goal state before:
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
m : IntervalIntegrable (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x ↦ ↑(-x) ^ r) volume 0 (-c)

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢

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
m : IntegrableOn (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Ioc 0 (-c)) volume
⊢ IntegrableOn (fun x ↦ ↑(-x) ^ r) (Ioc 0 (-c)) volume
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 {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : dist z ↑x₀ < ‖↑x₀‖
⊢ z ∈ {z | 0 < z.re}

Tactic:
dist_eq,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : ‖z - ↑x₀‖ < ‖↑x₀‖
⊢ z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) = 2 * ↑r * ↑(sinc r)

Tactic:
rw [integral_exp_mul_I_eq_sin]

Goal state after:
r : ℝ
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sinc r)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) = 0

Tactic:
by
    simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi,
      (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero]
    ring

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

Goal state before:
pp: case inr.inl
a : ℂ
h : 1 = ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

pp: case inr.inr
a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
· rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]
    simp_all

Goal state after:
case inr.inr
a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π * z.im / h < -2 * π * A / h ↔ A < z.im

Tactic:
div_lt_div_iff_of_pos_right hh,

Goal state after:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π * z.im < -2 * π * A ↔ A < z.im
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)

Goal state after:
n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h ↦ pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ dist z c < (z - c).re + 1

Tactic:
dist_eq,

Goal state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ ‖z - c‖ < (z - c).re + 1
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)

Tactic:
rw [abs_div, abs_of_pos H]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt (-1) = I

Tactic:
by
  simp [sqrt_neg_of_nonneg (a := (1 : 𝕜)) (by simp)]

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

Goal state before:
pp: case inl
hK : IsCompact ∅
⊢ ∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B

Tactic:
exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ (↑g 1 0 * z.im) ^ 2 ≤ Complex.normSq (denom g ↑z)

Tactic:
set c := g 1 0

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g ↑z)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0

Tactic:
rw [ha, map_zero, zero_add] at hg

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0»
z : ℂ
i : Fin 2
⊢ ![z.re * re 1 - z.im * im 1, z.re * im 1 + z.im * re 1] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

pp: case «1»
z : ℂ
i : Fin 2
⊢ ![z.re * I.re - z.im * I.im, z.re * I.im + z.im * I.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1

Tactic:
· simp only [one_re, mul_one, one_im, mul_zero,
      sub_zero, zero_add]
    fin_cases i <;> rfl

Goal state after:
case «1»
z : ℂ
i : Fin 2
⊢ ![z.re * I.re - z.im * I.im, z.re * I.im + z.im * I.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ ⇑g ⁻¹' {a}

Tactic:
rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
x : X
ha : IsGLB (range ⇑f) (g (e x))
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (g (e x)) b
hle : g (e x) ≤ b
hlt : g (e x) < b
c : ℝ := (g (e x) + b) / 2
hac : g (e x) < c
hcb : c < b
hsub : c - g (e x) = b - c
hg_mem : ∀ (y : Y), g y ∈ Icc (g (e x)) b
ha' : ¬∃ x_1, f x_1 = g (e x)
⊢ False
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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ a < (g - dg) y

Tactic:
calc
          a = c - (b - c) := by rw [← hsub, sub_sub_cancel]
          _ < g y - (b - c) := sub_lt_sub_right hc _
          _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _

Goal state after:
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 x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]

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 x : P
hne : x ≠ c
⊢ dist x c ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ sinh (dist z w / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))

Tactic:
dist_eq,

Goal state after:
z w : ℍ
⊢ sinh (2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im))) / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

Tactic:
dist_eq,

Goal state after:
z w : ℍ
⊢ cosh (2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r : ℝ
z : ℍ
⊢ dist z z = 0

Tactic:
dist_eq,

Goal state after:
z✝ w : ℍ
r : ℝ
z : ℍ
⊢ 2 * arsinh (dist ↑z ↑z / (2 * √(z.im * z.im))) = 0
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑Y.toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f)) x = (ConcreteCategory.hom (𝟙 Y)) x

Tactic:
apply E.apply_symm_apply

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

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
by
  let : TopologicalSpace α := ⊥
  have : DiscreteTopology α := ⟨rfl⟩
  exact funext (isDenseInducing_pure.extend_eq continuous_of_discreteTopology)

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

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)

Tactic:
by
  have h (b : Ultrafilter α) : ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
    -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ.
    let ⟨c, _, h'⟩ :=
      isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
    ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩
  let _ : TopologicalSpace α := ⊥
  exact isDenseInducing_pure.continuous_extend h

Goal state after:
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:
dist_eq,

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

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s

Tactic:
simp only [Function.comp_apply, mem_preimage, eventually_atTop]

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → g { down := ↑b } ∈ s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
⊢ 0 ≤ proximity f a

Tactic:
by
  by_cases h : a = ⊤ <;>
  · intro r
    simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)

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

Goal state before:
pp: case e'_3
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
⊢ {m |
      ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
        (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')} =
    {y |
      (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
        (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `ext` was not necessary.
    The cause of this might be `Matrix` function application defeq abuse. -/

Goal state after:
case e'_3
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
⊢ {m |
      ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
        (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')} =
    {y |
      (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
        (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ IsProperMap fun g ↦ g • I

Tactic:
refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun K hK ↦ ?_⟩
  obtain ⟨A, hA⟩ := absq_le hK
  obtain ⟨A', hA'⟩ := cdsq_le hK
  -- activate the sup-norm on matrices
  let : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
  have : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ) := pi_properSpace
  have : IsCompact {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ i j, |m i j| ≤ max √A √A'} := by
    convert! ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')
    simp only [le_sup_iff, Fin.forall_fin_two, Fin.isValue, Metric.closedBall, dist_zero_right,
      Matrix.norm_def, pi_norm_le_iff_of_nonempty, Real.norm_eq_abs]
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `ext` was not necessary.
    The cause of this might be `Matrix` function application defeq abuse. -/
    ext; grind
  have := Matrix.SpecialLinearGroup.isClosedEmbedding_val.isCompact_preimage this
  refine this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop) (fun g hg ↦ ?_)
  intro i j
  fin_cases i
  · refine le_trans ?_ <| le_max_left √A √A'
    exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA g hg)
  · refine le_trans ?_ <| le_max_right √A √A'
    exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA' g hg)

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
⊢ circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [circleAverage_congr_sphere (f₂ := fun _ ↦ log ‖meromorphicTrailingCoeffAt f 0‖),
    circleAverage_const]
  intro a ha
  simp only
  congr 2
  rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
  rw [meromorphicOrderAt_const]
  aesop

Goal state after: