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
f : ℂ → E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
x✝ : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
⊢ DifferentiableWithinAt ℂ f U z

Tactic:
obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
x✝ : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
⊢ DifferentiableWithinAt ℂ f U z
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
have hs' : s ⊆ Ι a b := by intro x hx; rcases hx with ⟨h1, h2⟩; grind

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, circleAverage (f i) c R

Tactic:
by
  unfold circleAverage
  simp [← Finset.smul_sum, intervalIntegral.integral_finsetSum h]

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

Goal state before:
pp: x : { x // 0 < x }
z : ℍ
⊢ 0 < (↑x • ↑z).im

Tactic:
by simpa using mul_pos x.2 z.im_pos

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

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

Tactic:
Complex.norm_def,

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

Goal state before:
pp: case neg
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
hlt : ‖0‖ < ‖f ↑x₀‖
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
      simpa only [exists_prop] using! hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this

Goal state after:
case neg
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
hlt : ‖0‖ < ‖f ↑x₀‖
⊢ ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f ↑x‖ ≤ ‖f ↑x₀‖
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: ⊢ Continuous log⁺

Tactic:
rw [continuous_iff_continuousAt]
  intro x
  by_cases hx : x = 0
  · apply ContinuousAt.congr (f := fun _ ↦ 0) (by fun_prop)
    filter_upwards [Metric.ball_mem_nhds _ zero_lt_one] with y hy
    rw [eq_comm, posLog_eq_zero_iff y]
    simp_all [le_of_lt]
  rw [posLog_def]
  fun_prop

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

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
f : α → ℝ
hs : s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

pp: case neg
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
· simp [hs, posLog]

Goal state after:
case neg
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)

Tactic:
by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]

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

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

Tactic:
norm_num at this

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
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 ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2

Tactic:
Complex.norm_def,

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

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ContinuousOn (fun x ↦ -x⁻¹ * (log x)⁻¹ ^ 2) [[a, b]]
⊢ ContinuousOn (deriv fun t ↦ (log t)⁻¹) [[a, b]]

Tactic:
convert this using 2 with x

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
this : ContinuousOn (fun x ↦ -x⁻¹ * (log x)⁻¹ ^ 2) [[a, b]]
x : ℝ
⊢ deriv (fun t ↦ (log t)⁻¹) x = -x⁻¹ * (log x)⁻¹ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)

Tactic:
let C := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
  have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
  have hu : ∀ x ∈ [[a, b]],
      HasDerivAt (fun y => cos y ^ (n + 1)) (-(n + 1 : ℕ) * sin x * cos x ^ n) x :=
    fun x _ => by
      simpa only [mul_right_comm, neg_mul, mul_neg] using! (hasDerivAt_cos x).pow (n + 1)
  have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_sin x
  have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
  · calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) := by
        rw [integral_sub, mul_sub, add_sub_assoc] <;>
          apply Continuous.intervalIntegrable <;> fun_prop
  all_goals apply Continuous.intervalIntegrable; fun_prop

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

Goal state before:
pp: a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ (2 * 0 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
norm_num at this

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 0 * cos x ^ (2 * 1 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
norm_num at this

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2 = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
norm_num at this

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 1 + 1) * cos x ^ 0 = ∫ (u : ℝ) in cos b..cos a, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
norm_num at this

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
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
z : ℂ
hz : z ∈ U
⊢ f z ≠ x

Tactic:
by simpa using hε₀.trans (hε z hz)

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
t₀ : c ∈ CB
t₁ : AccPt c (𝓟 CB)
⊢ ∑ᶠ (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:
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.Topology.TietzeExtension

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

Tactic:
by ext; subsingleton

Goal state after:
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
inst✝² : Nonempty n
F : Type u_3
inst✝¹ : Field F
inst✝ : IsAlgClosed F
r : Fˣ
x : F
hx : (X ^ Fintype.card n - C ↑r).IsRoot x
hx' : x ≠ 0
⊢ { val := x, inv := x⁻¹, val_inv := ⋯, inv_val := ⋯ } ^ Fintype.card n = r

Tactic:
by
    simpa [Units.ext_iff, sub_eq_zero] using hx

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

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

pp: case inr
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

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

Goal state after:
case inr
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
simp only [atImInfty_basis.mem_iff, true_and]

Goal state after:
S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S
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).mapMatrix (f.polyToMatrix (cornerAddX M k).det)).det = (f M.det).det

Tactic:
← RingHom.comp_apply,

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.comp 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).mapMatrix (↑(compRingEquiv m n R[X]) (f.polyToMatrix.mapMatrix (cornerAddX M k)))).det =
    (↑(compRingEquiv m n R) (f.mapMatrix M)).det

Tactic:
← RingHom.comp_apply,

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.comp ((↑(compRingEquiv m n R[X])).comp f.polyToMatrix.mapMatrix)) (cornerAddX M k)).det =
    (((↑(compRingEquiv m n R)).comp f.mapMatrix) M).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ (denom g ↑τ)⁻¹

Tactic:
simpa using contMDiff_denom_zpow g (-1)

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inr
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 : g y ≤ c
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
refine ⟨xl y, xu, ?_, hyxu.le⟩

Goal state after:
case inr.inr.inr
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 : g y ≤ c
⊢ f (xl y) ≤ (g - dg) y
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)
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
let F : X →ᵇ ℝ :=
    { toFun := (↑) ∘ h ∘ f
      continuous_toFun := by fun_prop
      map_bounded' := isBounded_range_iff.1
        ((isBounded_Ioo (-1 : ℝ) 1).subset <| range_subset_iff.2 fun x => (h (f x)).2) }

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' := ⋯ }
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
σ : L →ₐ[K] AlgebraicClosure L
⊢ σ x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) σ) x)

Tactic:
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
      AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]

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

Goal state before:
pp: α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s

Tactic:
refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: 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
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst✝¹] (fst ∘ Ψ '' fst ⁻¹' s)

Tactic:
have : CompactSpace t := isCompact_iff_compactSpace.mp ht

Goal state after:
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
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this✝ : s • t = fst ∘ Ψ '' fst ⁻¹' s
this : CompactSpace ↑t
⊢ IsClosed[inst✝¹] (fst ∘ Ψ '' fst ⁻¹' s)
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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
⊢ C(OnePoint ℕ, Y) ≃ { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }

Tactic:
refine (continuousMapDiscreteEquiv ℕ Y).trans {
    toFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [← Nat.cofinite_eq_atTop]⟩
    invFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [Nat.cofinite_eq_atTop]⟩ }

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 R - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]

Goal state after:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall 0 |R|)) u) * log (R * ‖0 - u‖⁻¹) + ↑((divisor f (closedBall 0 |R|)) 0) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖ -
      Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
β : ℝ
hβ : β ∈ uIcc 0 (2 * π)
⊢ (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α β = circleAverage (fun x ↦ log ‖f (circleMap 0 R β) - x‖) 0 1

Tactic:
by
          simp [F, circleAverage, Cartan.cartanKernel]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
have U_open {f} (hf : f ∈ 𝓕) (d : E) : IsOpen (U f d) := h𝓕_cont f hf |>.isOpen_preimage d

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos.refine_2
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : a ∈ closedBall 0 |r|
⊢ 1 ≤ r * ‖a‖⁻¹

Tactic:
· simpa [mul_comm r, one_le_inv_mul₀ (norm_pos_iff.mpr h₁a), abs_of_pos h₃r] using h₂a

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ locallyFinsuppWithin.logCounting (divisor (f₁ + f₂) univ)⁻ r ≤
    (locallyFinsuppWithin.logCounting (divisor f₁ univ)⁻ + locallyFinsuppWithin.logCounting (divisor f₂ univ)⁻) r

Tactic:
rw [← locallyFinsuppWithin.logCounting.map_add]

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ locallyFinsuppWithin.logCounting (divisor (f₁ + f₂) univ)⁻ r ≤
    locallyFinsuppWithin.logCounting ((divisor f₁ univ)⁻ + (divisor f₂ univ)⁻) r
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r

Tactic:
rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))

Goal state after: