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

Goal state before:
pp: ⊢ |rexp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20

Tactic:
apply exp_approx_start

Goal state after:
⊢ |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z ↦ expR (B * expR (c * |u z|))

Tactic:
have : ∀ {c₁ c₂ B₁ B₂}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z,
      ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ := fun hc hB₀ hB z ↦ by
    simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z ↦ expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z ↦ expR (B * expR (c * |u z|))
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ≠ 0

Tactic:
apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero (by fun_prop)
          (meromorphicOrderAt_canonicalFactor_ne_top x hR)

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)

Tactic:
by_cases h : ¬ MeromorphicAt f (x + c)

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ Γ = cov.liftPath (f.comp pγ.toContinuousMap) e₀ ⋯

Tactic:
eq_liftPath_iff'

Goal state after:
case e'_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ p ∘ ⇑Γ = ⇑(f.comp pγ.toContinuousMap) ∧ Γ 0 = e₀
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_3
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ Γ' = cov.liftPath (f.comp pγ'.toContinuousMap) e₀ ⋯

Tactic:
eq_liftPath_iff'

Goal state after:
case e'_3
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ p ∘ ⇑Γ' = ⇑(f.comp pγ'.toContinuousMap) ∧ Γ' 0 = e₀
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ sSupNormIm f z.re

Tactic:
refine le_csSup ?_ ?_

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ f '' re ⁻¹' {z.re})

case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ∈ norm ∘ f '' re ⁻¹' {z.re}
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)
  · simp only [tendsto_const_nhds_iff]
  -- Proof that we can let epsilon tend to zero.
  · rw [interpStrip_eq_of_mem_verticalStrip _ _ hz]
    convert! ContinuousWithinAt.tendsto _ using 2
    · simp only [ofReal_zero, zero_add]
    · simp_rw [← ofReal_add]
      have : ∀ x ∈ Ioi 0, (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re
          = ‖((x + sSupNormIm f 0 : ℝ) ^ (1 - z) * (x + sSupNormIm f 1 : ℝ) ^ z : ℂ)‖ := by
              intro x hx
              simp only [norm_mul]
              repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
              · simp only [sub_re, one_re]
              · simpa using (ne_comm.mpr (ne_of_lt hz.1))
              · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))
      apply tendsto_nhdsWithin_congr this _
      simp only [zero_add]
      rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
      · apply Tendsto.mul
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 0)]
            exact Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [sub_nonneg, le_of_lt hz.2]
        · apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 1)]
            exact Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [le_of_lt hz.1]
      · simpa using (ne_comm.mpr (ne_of_lt hz.1))
      · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))

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

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) x - I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x) I =
    I • (fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) x - I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x) 1

Tactic:
rw [fderiv_comp]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
        1

case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1)

case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) 1) x
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
        1

Tactic:
rw [fderiv_comp]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1

case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I)

case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) I) x
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1

Tactic:
rw [fderiv_comp]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1
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
⊢ IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U

Tactic:
by
  refine ⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩
  obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz
  have : DifferentiableOn ℂ f (ball z r) :=
    (IsConservativeOn.isExactOn_ball (hf'.mono h₁) (hf.mono h₁)).differentiableOn isOpen_ball
  apply (this z (mem_ball_self h₀)).mono_of_mem_nhdsWithin
  exact mem_nhdsWithin.mpr ⟨ball z r, isOpen_ball, mem_ball_self h₀, inter_subset_left⟩

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ circleAverage f c 0 = f c

Tactic:
by
  rw [circleAverage]
  simp only [circleMap_zero_radius, Function.const_apply,
    intervalIntegral.integral_const, sub_zero,
    ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ (mul_ne_zero two_ne_zero pi_ne_zero),
    one_smul]

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}
⊢ circleAverage (⇑g ∘ f) c R = g (f c)

Tactic:
obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e

Goal state after:
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|))
⊢ circleAverage (⇑g ∘ f) c R = g (f c)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
a : ℂ
ha : (ContinuousMultilinearMap.restrictScalars ℝ ∘ iteratedFDeriv ℂ 2 f) a = iteratedFDeriv ℝ 2 f a
this : (iteratedFDeriv ℂ 2 f a) (I • ![1, 1]) = (∏ i, I) • (iteratedFDeriv ℂ 2 f a) ![1, 1]
⊢ Laplacian.laplacian f a = 0 a

Tactic:
simp_all [laplacian_eq_iteratedFDeriv_complexPlane f, ← ha,
    ContinuousMultilinearMap.coe_restrictScalars]

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

Goal state before:
pp: case inr
⊢ Filter.Tendsto (fun x ↦ x * log x) (𝓝 0) (𝓝 (0 * log 0))

Tactic:
zero_mul

Goal state after:
case inr
⊢ Filter.Tendsto (fun x ↦ x * log x) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log 2 + log⁺ ‖a‖ + log⁺ ‖b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2

Tactic:
add_rotate

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_sdiff,
        Set.mem_ofPred_eq, Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
⊢ (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) =ᶠ[codiscreteWithin (sphere 0 |1|)] fun z ↦
    log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
← Pi.add_def,

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage ((fun z ↦ log ‖R‖) + fun z ↦ log ‖z + ↑R⁻¹ * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p = q * g'
⊢ 0 * (aeval z) g' = 0

Tactic:
zero_mul

Goal state after:
case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p = q * g'
⊢ 0 = 0
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p.mirror = q * g'
⊢ 0 * (aeval z) g' = 0

Tactic:
zero_mul

Goal state after:
case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p.mirror = q * g'
⊢ 0 = 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ circleAverage (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖

Tactic:
rw [this, circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])]

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ log ‖w - c - (ρ - c)‖ = log ‖w - ρ‖
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:
simpa using hε₀.trans (hε z hz)

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

Goal state before:
pp: cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : ↑(cd 0) * z + ↑(cd 1) = 0
⊢ cd 0 = 0

Tactic:
apply_fun Complex.im at h

Goal state after:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : (↑(cd 0) * z + ↑(cd 1)).im = Complex.im 0
⊢ cd 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
this : m.discr = (m 0 0 - m 1 1) ^ 2
⊢ m 0 0 - m 1 1 = 0 ↔ m 0 0 = m 1 1

Tactic:
sub_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
this : m.discr = (m 0 0 - m 1 1) ^ 2
⊢ m 0 0 = m 1 1 ↔ m 0 0 = m 1 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
x✝ : m ∈ Set.range ⇑(scalar (Fin 2))
b : K
hb : (scalar (Fin 2)) b = m
⊢ n = 0

Tactic:
← sub_eq_iff_eq_add'

Goal state after:
case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m - (scalar (Fin 2)) a = n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
x✝ : m ∈ Set.range ⇑(scalar (Fin 2))
b : K
hb : (scalar (Fin 2)) b = m
⊢ n = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

Tactic:
calc
    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
    _ = Complex.normSq (denom g z) := by simp [denom, Complex.normSq]; ring

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

Goal state before:
pp: case right
τ : ℍ
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
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ (fun τ ↦ ‖↑τ‖) ξ = r

Tactic:
simp_rw [hξτ, norm_mul, norm_div, norm_real, norm_norm]

Goal state after:
case right
τ : ℍ
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
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ‖r‖ / ‖↑τ‖ * ‖↑τ‖ = r
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) ((norm S) a) = (norm R) a

Tactic:
rw [norm_apply S, norm_apply R a, ← LinearMap.det_restrictScalars]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) ↑(gen K x) = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]

Goal state after: