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
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w w_in_z_ball ↦ ?_⟩
  set I₁ :=     ∫ x in c.re..w.re, f (x + c.im * I)
  set I₂ := I • ∫ y in c.im..w.im, f (w.re + y * I)
  set I₃ :=     ∫ x in c.re..z.re, f (x + c.im * I)
  set I₄ := I • ∫ y in c.im..z.im, f (z.re + y * I)
  set I₅ :=     ∫ x in z.re..w.re, f (x + z.im * I)
  set I₆ := I • ∫ y in z.im..w.im, f (w.re + y * I)
  set I₇ :=     ∫ x in z.re..w.re, f (x + c.im * I)
  set I₈ := I • ∫ y in c.im..z.im, f (w.re + y * I)
  have z_ball : ball z (r - dist z c) ⊆ ball c r := ball_subset_ball' (by simp)
  have w_mem : w ∈ ball c r := mem_of_subset_of_mem z_ball w_in_z_ball
  have integrableHoriz (a₁ a₂ b : ℝ) (ha₁ : a₁ + b * I ∈ ball c r) (ha₂ : a₂ + b * I ∈ ball c r) :
      IntervalIntegrable (fun x ↦ f (x + b * I)) volume a₁ a₂ :=
    ((f_cont.mono (mem_ball_of_map_re_aux ha₁ ha₂)).comp (by fun_prop)
      (mapsTo_image _ _)).intervalIntegrable
  have integrableVert (a b₁ b₂ : ℝ) (hb₁ : a + b₁ * I ∈ ball c r) (hb₂ : a + b₂ * I ∈ ball c r) :
      IntervalIntegrable (fun y ↦ f (a + y * I)) volume b₁ b₂ :=
    ((f_cont.mono (mem_ball_of_map_im_aux₁ hb₁ hb₂)).comp (by fun_prop)
      (mapsTo_image _ _)).intervalIntegrable
  have hI₁ : I₁ = I₃ + I₇ := by
    rw [intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableHoriz
    · exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball w_mem
  have hI₂ : I₂ = I₈ + I₆ := by
    rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableVert
    · exact re_add_im_mul_mem_ball w_mem
    · exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    · exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    · simpa using w_mem
  have hI₀ : I₇ - I₅ + I₈ - I₄ = 0 := by
    have wzInBall : w.re + z.im * I ∈ ball c r :=
      mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
    have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
      (convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall
        (by simpa using hz) (by simpa using wcInBall)
    simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
      hf (z.re + c.im * I) (w.re + z.im * I) hU
  grind [wedgeIntegral]

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
⊢ Δ (f₁ - f₂) x = Δ f₁ x - Δ f₂ x

Tactic:
by
  simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis,
    ← Finset.sum_sub_distrib, iteratedFDeriv_sub_apply h₁ h₂]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ z.arg ∈ Icc 0 (π / 2)

Tactic:
exact ⟨arg_nonneg_iff.2 hz_im, arg_le_pi_div_two_iff.2 (Or.inl hz_re)⟩

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

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
this : Tendsto f (𝓝[<] R) (𝓝 (f R))
⊢ (fun x ↦ c) =ᶠ[𝓝[<] R] f

Tactic:
apply Filter.eventuallyEq_of_mem (Ioo_mem_nhdsLT hR) (fun _ hx ↦ (h₂f hx).symm)

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

Goal state before:
pp: case mpr
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ) <;>
    simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R

Tactic:
apply circleAverage_congr_sphere fun z hz ↦ ?_
      have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz
      match_scalars
      simp only [q, W, real_smul, ofReal_div, coe_algebraMap, mul_one]
      rw [← norm_mul_exp_arg_mul_I w, ← norm_mul_exp_arg_mul_I z, hzR,
        ← circleAverage_re_smul_on_ball_zero_aux, norm_mul_exp_arg_mul_I w]
      field [hR.ne.symm]

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:
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.Log.PosLog

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ log⁺ ↑n = log ↑n

Tactic:
· simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
this : EqOn (f - g) 0 {z | 0 ≤ z.re}
⊢ EqOn f g {z | 0 ≤ z.re}

Tactic:
simpa only [EqOn, Pi.sub_apply, Pi.zero_apply, sub_eq_zero] using this

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
z : ℂ
hz : z ∈ U
⊢ ε < ‖f z - x‖

Tactic:
simpa [dist_eq_norm] using hε z hz

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

Goal state before:
pp: case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ u ∈ closedBall c |R|

Tactic:
apply D.supportWithinDomain

Goal state after:
case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ u ∈ D.support
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
S : Type u_4
T : Type u_5
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
by
  ext g
  induction g using Matrix.ProjGenLinGroup.induction_on with | mk g => simp

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

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖r / ‖‖↑τ‖‖ * ‖↑τ‖ - 1 * ‖↑τ‖‖ < ε

Tactic:
norm_norm,

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖r / ‖↑τ‖ * ‖↑τ‖ - 1 * ‖↑τ‖‖ < ε
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
⊢ ↑g = ↑(upperRightHom (↑g 0 1))

Tactic:
rw [g.val.eta_fin_two]

Goal state after:
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
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(upperRightHom (!![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.g
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
⊢ ↑g = ↑(-upperRightHom (-↑g 0 1))

Tactic:
rw [g.val.eta_fin_two]

Goal state after:
case mp.g
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
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(-upperRightHom (-!![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: τ : ℍ
⊢ ↑(J • τ) = -(starRingEnd ℂ) ↑τ

Tactic:
simp [UpperHalfPlane.coe_smul, σ, J, show ¬(1 : ℝ) < 0 by simp, num, denom]

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

Goal state before:
pp: case e_a
g : SL(2, ℤ)
z : ℍ
i j : Fin 2
⊢ ↑(-toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-g))) i j = ↑((mapGL ℝ) g) i j

Tactic:
simp [toGL]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((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) (diagonal fun m ↦ f (M k k))).det *
        ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R) (diagonal fun m ↦ f 1)).det)

Tactic:
comp_diagonal,

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 *
      (((reindex (Equiv.prodComm n { a // (a ≠ k) = True }) (Equiv.prodComm n { a // (a ≠ k) = True }))
            (blockDiagonal fun m ↦ f (M k k))).det *
        ((reindex (Equiv.prodComm n { a // (a ≠ k) = False }) (Equiv.prodComm n { a // (a ≠ k) = False }))
            (blockDiagonal fun m ↦ f 1)).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 { a // (a = k) = True } { a // (a = k) = True } n n R) (diagonal fun m ↦ f (M k k))).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det

Tactic:
comp_diagonal,

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
⊢ ((reindex (Equiv.prodComm n { a // (a = k) = True }) (Equiv.prodComm n { a // (a = k) = True }))
          (blockDiagonal fun m ↦ f (M k k))).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
⊢ (fun x ↦ ↑((1 / ‖x.im‖₊) ^ 2)) ↑τ =
    (fun x ↦ ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)) ↑τ

Tactic:
simp only [← Real.enorm_eq_ofReal_abs, enorm_eq_nnnorm]

Goal state after:
case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
⊢ ↑((1 / ‖(↑τ).im‖₊) ^ 2) = ↑‖(smulFDeriv g ↑τ).det‖₊ * ↑((1 / ‖(↑(g • ↑ofComplex ↑τ)).im‖₊) ^ 2)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
H : FiniteDimensional (↥K⟮x⟯) L
⊢ FiniteDimensional K L

Tactic:
have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx

Goal state after:
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
H : FiniteDimensional (↥K⟮x⟯) L
this : FiniteDimensional K ↥K⟮x⟯
⊢ FiniteDimensional K L
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: 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
S : Set ((fun X ↦ ↑X.toTop) X)
⊢ IsClosed S → IsClosed (⇑E.symm ⁻¹' S)

Tactic:
hS

Goal state after:
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
S : Set ((fun X ↦ ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E.symm ⁻¹' S)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {a | s ∈ pure a} ∈ b

Tactic:
mem_pure,

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {a | a ∈ s} ∈ b
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ Prod.map π π ⁻¹' diagonal (Quotient R) = range fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
ext ⟨x₁, x₂⟩
    simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
      exists_eq_right]
    rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
this : Continuous[t, compactlyGenerated X] id
⊢ t ≤ compactlyGenerated X

Tactic:
rwa [← continuous_id_iff_le]

Goal state after:
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✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
⊢ NormalSpace (OnePoint X)

Tactic:
by
  suffices R1Space (OnePoint X) by infer_instance
  have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z ↦ by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
  refine ⟨fun x y ↦ ?_⟩
  induction x using OnePoint.rec <;> induction y using OnePoint.rec
  · exact .inl le_rfl
  · exact .inr (key _).symm
  · exact .inr (key _)
  · rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]
    apply specializes_or_disjoint_nhds

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

Goal state before:
pp: E : Type u_2
inst✝ : NormedAddCommGroup E
r : ℝ
f : locallyFinsupp E ℤ
⊢ ((toClosedBall r) f).support ⊆ closedBall 0 |r|

Tactic:
simp_all [toClosedBall, restrict_apply]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
h : e = ⊤
⊢ MonotoneOn (logCounting f e) (Ioi 0)

Tactic:
simpa [logCounting, h] using locallyFinsuppWithin.logCounting_mono (by positivity)

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
h : ¬e = ⊤
⊢ MonotoneOn (logCounting f e) (Ioi 0)

Tactic:
simpa [logCounting, h] using locallyFinsuppWithin.logCounting_mono (by positivity)

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ Fintype.card ↥s ≤ n

Tactic:
apply Nat.le_of_lt_succ

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ Fintype.card ↥s < n.succ
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.map _⟩
  rwa [Wbtw, ← affineSegment_image, hf.mem_image_iff
    ((affineSegment_subset_affineSpan R x z).trans (affineSpan_le.2 (Set.pair_subset hx hz))) hy]
    at h

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite (F.obj j)
hne : ∀ (j : J), Nonempty (F.obj j)
⊢ F.sections.Nonempty

Tactic:
by
  let F' : J ⥤ TopCat := F ⋙ TopCat.discrete
  have : ∀ j, DiscreteTopology (F'.obj j) := fun _ => ⟨rfl⟩
  have : ∀ j, Finite (F'.obj j) := hf
  have : ∀ j, Nonempty (F'.obj j) := hne
  obtain ⟨⟨u, hu⟩⟩ := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} F'
  exact ⟨u, hu⟩

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (f.symm val✝) = x

Tactic:
rw [(eq_some_iff f).2 hfx]

Goal state after:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
hs : s.Nonempty
j : J
⊢ Nonempty ((F.toPreimages s).obj j)

Tactic:
simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]
  obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)
  · exact ⟨(hFn j).some, fun ji => h.elim ji⟩
  · obtain ⟨y, ys⟩ := hs
    obtain ⟨x, rfl⟩ := Fsur ji y
    exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ (M * f.toPEquiv.toMatrix) i j = M.submatrix id (⇑f.symm) i j

Tactic:
rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix

Tactic:
intro f g
  refine not_imp_not.1 ?_
  simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
  intro i hi
  use i
  rcases hf : f i with - | fi
  · rcases hg : g i with - | gi
    · rw [hf, hg] at hi; exact (hi rfl).elim
    · use gi
      simp
  · use fi
    simp [hf.symm, Ne.symm hi]

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)

Tactic:
by
  rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩
  simp [SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)]

Goal state after: