mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
hg : AnalyticOn 𝕜 g univ
⊢ locallyFinsuppWithin.logCounting (divisor (f + g) univ)⁻ = locallyFinsuppWithin.logCounting (divisor f univ)⁻

Tactic:
hf.meromorphicOn.negPart_divisor_add_of_analyticNhdOn_right
    (isOpen_univ.analyticOn_iff_analyticOnNhd.1 hg)

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
hg : AnalyticOn 𝕜 g univ
⊢ locallyFinsuppWithin.logCounting (divisor f univ)⁻ = locallyFinsuppWithin.logCounting (divisor f univ)⁻
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
⊢ HasConstantSpeedOnWith f (Icc x z) l

pp: case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
yx : y ≤ x
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
· rcases le_total y z with (yz | zy)
    · rw [← Set.Icc_union_Icc_eq_Icc xy yz]
      exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)
    · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
      rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]

Goal state after:
case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
yx : y ≤ x
⊢ HasConstantSpeedOnWith f (Icc x z) l
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R w x z

Tactic:
by
  rcases h₁ with ⟨t₁, ht₁, rfl⟩
  rcases h₂ with ⟨t₂, ht₂, rfl⟩
  refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩
  rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ιA f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd

Tactic:
apply Finset.mem_union_left

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) := ⋯
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) := ⋯
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ιA f ∈ Finset.image ιA A.snd
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
x✝ : β
⊢ x✝ ∈ R.image ↑A ↔ x✝ ∈ ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)

Tactic:
simp [SetRel.image]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ Injective toFun

Tactic:
rintro ⟨f₁, f₂, hf⟩ ⟨g₁, g₂, hg⟩ (rfl : f₁ = g₁)

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
g₂ : β → Option α
hg : ∀ (a : α) (b : β), g₂ b = some a ↔ f₁ a = some b
⊢ { toFun := f₁, invFun := f₂, inv := hf } = { toFun := f₁, invFun := g₂, inv := hg }
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e_y.e_a
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
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ ({i, j}.orderEmbOfFin ⋯) 1 = max i j

Tactic:
convert! Finset.orderEmbOfFin_last _ _
    · exact (Finset.max'_pair i j).symm
    · lia

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
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
hs : s.Nonempty
j : J
⊢ Nonempty ((F.toPreimages s).obj j)

Tactic:
by
  simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]
  obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)
  · exact ⟨(hFn j).some, fun ji => h.elim ji⟩
  · obtain ⟨y, ys⟩ := hs
    obtain ⟨x, rfl⟩ := Fsur ji y
    exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ ∀ (x : β), f x✝ = some x → ¬(if x = b then some c else none) = some a✝

Tactic:
intros

Goal state after:
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
⊢ ¬(if x✝ = b then some c else none) = some a✝¹
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e'_11
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
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ ({i, j}.orderEmbOfFin ⋯) 1 = max i j

Tactic:
convert! Finset.orderEmbOfFin_last _ _
    · exact (Finset.max'_pair i j).symm
    · lia

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : x ∈ (convexHull 𝕜) ↑t
⊢ t ∈ {t | ↑t ⊆ s ∧ x ∈ (convexHull 𝕜) ↑t}

Tactic:
exact ⟨ht₁, ht₂⟩

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

Goal state before:
pp: case refine_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ False

Tactic:
apply hwe

Goal state after:
case refine_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := ⋯
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ w e • e = 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)

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:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s✝ t : Set M
y✝ : N
s : Set M
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : N
hy : y ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (c • y)

Tactic:
by rw [← Nonneg.coe_smul, map_smul]; exact mul_nonneg c.2 (hy hx)

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

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}

Tactic:
have hg0 : g 0 = a := AffineMap.lineMap_apply_zero a x

Goal state after:
E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}
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] {f | ConvexOn 𝕜 s f}

Tactic:
by
  simp only [ConvexOn, ofPred_and, ofPred_forall]
  refine IsClosed.inter isClosed_const ?_
  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:
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
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))

Tactic:
refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : p i ∈ (convexHull 𝕜) (p '' (s \ {i}))
⊢ False

case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
⊢ i ∈ s
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ ∀ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i} ⊆ interior ((convexHull ℝ) (range ⇑b)) + ↑u

Tactic:
intros

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
i✝ : E
j✝ : i✝ ∈ ↑u
⊢ interior ((convexHull ℝ) (range ⇑b)) + {i✝} ⊆ interior ((convexHull ℝ) (range ⇑b)) + ↑u
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
h : IsInducing Subtype.val
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = closure[inst✝¹] s ∩ ↑(affineSpan 𝕜 s)

Tactic:
h.closure_eq_preimage_closure_image,

Goal state after:
𝕜 : 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
h : IsInducing Subtype.val
⊢ Subtype.val '' Subtype.val ⁻¹' closure[inst✝¹] (Subtype.val '' Subtype.val ⁻¹' s) =
    closure[inst✝¹] s ∩ ↑(affineSpan 𝕜 s)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case refine_1
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ico y z) f

Tactic:
exact hf_cvx.subset Ico_subset_Icc_self (convex_Ico y z)

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
x : P
⊢ (Finset.affineCombination R {x} id) ⇑(Finsupp.single x 1) = x

Tactic:
exact ({x} : Finset P).affineCombination_of_eq_one_of_eq_zero _ _
    (Finset.mem_singleton_self x) Finsupp.single_eq_same fun j _ hne => Finsupp.single_eq_of_ne hne

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

Goal state before:
pp: case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_card : finrank 𝕜 E + 1 ≤ #s
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
generalize hn : #s = n

Goal state after:
case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_card : finrank 𝕜 E + 1 ≤ #s
n : ℕ
hn : #s = n
⊢ (⋂ i ∈ s, F i).Nonempty
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
have hp₀' : 0 < 1 / p := div_pos zero_lt_one hp₀

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ p
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ fromEdgeSet s ≤ G ↔ s \ Sym2.diagSet ⊆ G.edgeSet

Tactic:
by simp [← edgeSet_subset_edgeSet]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.edgeSet = s → G = fromEdgeSet s ∧ Disjoint s Sym2.diagSet

Tactic:
by rintro rfl; simp +contextual [Set.disjoint_right]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v : V
inst✝ : Nontrivial V
h : G.IsUniversal v
w : V
h' : ¬v = w
⊢ ¬G.IsIsolated w

Tactic:
exact Adj.not_isIsolated_right (h h')

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

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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s ∧ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
and_congr_right_iff

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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s ∧ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
and_congr_right_iff

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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Tactic:
and_congr_right_iff

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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case hxy
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = 2⁻¹ * dist x z

Tactic:
← div_eq_inv_mul

Goal state after:
case hxy
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = dist x z / 2
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = 2⁻¹ * dist x z

Tactic:
← div_eq_inv_mul

Goal state after:
case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = dist x z / 2
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ ((convexHull 𝕜) (insert c C))ᶜ
h✝ : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜) (insert c C)) t
⊢ False

Tactic:
exact hc (subset_convexHull _ _ <| mem_insert _ _)

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

Goal state before:
pp: case mp
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
s : AffineSubspace R P
x y : P
⊢ s.WSameSide x y ∧ s.WOppSide x y → x ∈ s ∨ y ∈ s

Tactic:
rintro ⟨hs, ho⟩

Goal state after:
case mp
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
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide x y
⊢ x ∈ s ∨ y ∈ s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inr.inr
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
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ∃ p ∈ s, Wbtw R x p y

Tactic:
refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩
    · have : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) =
          (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) := by
        rw [← neg_vsub_eq_vsub_rev p₂ y]
        linear_combination (norm := match_scalars <;> field) (r₁ + r₂)⁻¹ • h
      rw [lineMap_apply, ← vsub_vadd x p₁, ← vsub_vadd y p₂, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
        ← vadd_assoc, vadd_eq_add, this]
      exact s.smul_vsub_vadd_mem (r₂ / (r₁ + r₂)) hp₂ hp₁ hp₁
    · exact Set.mem_image_of_mem _
        ⟨by positivity,
          div_le_one_of_le₀ (le_add_of_nonneg_left hr₁.le) (Left.add_pos hr₁ hr₂).le⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)

Tactic:
simpa [add_comm, -neg_le_neg_iff, le_sub_iff_add_le'] using hf.2 hx hy ha hb hab

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

Goal state before:
pp: case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
rw [coe_eq_bot_iff] at h

Goal state after:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | s.WSameSide x y}