mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: 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
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
x✝ : FundamentalGroupoid X
x : ↑(p ⁻¹' {x✝.as})
⊢ (ConcreteCategory.hom (↾cov.monodromy (𝟙 x✝))).toFun x = (ConcreteCategory.hom (𝟙 ↑(p ⁻¹' {x✝.as}))).toFun x

Tactic:
simpa using! congr_fun cov.monodromy_refl x

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0 ∨ ∀ (x : ℂ), id x - 1 ≠ 0

Tactic:
left

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case pos.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0

Tactic:
left

Goal state after:
case pos.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬1 - z = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0 ∨ 1 - id z ≠ 0

Tactic:
left

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0

Tactic:
left

Goal state after:
case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ w.im = a - b → w.im ∈ Icc (a - b) (a + b)

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ w.im = a + b → w.im ∈ Icc (a - b) (a + b)

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ δ * expR (d * |w.re|) ≤ 0

Tactic:
exacts [fun h => h.symm ▸ left_mem_Icc.2 hab.le, fun h => h.symm ▸ right_mem_Icc.2 hab.le,
      mul_nonpos_of_nonpos_of_nonneg δ₀.le (Real.exp_pos _).le]

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

Goal state before:
pp: case hg.hf
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
this :
  ∀ 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‖
⊢ Tendsto (fun a ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))

Tactic:
← zero_add (sSupNormIm f 1)

Goal state after:
case hg.hf
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
this :
  ∀ 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‖
⊢ Tendsto (fun a ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 1))
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re ∨
    sSupNormIm f 0 ^ (1 - z.re) ≤ 0 ∧ sSupNormIm f 1 ^ z.re ≤ 0

Tactic:
left

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re
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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn (fun x ↦ f (↑x + ↑z.im * I)) s
int1 : IntervalIntegrable (fun x ↦ f (↑x + ↑z.im * I)) volume z.re z.re
int2 : StronglyMeasurableAtFilter (fun x ↦ f (↑x + ↑z.im * I)) (𝓝 z.re) volume
int3 : ContinuousAt (fun x ↦ f (↑x + ↑z.im * I)) z.re
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re

Tactic:
simpa using intervalIntegral.integral_hasDerivAt_right int1 int2 int3 |>.isLittleO

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)

Tactic:
interval_average_eq,

Goal state after:
f : ℝ → ℝ
a b : ℝ
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
⊢ ⨍ (x : ℝ) in a..b, f₁ x = ⨍ (x : ℝ) in a..b, f₂ x

Tactic:
interval_average_eq,

Goal state after:
a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f₁ x = ⨍ (x : ℝ) in a..b, f₂ x
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
a✝ : z ∈ univ
⊢ HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
have h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1)) := h₂.mono (subset_univ _)

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
a✝ : z ∈ univ
h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1))
⊢ HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr
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
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨ζ, hζ, rfl⟩ : ∃ ζ : ℂ, ζ.im ∈ Icc 0 (π / 2) ∧ exp ζ = z := by
    refine ⟨log z, ?_, exp_log hzne⟩
    rw [log_im]
    exact ⟨arg_nonneg_iff.2 hz_im, arg_le_pi_div_two_iff.2 (Or.inl hz_re)⟩

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
⊢ ‖f (cexp ζ)‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) = a

Tactic:
left

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ circleAverage f c R ≤ a

Tactic:
rw [← circleAverage_const a c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
    mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) ≤ ∫ (θ : ℝ) in 0..2 * π, a
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : ¬CircleIntegrable f c R
⊢ 0 ≤ circleAverage f c R

Tactic:
· rw [circleAverage.integral_undef hf]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)

Tactic:
← smul_sub

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    (2 * π)⁻¹ • ((∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ ↑z ≠ 0

Tactic:
exact z.ne_zero

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

Goal state before:
pp: ⊢ IsIntegral ℤ I

Tactic:
by
  refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩
  rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]

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

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 *
      (‖↑R * cexp (↑θ * I)‖ ^ 2 + normSq (↑r * cexp (↑φ * I)) -
        2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤
    (R + r) * (R + r)

pp: case hpos
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2

Tactic:
normSq_eq_norm_sq

Goal state after:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 *
      (‖↑R * cexp (↑θ * I)‖ ^ 2 + ‖↑r * cexp (↑φ * I)‖ ^ 2 -
        2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤
    (R + r) * (R + r)

case hpos
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: ⊢ log⁺ 0 = 0

Tactic:
simp [posLog]

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

Goal state before:
pp: ⊢ log⁺ 1 = 0

Tactic:
simp [posLog]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ log⁺ x

Tactic:
simp [posLog]

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

Goal state before:
pp: x : ℝ
⊢ log⁺ (-x) = log⁺ x

Tactic:
simp [posLog]

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

Goal state before:
pp: x : ℝ
⊢ log⁺ |x| = log⁺ x

Tactic:
simp [posLog]

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

Goal state before:
pp: x : ℝ
⊢ log⁺ |x| = 0 ↔ log |x| ≤ 0

Tactic:
simp [posLog]

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

Goal state before:
pp: case empty
α : Type u_1
f : α → ℝ
⊢ log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)

Tactic:
simp [posLog]

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

Goal state before:
pp: case inl
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
left

Goal state after:
case inl
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

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

Tactic:
left

Goal state after:
| (∫ (x : ℝ) in 0..π / 2, log (sin x)) + ∫ (x : ℝ) in π / 2..π, log (sin x)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1

Tactic:
left

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ f x = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
by
    have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
    rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]
    simp

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

Goal state before:
pp: a b : ℝ
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]
  · rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]
    ring
  all_goals exact intervalIntegrable_log'

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1

Tactic:
left

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ f x = 0
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
left

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := ⋯
gray : E → ℂ → ℂ := ⋯
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
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
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p = 0

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' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0

Tactic:
· obtain ⟨g', hg'⟩ := hq
    rw [hg', aeval_mul, hz, 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' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 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' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0

Tactic:
· obtain ⟨g', hg'⟩ := hq'
    rw [hg', aeval_mul, hz, zero_mul]

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ f c ≤ f z

Tactic:
by
  have h' (n : ℕ) : 0 ≤ iteratedDeriv n (f · - f c) c := by
    cases n with
    | zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
    | succ n =>
      specialize h (n + 1) n.succ_ne_zero
      rw [iteratedDeriv_succ'] at h ⊢
      rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
  exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun z ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
left

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun z ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: τ : ℍ
⊢ ‖cexp (2 * ↑π * Complex.I * ↑τ)‖ < 1

Tactic:
simpa [Function.Periodic.norm_qParam, Complex.norm_exp] using τ.norm_qParam_lt_one 1

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
Z : Type w
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TietzeExtension Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y × Z)
g₁ : C(X✝, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.fst.comp f
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g₂, hg₂⟩ := (ContinuousMap.snd.comp f).exists_restrict_eq hs

Goal state after:
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
Z : Type w
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TietzeExtension Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y × Z)
g₁ : C(X✝, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.fst.comp f
g₂ : C(X✝, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.snd.comp f
⊢ ∃ g, ContinuousMap.restrict s g = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inl.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 ≠ 0
⊢ False

Tactic:
· have : 0 < 1 + √(-g.val.det) / |g 1 0| := by simp [add_pos, *]
        specialize hg ⟨⟨-g 1 1 / g 1 0, 1 + √(-g.val.det) / |g 1 0|⟩, this⟩
        simp [gl_smul_eq_self_iff_dist_eq hlt ha hc, Complex.dist_eq_re_im, Real.sqrt_sq this.le]
          at hg

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

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

Tactic:
by
  ext
  rw [coe_J_smul, ofComplex_apply_of_im_pos (by simpa using τ.im_pos)]

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

Goal state before:
pp: a b : SL(2, ℤ)
⊢ coe a = coe b ↔ a = b

Tactic:
by
  refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
  simp only [Subtype.ext_iff, GeneralLinearGroup.ext_iff] at h
  simpa [coe] using h i j

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 * auxMat M k).map ⇑f)).det

Tactic:
simp_rw [← f.mapMatrix_apply, ← compRingEquiv_apply, map_mul, det_mul, f.mapMatrix_apply,
      compRingEquiv_apply, ((auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
      comp_toSquareBlock (b := (· ≠ k)), det_reindex_self, map_toSquareBlock,
      auxMat_toSquareBlock_eq, auxMat_toSquareBlock_ne, smul_one_eq_diagonal, ← diagonal_one,
      diagonal_map (map_zero _), comp_diagonal, det_reindex_self]
    simp

Goal state after: