mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Goal state after:
case «0».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (m 0 0 - (m 0 0 + m 1 1) / 2) * (m 0 0 - (m 0 0 + m 1 1) / 2) + m 0 1 * m 1 0 =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Goal state after:
case «0».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (m 0 0 - (m 0 0 + m 1 1) / 2) * m 0 1 + m 0 1 * (m 1 1 - (m 0 0 + m 1 1) / 2) = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «1».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Goal state after:
case «1».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m 1 0 * (m 0 0 - (m 0 0 + m 1 1) / 2) + (m 1 1 - (m 0 0 + m 1 1) / 2) * m 1 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «1».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Goal state after:
case «1».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m 1 0 * m 0 1 + (m 1 1 - (m 0 0 + m 1 1) / 2) * (m 1 1 - (m 0 0 + m 1 1) / 2) =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ ↑(g • z) = ↑{ coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }

Tactic:
simp [coe_smul_of_det_pos hg]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ (↑g).trace ≠ 0 ∧ True

Tactic:
and_true,

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ (↑g).trace ≠ 0
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
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
⊢ ⇑(const Y ((a + b) / 2) + g) ∘ e = ⇑f

Tactic:
ext x

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
x : X
⊢ (⇑(const Y ((a + b) / 2) + g) ∘ e) x = f x
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ (trace ℝ ℂ) z = 2 * z.re

Tactic:
Algebra.trace_eq_matrix_trace Complex.basisOneI,

Goal state after:
z : ℂ
⊢ ((leftMulMatrix basisOneI) z).trace = 2 * z.re
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
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' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ⇑g ∘ e = ⇑f

Tactic:
ext x

Goal state after:
case refine_2
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' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
x : X
⊢ (⇑g ∘ e) x = f x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
⊢ inversion c R c = c

Tactic:
simp [inversion]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ inversion c 0 x = c

Tactic:
simp [inversion]

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

Goal state before:
pp: a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Tactic:
Complex.dist_self_conj,

Goal state after:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * (2 * |(↑b).im|))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a.e_a
a b c : ℍ
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im

Tactic:
rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
      mul_comm] <;> exact (im_pos _).le

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

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center |log z.im - log w.im|) = w.im * |Real.sinh (log z.im - log w.im)|

Tactic:
← log_div z.im_ne_zero w.im_ne_zero,

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist ↑z ↑(w.center |log (z.im / w.im)|) = w.im * |Real.sinh (log (z.im / w.im))|
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
⊢ Set.range ⇑toGL = ⇑GeneralLinearGroup.det ⁻¹' {1}

Tactic:
ext x

Goal state after:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
x : GL n A
⊢ x ∈ Set.range ⇑toGL ↔ x ∈ ⇑GeneralLinearGroup.det ⁻¹' {1}
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case refine_1
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } = 𝟙 X

Tactic:
ext x

Goal state after:
case refine_1
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑X.toTop
⊢ (ConcreteCategory.hom (f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE })) x = (ConcreteCategory.hom (𝟙 X)) x
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y

Tactic:
ext x

Goal state after:
case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑Y.toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f)) x = (ConcreteCategory.hom (𝟙 Y)) x
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
⊢ stoneCechExtend hg ∘ stoneCechUnit = g

Tactic:
ext x

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ (stoneCechExtend hg ∘ stoneCechUnit) x = g x
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
⊢ (fun f ↦ ofHom (fun x ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ })
      ((fun f ↦ TopCat.ofHom { toFun := ⇑(ConcreteCategory.hom f) ∘ stoneCechUnit, continuous_toFun := ⋯ })
        { hom := { hom' := { toFun := f, continuous_toFun := hf } } }) =
    { hom := { hom' := { toFun := f, continuous_toFun := hf } } }

Tactic:
ext x

Goal state after:
X : TopCat
Y : CompHaus
f : ↑(stoneCechObj X).toTop → ↑Y.toTop
hf : Continuous f
x : ↑(of (fun x ↦ True) (StoneCech ↑X)).toTop
⊢ (ConcreteCategory.hom
        ((fun f ↦ ofHom (fun x ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ })
          ((fun f ↦ TopCat.ofHom { toFun := ⇑(ConcreteCategory.hom f) ∘ stoneCechUnit, continuous_toFun := ⋯ })
            { hom := { hom' := { toFun := f, continuous_toFun := hf } } })))
      x =
    (ConcreteCategory.hom { hom := { hom' := { toFun := f, continuous_toFun := hf } } }) 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
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
⊢ g ∘ f = Function.diag

Tactic:
ext x

Goal state after:
case fst
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 := ⋯
proper_f : IsProperMap f
g : G × X → X × X := ⋯
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).1 = (Function.diag x).1

case snd
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 := ⋯
proper_f : IsProperMap f
g : G × X → X × X := ⋯
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).2 = (Function.diag x).2
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✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
⊢ (fun f ↦
        {
          toFun := fun x ↦
            match x with
            | none => Classical.choose ⋯
            | Option.some x => ↑f x,
          continuous_toFun := ⋯ })
      ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f) =
    f

Tactic:
ext x

Goal state after:
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ((fun f ↦
          {
            toFun := fun x ↦
              match x with
              | none => Classical.choose ⋯
              | Option.some x => ↑f x,
            continuous_toFun := ⋯ })
        ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
      x =
    f x
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) = (∑ i ∈ s, fun x ↦ log⁺ ‖f i x‖) + fun x ↦ log ↑s.card

Tactic:
ext x

Goal state after:
case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
⊢ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card = ((∑ i ∈ s, fun x ↦ log⁺ ‖f i x‖) + fun x ↦ log ↑s.card) x
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) ⊤ = n • proximity f ⊤

Tactic:
ext x

Goal state after:
f : ℂ → ℂ
n : ℕ
x : ℝ
⊢ proximity (f ^ n) ⊤ x = (n • proximity f ⊤) x
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:

Tactic:
characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R := by simp
  _ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R := by
    rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
  _ = log ‖meromorphicTrailingCoeffAt f 0‖ := by
    rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
    unfold Function.locallyFinsuppWithin.logCounting
    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
⊢ Integrable (fun β ↦ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ) μ

Tactic:
apply Integrable.mono (h_int_Bound.const_mul (2 * π))
      h_meas_K.stronglyMeasurable.integral_prod_left'.aestronglyMeasurable

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := ⋯
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, ‖∫ (x : ℝ), (cartanKernel f R (x, a).1 (x, a).2)⁺ ∂μ‖ ≤ ‖2 * π * (log⁺ ‖f (circleMap 0 R a)‖ + log 2)‖
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: case pos.refine_1
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ y - z ∈ (↑E)ᶜ

Tactic:
simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]

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

Goal state before:
pp: case pos.refine_2
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ y + z ∈ (↑E)ᶜ

Tactic:
simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]

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}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
d : E
⊢ {x | s x < d} = ⋃ f, U (↑f) d

Tactic:
ext x

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)
d : E
x : X
⊢ x ∈ {x | s x < d} ↔ x ∈ ⋃ f, U (↑f) d
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0

Tactic:
by_contra! ⟨h, hfs⟩
    simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
    push Not at hfs
    obtain ⟨x, xs, y, ys, hxy⟩ := hfs
    rcases le_total x y with (xy | yx)
    · exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)
    · rw [edist_comm] at hxy
      exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0

Tactic:
· rintro h x _ y _
    simpa [h] using eVariationOn.mono (s := s) f inter_subset_left

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
⊢ (s'.biUnion fun x_1 ↦ t ↑x_1) = (image (fun z ↦ ↑z) s').biUnion t

Tactic:
ext x

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x✝ : ι
a : α
s' : Finset ↑{x' | x' ≠ x✝}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
x : α
⊢ (x ∈ s'.biUnion fun x ↦ t ↑x) ↔ x ∈ (image (fun z ↦ ↑z) s').biUnion t
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
⊢ sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c} = s.domRestrict φ

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
⊢ sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c} x = s.domRestrict φ x
Module: Mathlib.Analysis.Convex.Between

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

Tactic:
hf.wbtw_map_iff hx hy hz,

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'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Wbtw R x y z ∧ f y ≠ f x ∧ f y ≠ f z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
r : ℝ
hr : r < s.domRestrict φ x
z : ℝ
hz : r < z ∧ z < s.domRestrict φ x
l : E →L[𝕜] 𝕜
c : ℝ
hlc : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l ↑x) + c = z
⊢ ∃ a ∈ range fun f ↦ ↑f x, r < a

Tactic:
exact ⟨z, hlc.2 ▸ ⟨⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩, hz.1⟩

Goal state after: