mathlib-initiative/mathlib-tactics huggingface dataset:
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 z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap ((lineMap w ((lineMap w z) t₁)) t₂) z) ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) = (lineMap w z) t₁

Tactic:
simp only [lineMap_apply, smul_smul, ← add_vadd, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul,
    ← add_smul, vadd_vsub, vadd_right_cancel_iff, div_mul_eq_mul_div, div_sub_div_same]

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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
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)
h : x₁ i j ≠ x₂ i j
h₂ : Equiv.Perm.permMatrix R σ i j ∈ Set.Ioo 0 1
⊢ False

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
s t : Set M
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
aesop

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
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
aesop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
⊢ ‖(ε / ‖x - y‖) • (x - y)‖ ≤ ε

Tactic:
by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']

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

Goal state before:
pp: 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

Tactic:
rw [hc.mem_convexHull_iff] at h

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 : i ∈ s \ {i}
⊢ False
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' closure[inst✝³] s = y +ᵥ ⇑h '' closure[inst✝³] (-x +ᵥ s)

Tactic:
by
        simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]

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 : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|

Tactic:
refine ⟨|r| + 2 * |f x₀|, ?_⟩

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 : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
⊢ ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)
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 : ConcaveOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f| ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x₀) f

Tactic:
simpa [Pi.neg_def, Pi.abs_def] using hf.neg.isBoundedUnder_abs hC

Goal state after:
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
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

Tactic:
convexJoin_assoc,

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
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 s (convexJoin 𝕜 u t)
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
a b c d : E
⊢ convexJoin 𝕜 (convexJoin 𝕜 {a} ((convexHull 𝕜) {b})) (convexJoin 𝕜 {c} ((convexHull 𝕜) {d})) =
    convexJoin 𝕜 {a} (convexJoin 𝕜 {b} (convexJoin 𝕜 {c} ((convexHull 𝕜) {d})))

Tactic:
convexJoin_assoc,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c d : E
⊢ convexJoin 𝕜 {a} (convexJoin 𝕜 ((convexHull 𝕜) {b}) (convexJoin 𝕜 {c} ((convexHull 𝕜) {d}))) =
    convexJoin 𝕜 {a} (convexJoin 𝕜 {b} (convexJoin 𝕜 {c} ((convexHull 𝕜) {d})))
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
hs : IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ s ⊆ range Subtype.val

Tactic:
exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

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

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
⊢ w.restrict {x} hx = single x

Tactic:
classical
  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx

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

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist x (convexCombPair s t hs ht h x y) = t * dist x y

Tactic:
by
  rw [dist_comm, dist_convexCombPair_left]

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : s ∈ K.faces → ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
obtain ⟨t, ht⟩ := hs' hs

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : s ∈ K.faces → ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t
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
n : ℕ
h_card : finrank 𝕜 E + 1 ≤ n
hn : #s = n
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
induction n, h_card using Nat.le_induction generalizing ι with
  | base => exact helly_theorem_corner (le_of_eq hn) h_inter
  /- Construct a family of vectors indexed by `ι` such that the vector corresponding to `i : ι`
  is an arbitrary element of the intersection of all `F j` except `F i`. -/
  | succ k h_card hk =>
  let a (i : s) : E := Set.Nonempty.some (s := ⋂ j ∈ s.erase i, F j) <| by
    apply hk (s := s.erase i)
    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
    · intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
    · simp only [coe_mem, card_erase_of_mem]; lia
  /- This family of vectors is not affine independent because the number of them exceeds the
  dimension of the space. -/
  have h_ind : ¬AffineIndependent 𝕜 a := by
    rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
    · exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)
    · simp only [card_coe]; lia
  /- Use `radon_partition` to conclude there is a subset `I` of `s` and a point `p : E` which
  lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂ i ∈ s, F i`. -/
  obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind
  use p
  apply mem_biInter
  intro i hi
  lift i to s using hi
  /- It suffices to show that for any subcollection `J` of `s` containing `i`, the convex
  hull of `a '' (s \ J)` is contained in `F i`. -/
  suffices ∀ J : Set s, (i ∈ J) → (convexHull 𝕜) (a '' Jᶜ) ⊆ F i by
    by_cases h : i ∈ I
    · exact this I h hp_Ic
    · apply this Iᶜ h; rwa [compl_compl]
  /- Given any subcollection `J` of `ι` containing `i`, because `F i` is convex, we need only
  show that `a j ∈ F i` for each `j ∈ s \ J`. -/
  intro J hi
  rw [convexHull_subset_iff (h_convex i.1 i.2)]
  rintro v ⟨j, hj, hj_v⟩
  rw [← hj_v]
  /- Since `j ∈ Jᶜ` and `i ∈ J`, we conclude that `i ≠ j`, and hence by the definition of `a`:
  `a j ∈ ⋂ F '' (Set.univ \ {j}) ⊆ F i`. -/
  apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
  · apply iInter₂_subset
    simp [mem_erase, ne_of_mem_of_not_mem hi hj]
  · apply Nonempty.some_mem

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

Goal state before:
pp: ι : 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
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
hJ : ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
obtain ⟨J, hJ_ss, hJ_card⟩ := hJ

Goal state after:
ι : 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
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e ∧ w ∈ e
⊢ G.Adj v w

Tactic:
rw [Sym2.mem_and_mem_iff hne] at hv

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : e = s(v, w)
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁ \ G₂).edgeSet

Tactic:
rw [edgeSet_sdiff]

Goal state after:
ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁.edgeSet \ G₂.edgeSet)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s t : Set (Sym2 V)
⊢ fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t

Tactic:
by
  ext v w
  simp only [fromEdgeSet_adj, Set.mem_inter_iff, Ne, inf_adj]
  tauto

Goal state after:
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : x ∈ interior S
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v✝ w : V
e : Sym2 V
inst✝ : DecidableEq V
v : V
x : ↑(G.incidenceSet v)
⊢ (fun w ↦ ⟨s(v, ↑w), ⋯⟩) ((fun e ↦ ⟨G.otherVertexOfIncident ⋯, ⋯⟩) x) = x

Tactic:
simp [otherVertexOfIncident]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : 0 + bz = 1
⊢ ∃ x_1 ∈ segment 𝕜 u v, x_1 ∈ (convexHull 𝕜) {p, q, 0 • x + bz • y}

Tactic:
rw [zero_add] at habz
    rw [zero_smul, zero_add, habz, one_smul]
    refine ⟨v, by apply right_mem_segment, segment_subset_convexHull ?_ ?_ hv⟩ <;> simp

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

Goal state before:
pp: case inr.inr.refine_1
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)
⊢ (lineMap x y) (r₂ / (r₁ + r₂)) ∈ s

pp: case inr.inr.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
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)
⊢ Wbtw R x ((lineMap x y) (r₂ / (r₁ + r₂))) y

Tactic:
· 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₁

Goal state after:
case inr.inr.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
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)
⊢ Wbtw R x ((lineMap x y) (r₂ / (r₁ + r₂))) 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 p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
⊢ s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
by
  refine ⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
  rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm,
    vsub_right_mem_direction_iff_mem hp₁] at h

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y) x_1 = z) ↔
    ∀ (δ : 𝕜), 0 < δ → δ < 1 → (lineMap x y) δ ∉ s

Tactic:
aesop

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

Goal state before:
pp: 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
⊢ IsPreconnected {y | s.SOppSide x y}

Tactic:
by
  rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
  · rw [coe_eq_bot_iff] at h
    simp only [h, not_sOppSide_bot]
    exact isPreconnected_empty
  · by_cases hx : x ∈ s
    · simp only [hx, SOppSide, not_true, false_and, and_false]
      exact isPreconnected_empty
    · exact (isConnected_setOfPred_sOppSide hx h).isPreconnected

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem✝ : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, (lineMap y x) δ ∈ s
δ : 𝕜
hmem : (lineMap y x) δ ∈ s
hsbt : δ ∈ Set.Ioo 0 1
⊢ Sbtw 𝕜 y ((lineMap y x) δ) x

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: case e_6
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1

Tactic:
exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x

Goal state after:
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto f (cocompact E) (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Goal state after:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto (fun x ↦ ‖f x‖) (cocompact E) (𝓝 0)
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
a✝ : E
⊢ a✝ ∈ (Metric.closedBall 0 r)ᶜ → a✝ ∈ (fun x ↦ ‖f x‖) ⁻¹' s

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re ⟪T x, y⟫_𝕜 + re ⟪T y, x⟫_𝕜 = re (2 * ↑(re ⟪T x, y⟫_𝕜))
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4

Tactic:
re_mul_ofReal,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re ⟪T x, y⟫_𝕜 + re ⟪T y, x⟫_𝕜 = re 2 * re ⟪T x, y⟫_𝕜
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜₁
inst✝⁶ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : SeminormedAddCommGroup M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : NormedSpace 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : SeminormedAddCommGroup M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : NormedSpace 𝕜₁ M₁
inst✝² : Module 𝕜₂ M₂
inst✝¹ : ContinuousConstSMul 𝕜₂ M₂
inst✝ : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Goal state after: