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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
⊢ g ∈ Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}

Tactic:
intro i j

Goal state after:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
i j : Fin 2
⊢ |↑g i j| ≤ max √A √A'
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
z : E
f : locallyFinsupp E ℤ
ha : z ∈ closedBall 0 |r|
⊢ ((toClosedBall r) f) z = f z

Tactic:
unfold toClosedBall

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
z : E
f : locallyFinsupp E ℤ
ha : z ∈ closedBall 0 |r|
⊢ ((restrictMonoidHom ⋯) f) z = f z
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) 0 1 =
    circleAverage (fun x ↦ logCounting f (↑x) R) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
rw [← circleAverage_add (circleIntegrable_logCounting h)
        circleIntegrable_log_meromorphicTrailingCoeffAt, circleAverage_congr_sphere]
      intro a ha
      simp [logCounting_add_log_trailingCoeff_eq_circleAverage_add_logCounting_top h hR a]

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

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting D ℓ < logCounting D (1 + ℓ)

Tactic:
apply logCounting_strictMono he

Goal state after:
case hbc.x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ℓ ∈ Ioi ‖e‖

case hbc.x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 + ℓ ∈ Ioi ‖e‖

case hbc.a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ℓ < 1 + ℓ
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : (support D).Finite
⊢ (∑ x ∈ h.toFinset, logCounting (single x (D x))) =O[atTop] log

Tactic:
exact Asymptotics.IsBigO.sum fun _ _ ↦ logCounting_single_isBigO_log

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : f₁ ≤ f₂
hr : 1 ≤ r
⊢ logCounting f₁ r ≤ logCounting f₂ r

Tactic:
← sub_nonneg

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f₂ - f₁
hr : 1 ≤ r
⊢ 0 ≤ logCounting f₂ r - logCounting f₁ r
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f y) (f x) ≠ 0
yx : y ≤ x
⊢ False

Tactic:
exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)

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

Goal state before:
pp: α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
hl : Triplewise p l
⊢ Triplewise q l

Tactic:
induction hl with
  | nil => exact .nil
  | cons head tail ih => exact .cons (head.imp h) ih

Goal state after:
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
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
⊢ IsClosed {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}

Tactic:
let A := { p : E × EReal | p.1 ∈ s ∧ φ p.1 ≤ p.2 }
  have hC : { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 }
    = (Prod.map id ((Real.toEReal ∘ re) : 𝕜 → EReal)) ⁻¹' A := by simp [A]
  refine hC.symm ▸ IsClosed.preimage ?_ ?_
  · exact continuous_id.prodMap <| continuous_coe_real_ereal.comp reCLM.cont
  · exact (lowerSemicontinuousOn_iff_isClosed_epigraph hsc).1
      (continuous_coe_real_ereal.comp_lowerSemicontinuousOn hφ_cont (EReal.coe_strictMono.monotone))

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
x y z : V
p : P
⊢ z +ᵥ p ∈ (fun x ↦ x +ᵥ p) '' affineSegment R x y ↔ z ∈ affineSegment R x y

Tactic:
(vadd_right_injective p).mem_set_image

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
x y z : V
p : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
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'
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
have : Function.Injective f.toAffineMap := f.injective
  -- `refine` or `exact` are very slow, `apply` is fast. Please check before golfing.
  apply this.wbtw_map_iff

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

Goal state before:
pp: case neg
𝕜 : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ

Tactic:
by_cases! hsφ : s.domRestrict φ = 0
    · have := congrFun hsφ
      refine ⟨fun _ => 0, fun _ => 0, ?_, ?_⟩
      · simp_all [domRestrict_def]
      · ext; simp_all
    · obtain ⟨x, hx⟩ := Function.ne_iff.1 hsφ
      have : s = ∅ := by have := congrFun h𝓕'.2.1 x; simp_all
      grind

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

Goal state before:
pp: case 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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))

Tactic:
simp [max_eq_left hji.le, min_eq_right hji.le]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : 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
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous f

Tactic:
by rw [hlc]; fun_prop

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
i : J
f : i ⟶ j
⊢ Function.Injective fun s ↦ ↑s j

Tactic:
refine fun s₀ s₁ h => Subtype.ext <| funext fun k => ?_
  obtain ⟨m, mi, mk, _⟩ := IsCofilteredOrEmpty.cone_objs i k
  dsimp at h
  rw [← s₀.prop (mi ≫ f), ← s₁.prop (mi ≫ f)] at h
  rw [← s₀.prop mk, ← s₁.prop mk]
  exact congr_arg _ (Finj m (mi ≫ f) h)

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ some b = some j ↔ some j = some j

Tactic:
Subsingleton.elim b j

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ some j = some j ↔ some j = some j
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Zero R
inst✝ : One R
⊢ (Equiv.symm σ).toPEquiv.toMatrix = Perm.permMatrix R σ⁻¹

Tactic:
← Equiv.Perm.inv_def

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Zero R
inst✝ : One R
⊢ (toPEquiv σ⁻¹).toMatrix = Perm.permMatrix R σ⁻¹
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case 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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (max i j)) p (s.points (min i j))

Tactic:
simp [max_eq_left hji.le, min_eq_right hji.le]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: case refine_1
R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
⊢ M * N ∈ fun M ↦ ∀ (i j : n), 0 ≤ M i j

Tactic:
intro i j

Goal state after:
case refine_1
R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
i j : n
⊢ 0 ≤ (M * N) i j
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s

Tactic:
rintro ⟨M', hM', rfl⟩

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : M' ∈ doublyStochastic R n
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j, (s • M') i j = s) ∧ ∀ (j : n), ∑ i, (s • M') i j = s
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
⊢ ∃ b ∈ ↑K, ‖x - b‖ < ε

Tactic:
obtain ⟨n, hn⟩ := hu (ε / C) (div_pos hε hC_pos)

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
⊢ ∃ b ∈ ↑K, ‖x - b‖ < ε
Module: Mathlib.Analysis.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hC : (↑C).Nonempty
hSclos : IsClosed ↑C
⊢ C.Pointed

Tactic:
obtain ⟨x, hx⟩ := hC
  let f : 𝕜 → E := (· • x)
  -- The closure of `f (0, ∞)` is a subset of `C`
  have hfS : closure (f '' Set.Ioi 0) ⊆ C :=
    hSclos.closure_subset_iff.2 <| by rintro _ ⟨_, h, rfl⟩; exact C.smul_mem h hx
  -- `f` is continuous at `0` from the right
  have fc : ContinuousWithinAt f (Set.Ioi (0 : 𝕜)) 0 := by fun_prop
  -- `0 ∈ closure f (0, ∞) ⊆ C, 0 ∈ C`
  simpa [f, Pointed, ← SetLike.mem_coe] using hfS <| fc.mem_closure_image <| by simp

Goal state after:
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 : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y ≠ (lineMap x y) r

Tactic:
rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]

Goal state after:
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 : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : 1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

pp: 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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
· rw [sub_eq_zero, eq_comm] at h
    rw [h]
    suffices t₁ = 1 by simp [this]
    exact
      eq_of_le_of_not_lt ht₁.2 fun ht₁lt =>
        (mul_lt_one_of_nonneg_of_lt_one_right ht₂.2 ht₁.1 ht₁lt).ne h

Goal state after:
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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM
    exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3

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✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Collinear R {x, y, z}
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
collinear_iff_of_mem (Set.mem_insert _ _)

Goal state after:
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 : ∃ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
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), x₁ i j = x₂ i j

Tactic:
intro i j

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
⊢ x₁ i j = x₂ i j
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : ((convexHull 𝕜) (p '' s)).Nonempty
⊢ x ∈ s

Tactic:
convexHull_nonempty_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : (p '' s).Nonempty
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ y +ᵥ ⇑h '' closure[inst✝³] (-x +ᵥ s) = closure[inst✝³] t

Tactic:
by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -(2 * |f x₀|) - f y ≤ |r|

Tactic:
sub_le_iff_le_add',

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -(2 * |f x₀|) ≤ f y + |r|
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : t =ᵐ[μ] univ
⊢ ∫ (x : α) in t, f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ

Tactic:
rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : StrictConvexSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall 0 r)

Tactic:
by
    rw [← f.isometry.preimage_closedBall]
    exact (strictConvex_closedBall _ _ _).linearIsometry_preimage _

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Bornology.IsBounded s
⊢ μ (frontier s) = 0

Tactic:
replace hb : μ (interior s) ≠ ∞ := (hb.subset interior_subset).measure_lt_top.ne

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
⊢ μ (frontier s) = 0
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ici y)

Tactic:
intro x hx
  rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy
  · exact hf_cont
  · have h := hf_cvx.continuousOn_interior x
    simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
    rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h
    exact (h hxy).continuousWithinAt

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
⊢ w.weights.support = {x} → w = single x

Tactic:
support_eq_singleton'

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
⊢ (∃ b, b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (interior (⇑φ.symm '' s)).Nonempty

Tactic:
← φ.symm.image_interior,

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (⇑φ.symm '' interior s).Nonempty