mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ deriv (iteratedDeriv (n + 1) cosh) = iteratedDeriv (n + 1) sinh

Tactic:
ih,

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ deriv (iteratedDeriv n sinh) = iteratedDeriv (n + 1) sinh
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b

Tactic:
by
  rw [TopologicalSpace.nhds_generateFrom]
  simp only [comap_iInf, comap_principal]
  intro s hs
  rw [← le_principal_iff]
  refine iInf_le_of_le { u | s ∈ u } ?_
  refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_
  exact principal_mono.2 fun _ ↦ id

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
x : α
⊢ IsOpen[induced pure Ultrafilter.topologicalSpace] {x}

Tactic:
use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _

Goal state after:
case right
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
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‖) 0 r

Tactic:
exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)

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)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
d : E
⊢ ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d

Tactic:
simp_rw [this d]

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)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
d : E
⊢ ∃ A ⊆ 𝓕, A.Countable ∧ ⋃ f, U (↑f) d = ⋃ f ∈ A, U f d
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inr
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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ eVariationOn f (s ∩ Icc z x ∪ t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
@eVariationOn.union _ _ _ _ f _ _ x,

Goal state after:
case inl.inr
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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ eVariationOn f (s ∩ Icc z x) + eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - z))

case inl.inr.hs
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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ IsGreatest (s ∩ Icc z x) x

case inl.inr.ht
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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ IsLeast (t ∩ Icc x y) x
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos.refine_2
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : a ∈ closedBall 0 |r|
⊢ 1 ≤ r * ‖a‖⁻¹

Tactic:
simpa [mul_comm r, one_le_inv_mul₀ (norm_pos_iff.mpr h₁a), abs_of_pos h₃r] using h₂a

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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
⊢ ∃ l c, s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l x) + c = a

Tactic:
by
  let A := { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 }
  obtain ⟨L, ⟨b, hLb⟩⟩ := geometric_hahn_banach_point_closed (𝕜 := 𝕜) hφcv.convex_re_epigraph
    (hφc.isClosed_re_epigraph hsc) (by simp [A, hax] : (x, ofReal a) ∉ A)
  let u := L.comp (.inl 𝕜 E 𝕜)
  let c := (re (L (0, 1)))⁻¹
  refine ⟨- c • u, c * re (u x) + a, fun z => ?_, ?_⟩
  · have hv (v : 𝕜) : v * L (0, 1) = L (0, v) := by rw [← smul_eq_mul, ← map_smul]; simp
    have hine {w : E} (h : w ∈ s) : re (L (x, 0)) + re (L (0, 1)) * a
      < re (L (w, 0)) + re (L (0, 1)) * φ w := by
      have hw := hLb.1.trans (hLb.2 _ (by simp [A, h] : (w, ofReal (φ w)) ∈ A))
      rw [← coprod_comp_inl_inr L] at hw
      simpa [-coprod_comp_inl_inr, ← hv (ofReal a), ← hv (ofReal (φ w)), mul_comm a,
        mul_comm (φ w)] using hw
    have hc : 0 < c := inv_pos.2 (pos_of_right_mul_lt_le (lt_of_add_lt_add_left (hine hx)) hax.le)
    simpa [smul_re, u, c, mul_add, ← mul_assoc, inv_mul_cancel₀ (ne_of_gt (inv_pos.1 hc))]
      using mul_le_mul_of_nonneg_left (hine z.2).le hc.le
  · simp [u, c, smul_re]

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' ⟨x'', hx''⟩ ∈ t'' ⟨x'', hx''⟩
⊢ f'' ⟨x'', hx''⟩ ∉ s.biUnion t

Tactic:
mem_sdiff

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' ⟨x'', hx''⟩ ∈ t ↑⟨x'', hx''⟩ ∧ f'' ⟨x'', hx''⟩ ∉ s.biUnion t
⊢ f'' ⟨x'', hx''⟩ ∉ s.biUnion t
Module: Mathlib.Analysis.Convex.BetweenList

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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
· by_cases hl : l = []
    · rcases exists_pair_ne P with ⟨p₁, p₂, hp₁p₂⟩
      exact ⟨p₁, p₂, hp₁p₂, by simp [hl, sortedLT_iff_pairwise]⟩
    · by_cases hlen : l.length = 1
      · rw [length_eq_one_iff] at hlen
        rcases hlen with ⟨p₁, rfl⟩
        rcases exists_ne p₁ with ⟨p₂, hp₂p₁⟩
        exact ⟨p₁, p₂, hp₂p₁.symm, [0], by simp [sortedLT_iff_pairwise]⟩
      · refine ⟨l.head hl, l.getLast hl, ?_⟩
        rw [← exists_map_eq_of_sorted_nonempty_iff_sbtw hl] at h
        simp only [hlen, false_or] at h
        rcases h with ⟨l', hl's, hl'l, hl⟩
        exact ⟨hl, l', hl's, hl'l⟩

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

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a

Tactic:
exact ⟨x, hx, hf₂ x⟩

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

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)

Tactic:
· rintro ⟨f, hf₁, hf₂⟩ s
    rw [← card_image_of_injective s hf₁]
    apply card_le_card
    intro
    rw [mem_image, mem_biUnion]
    rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx, hf₂ x⟩

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

Goal state before:
pp: case pos.refine_2
𝕜 : 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 : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
⊢ ⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i) = s.domRestrict φ

Tactic:
· ext; simp_all

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
⊢ (ConcreteCategory.hom (F.map f)) x ∈ F.eventualRange i

Tactic:
mem_eventualRange_iff

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), (ConcreteCategory.hom (F.map f)) x ∈ range ⇑(ConcreteCategory.hom (F.map f_1))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}

Tactic:
let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
      rintro f i
      refine ⟨f.val i, ?_⟩
      rw [mem_biUnion]
      exact ⟨i, i.property, f.property.2 i⟩

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
have : ∀ j, Fintype (F.obj j) := fun j => Fintype.ofFinite (F.obj j)

Goal state after:
J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this : (j : J) → Fintype (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
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✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
⊢ Sbtw R (Pi.single i₁ 1 i₁) (w i₁) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)

Tactic:
Pi.single_eq_same,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
⊢ Sbtw R 1 (w i₁) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1.left
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 x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 0 ≤ 1 - t₁ + t₁ * t₂

Tactic:
nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]

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

Goal state before:
pp: case hb
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 x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 0 ≤ 1 - t₁ + t₁ * t₂

Tactic:
nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]

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
w x y z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
⊢ t₁ = 1

Tactic:
nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ E
inst✝³ : ContinuousSMul ℝ E
inst✝² : LocallyConvexSpace ℝ E
inst✝¹ : Module ℝ F
p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ
inst✝ : p.IsContPerfPair
C : ProperCone ℝ E
⊢ dual p.flip ↑(dual p ↑C) = C

Tactic:
by
  refine le_antisymm (fun x ↦ ?_) subset_dual_dual
  simp only [mem_dual, SetLike.mem_coe]
  contrapose!
  simpa [p.flip.toContPerfPair.surjective.exists] using C.hyperplane_separation_point

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

Goal state before:
pp: case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c

Tactic:
calc
    ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
    _ ≤ f (ya * a + yc * c) := hfy
    _ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac

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 → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
tfae_have 2 → 3 := by
    obtain ⟨x₀, hx₀⟩ := hC'
    exact fun h ↦ ⟨x₀, hx₀, h.continuousAt <| hC.mem_nhds hx₀⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ ∀ (x : E),
    (∃ a, (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) →
      ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b

Tactic:
rintro _ ⟨z, ⟨x, hx, y, hy, a₁, b₁, ha₁, hb₁, hab₁, rfl⟩, z, hz, a₂, b₂, ha₂, hb₂, hab₂, rfl⟩

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty]; rintro h rfl; exact h intrinsicClosure_empty

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
x✝ : x ∈ f ∘ Subtype.val ⁻¹' f '' s
w✝ : P
hy : w✝ ∈ s
hfy : f w✝ = (f ∘ Subtype.val) x
⊢ x ∈ Subtype.val ⁻¹' s

Tactic:
change (x : P) ∈ s

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
x✝ : x ∈ f ∘ Subtype.val ⁻¹' f '' s
w✝ : P
hy : w✝ ∈ s
hfy : f w✝ = (f ∘ Subtype.val) x
⊢ ↑x ∈ s
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:
rw [← f.isometry.preimage_closedBall]
    exact (strictConvex_closedBall _ _ _).linearIsometry_preimage _

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

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
i : M
⊢ (map f w).weights i = (map g w).weights i

Tactic:
simp only [weights_map]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
i : M
⊢ (mapDomain f w.weights) i = (mapDomain g w.weights) i