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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)

Tactic:
calc
  -- Bound by the sum from Jensen's formula
  _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]
  _ ≤ Real.log M - Real.log ‖f c‖ := by linarith --Uses jensen and integral_bound
  _ = _ := by rw [← log_div (by linarith) (norm_ne_zero_iff.mpr h₂f)]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2

Tactic:
rw [eq_div_iff (by positivity), dist_eq_norm, ← Complex.normSq_eq_norm_sq, Complex.normSq_apply,
    gl_smul_eq_iff_num_eq, σ, g.val_det_apply, if_neg h.not_gt]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z = Complex.conjCAE ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (¬∃ y, (scalar (Fin 2)) y * ↑g = ↑g * m) ∧ m.discr = 0 ↔ (¬∃ y, (scalar (Fin 2)) y = m) ∧ m.discr = 0

Tactic:
scalar_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (¬∃ y, (diagonal fun x ↦ y) * ↑g = ↑g * m) ∧ m.discr = 0 ↔ (¬∃ y, (diagonal fun x ↦ y) = m) ∧ m.discr = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.right
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
⊢ ((scalar (Fin 2)) a + n - (scalar (Fin 2)) ((((scalar (Fin 2)) a).trace + n.trace) / 2)) ^ 2 = 0

Tactic:
scalar_apply,

Goal state after:
case mpr.right
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
⊢ ((diagonal fun x ↦ a) + n - (scalar (Fin 2)) (((diagonal fun x ↦ a).trace + n.trace) / 2)) ^ 2 = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g).det
⊢ False

Tactic:
· have := isElliptic_of_exists_smul_eq_self hgt hgc ⟨.I, hg _⟩
      contrapose! hg
      simp [gl_smul_eq_self_iff_eq_fixedPt hgt this, exists_ne]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 → ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
refine fun hP ↦ ⟨g 0 0, ?_⟩
    have hb : g 0 1 = 0 := by simpa using congr_arg (coeff · 0) hP
    have hc : g 1 0 = 0 := by simpa using congr_arg (coeff · 2) hP
    have hd : g 1 1 = g 0 0 := by simpa [sub_eq_zero] using congr_arg (coeff · 1) hP
    ext i j
    fin_cases i <;>
    fin_cases j <;>
    simp [hb, hc, hd]

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

Goal state before:
pp: τ : ℍ
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' : r < 0
⊢ False

Tactic:
mem_ball_iff_norm,

Goal state after:
τ : ℍ
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 - ‖↑τ‖‖ < ε
hr' : r < 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
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
⊢ ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε

Tactic:
mem_ball_iff_norm,

Goal state after:
τ : ℍ
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
⊢ ‖↑r / ↑‖↑τ‖ * ↑τ - ↑τ‖ < ε
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
this : ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • { coe := z, coe_im_pos := hz }) =
    ↑(((fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x) { coe := z, coe_im_pos := hz })

Tactic:
simpa [specialLinearGroup_apply, add_mul]

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

Goal state before:
pp: z : ℍ
this✝ : ↑√z.im ≠ 0
this : ↑z.re / ↑√z.im + ↑√z.im * Complex.I = ↑z * (↑√z.im)⁻¹
⊢ ↑(z.toSL2R • I) = ↑z

Tactic:
coe_specialLinearGroup_apply,

Goal state after:
z : ℍ
this✝ : ↑√z.im ≠ 0
this : ↑z.re / ↑√z.im + ↑√z.im * Complex.I = ↑z * (↑√z.im)⁻¹
⊢ (↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 1))) /
      (↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 1))) =
    ↑z
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
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)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ⇑h) a = G y
⊢ g y ∈ t

Tactic:
convert! ha

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
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)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ⇑h) a = G y
⊢ g y = a
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c

Tactic:
simp [dist_comm, mul_comm]

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

Goal state before:
pp: case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

pp: case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom f) → Mono f

Tactic:
· intro hf x₁ x₂ h
    let g₁ : X ⟶ X := ofHom _ ⟨fun _ => x₁, continuous_const⟩
    let g₂ : X ⟶ X := ofHom _ ⟨fun _ => x₂, continuous_const⟩
    have : g₁ ≫ f = g₂ ≫ f := by ext; exact h
    exact CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁

Goal state after:
case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom f) → Mono f
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
rwa [show Ultrafilter.extend g G = g x by rwa [ultrafilter_extend_eq_iff, G.coe_map],
       ultrafilter_extend_eq_iff, F.coe_map]

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

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

Tactic:
exact congr_fun (stoneCechExtend_extends hf) _

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

Goal state before:
pp: case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ (convexHull ℝ) (connectedComponentIn s x) ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)

Tactic:
apply convexHull_mono

Goal state after:
case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ (convexHull ℝ) (connectedComponentIn t x) ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)

Tactic:
apply convexHull_mono

Goal state after:
case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
⊢ w ∈ s ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y

Tactic:
rintro ⟨ws, zwy⟩

Goal state after:
case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ⋯
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∉ closedBall 0 |a|
⊢ 1 ≤ b * ‖z‖⁻¹

Tactic:
apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ⋯
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∉ closedBall 0 |a|
⊢ 1 * ‖z‖ ≤ b
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y → w ∈ t ∩ Icc z y

Tactic:
rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.1, zw, wy⟩
        · exact ⟨wt, zw, wy⟩

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

Tactic:
dsimp only [naturalParameterization]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c' ≤ s.domRestrict f
hlc'_eq : re (l x) + c' = a
y : ℝ
⊢ y • l 1 = l y

Tactic:
← map_smul,

Goal state after:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c' ≤ s.domRestrict f
hlc'_eq : re (l x) + c' = a
y : ℝ
⊢ l (y • 1) = l y
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Injective ↑f
hc : ∀ (x : ↥ι''), ↑f x ∈ t ↑x
⊢ (fun i ↦ ↑f ⟨↑i, ⋯⟩) ∈ hallMatchingsOn t ι'

Tactic:
refine ⟨?_, fun i => hc ⟨i, h i.property⟩⟩

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Injective ↑f
hc : ∀ (x : ↥ι''), ↑f x ∈ t ↑x
⊢ Injective fun i ↦ ↑f ⟨↑i, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
⊢ Convex R ↑(rowStochastic R n)

Tactic:
intro x hx y hy a b ha hb h

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : Matrix n n R
hx : x ∈ ↑(rowStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(rowStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(rowStochastic R n)
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
⊢ Convex R ↑(colStochastic R n)

Tactic:
intro x hx y hy a b ha hb h

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : Matrix n n R
hx : x ∈ ↑(colStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(colStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(colStochastic R n)
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
⊢ Convex R ↑(doublyStochastic R n)

Tactic:
intro x hx y hy a b ha hb h

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : Matrix n n R
hx : x ∈ ↑(doublyStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(doublyStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(doublyStochastic R n)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
x y z : P
h : x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1
⊢ Wbtw R x y z

Tactic:
· rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)
    · exact wbtw_self_left _ _ _
    · rw [Set.mem_Ici] at hr
      refine ⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one_of_one_le₀ hr⟩, ?_⟩
      simp only [lineMap_apply, smul_smul, vadd_vsub]
      rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]

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

Goal state before:
pp: case refine_1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ Set.extremePoints R ↑(doublyStochastic R n) ⊆ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
doublyStochastic_eq_convexHull_permMatrix

Goal state after:
case refine_1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ Set.extremePoints R ((convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}) ⊆
    {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
⊢ x₁ i j = x₂ i j

Tactic:
by_contra! h

Goal state after:
case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ False
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ ↑(doublyStochastic ℝ n)
⊢ ‖M‖ ≤ 1

Tactic:
doublyStochastic_eq_convexHull_permMatrix

Goal state after:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ (convexHull ℝ) {x | ∃ σ, Equiv.Perm.permMatrix ℝ σ = x}
⊢ ‖M‖ ≤ 1
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
i : ↑s
x✝² : i ∈ Finset.univ
f : F →L[ℝ] ℝ
hf : ↑f ∈ dual (Dual.eval ℝ F) ↑C₂
hz : ∀ φ ∈ dual (Dual.eval ℝ E) ↑C₁, ∀ ψ ∈ dual (Dual.eval ℝ F) ↑↑C₂, 0 ≤ ((dualDistrib ℝ E F) (φ ⊗ₜ[ℝ] ψ)) z
h_nonneg : 0 ≤ ((dualDistrib ℝ E F) (b.coord i ⊗ₜ[ℝ] ↑f)) z
x✝¹ : E
x✝ : F
⊢ ((AlgebraTensorModule.curry ((dualDistrib ℝ E F) (b.coord i ⊗ₜ[ℝ] ↑f))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑f ∘ₗ ↑(TensorProduct.lid ℝ F) ∘ₗ LinearMap.rTensor F (b.coord i))) x✝¹) x✝

Tactic:
simp [mul_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : PartialOrder β
inst✝⁷ : TopologicalSpace β
inst✝⁶ : OrderClosedTopology β
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : SMul 𝕜 α
inst✝² : SMul 𝕜 β
inst✝¹ : ContinuousConstSMul 𝕜 β
inst✝ : ContinuousAdd β
s : Set α
⊢ IsClosed[Pi.topologicalSpace]
    (⋂ i ∈ s,
      ⋂ i_1 ∈ s,
        ⋂ i_2,
          ⋂ i_3,
            ⋂ (_ : 0 ≤ i_2),
              ⋂ (_ : 0 ≤ i_3), ⋂ (_ : i_2 + i_3 = 1), {x | x (i_2 • i + i_3 • i_1) ≤ i_2 • x i + i_3 • x i_1})

Tactic:
exact isClosed_iInter fun x => isClosed_iInter fun hx => isClosed_iInter fun y =>
      isClosed_iInter fun hy => isClosed_iInter fun a => isClosed_iInter fun b =>
      isClosed_iInter fun ha => isClosed_iInter fun hb => isClosed_iInter fun hab =>
      isClosed_le (by fun_prop) (by fun_prop)

Goal state after: