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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u / denom h u + ↑(↑g 1 1)) = num g (num h u / denom h u) * denom (g * h) u

Tactic:
div_add' _ _ _ (denom_ne_zero_of_im _ hu),

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * ((↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u) =
    num g (num h u / denom h u) * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: 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
⊢ 0 < (1 + Complex.I).im

Tactic:
by simp

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * num h u / denom h u + ↑(↑g 0 1)) * denom (g * h) u

Tactic:
div_add' _ _ _ (denom_ne_zero_of_im _ hu),

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * num h u + ↑(↑g 0 1) * denom h u) / denom h u * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ z.im ≤ (↑(↑N * -n) +ᵥ z).im

Tactic:
by simp

Goal state after:
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 : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun t ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)

Tactic:
rw [← zero_mul ‖f‖]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun t ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((mapGL ℝ) g))

Tactic:
by simp

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

Goal state before:
pp: t : ℝ
ht : 0 < t
⊢ { coe := ↑I * ↑t, coe_im_pos := ⋯ }.im = t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddGroup α
f : ℍ → α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ im ⁻¹' Set.Ici ia, f x ∈ Metric.closedBall 0 ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ ε

Tactic:
by simp

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

Goal state before:
pp: ⊢ !![-1, 0; 0, 1].det ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
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 →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
⊢ Disjoint (Iic c) {b}

Tactic:
· exact Set.disjoint_singleton_right.2 hcb.not_ge

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

Goal state before:
pp: g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
⊢ Set.InjOn ((fun z ↦ ↑(g • ↑ofComplex z)) ∘ UpperHalfPlane.coe) s

Tactic:
by simp

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),

Goal state after:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) sinh = cosh

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) cosh = sinh

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sinh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 sinh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cosh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 cosh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sinh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 sinh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 cosh)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 cosh)

Tactic:
by simp

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

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by
  ext w; constructor
  · rintro ⟨w, hw, rfl⟩
    exact dist_eq_iff_dist_coe_center_eq.1 hw
  · intro hw
    lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)
    exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ CompactSpace ↑{u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
← isCompact_iff_compactSpace

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ IsCompact {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
⊢ (∞ ∈ univ → IsCompact (some ⁻¹' univ)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' univ)

Tactic:
by simp

Goal state after:
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
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
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✝ : IsTopologicalGroup G
x✝ : G × G
⊢ (fun gh ↦ (gh.1 * gh.2⁻¹, gh.2)) ((fun gh ↦ (gh.1 * gh.2, gh.2)) x✝) = x✝

Tactic:
by simp

Goal state after:
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✝ : IsTopologicalGroup G
x✝ : G × G
⊢ (fun gh ↦ (gh.1 * gh.2, gh.2)) ((fun gh ↦ (gh.1 * gh.2⁻¹, gh.2)) x✝) = x✝

Tactic:
by simp

Goal state after:
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✝ : IsTopologicalGroup G
x✝ : Gᵐᵒᵖ × G
⊢ (fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2)) ((fun gh ↦ (gh.2 * unop gh.1, gh.2)) x✝) = x✝

Tactic:
by simp

Goal state after:
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✝ : IsTopologicalGroup G
x✝ : G × G
⊢ (fun gh ↦ (gh.2 * unop gh.1, gh.2)) ((fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2)) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x

Tactic:
rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]; rfl

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
z : X
⊢ Disjoint (𝓝 ↑z) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
disjoint_sup_right,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (map some (coclosedCompact X)) ∧ Disjoint (𝓝 ↑z) (pure ∞)
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✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ univ ⊆ {↑val} ∪ {↑val}ᶜ

Tactic:
by simp

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

Goal state before:
pp: ⊢ Continuous ↿num

Tactic:
unfold num

Goal state after:
⊢ Continuous ↿fun g z ↦ ↑(↑g 0 0) * z + ↑(↑g 0 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
⊢ !![0, -1; 1, 0].det = 1

Tactic:
by simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
⊢ ℱ ≤ 𝓟 s → ℱ ≤ 𝓝 x → x ∈ s

Tactic:
hℱ₂

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
⊢ ℱ ≤ 𝓝 x → x ∈ s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

pp: case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
· apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))

Goal state after:
case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)

Tactic:
by
    rw [logCounting_inv]

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R

Tactic:
by simp

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0

Tactic:
by simp

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

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)

Tactic:
apply add_le_add (proximity_mul_zero_le h₁f₁ h₁f₂ r)
    (logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → f a_1 - a.untop₀ = g a_1 - a.untop₀

Tactic:
by simp

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

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

Tactic:
exact locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const h hR

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ Triplewise p (l₁ ++ l₂) ↔
    Triplewise p l₁ ∧
      Triplewise p l₂ ∧ (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) l₁

Tactic:
induction l₁ with

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

Goal state before:
pp: case cons.refine_2.refine_1.cons.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False

Tactic:
· simpa using hp.1 head hat

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

Goal state before:
pp: case neg.cons
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

Tactic:
by_cases ht2 : tail = []

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : ¬tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail
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'
f : P →ᵃ[R] P'
x y : P
⊢ (fun x_1 ↦ f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(lineMap (f x) (f y)) '' Set.Icc 0 1

Tactic:
← comp_lineMap

Goal state after:
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'
f : P →ᵃ[R] P'
x y : P
⊢ (fun x_1 ↦ f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(f.comp (lineMap x y)) '' Set.Icc 0 1
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ f x - 1 < f x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
l' : List R
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ ∀ (a b : R), (lineMap (l.head hl) (l.getLast hl)) a ≠ (lineMap (l.head hl) (l.getLast hl)) b → a ≠ b

Tactic:
by simp

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✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0

Tactic:
simp [sub_eq_zero, ht.1.ne.symm, ht.2.ne, hxz.symm]

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✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y : P
r : R
⊢ x ≠ y → ((lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)

Tactic:
intro hxy

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y : P
r : R
hxy : x ≠ y
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ (lineMap (s.points 0) (s.points 1)) (w 1) ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
exact Set.mem_image_of_mem _ (h01 _)

Goal state after: