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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 = (↑S * ↑g) 1 0 ^ 2 + (↑S * ↑g) 1 1 ^ 2

Tactic:
Matrix.eta_fin_two g.val,

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 0 ^ 2 + !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1 ^ 2 =
    (↑S * !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1]) 1 0 ^ 2 + (↑S * !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1]) 1 1 ^ 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case «1»
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
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ max √A √A'

Tactic:
· refine le_trans ?_ <| le_max_right √A √A'
    exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA' g hg)

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

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

Tactic:
rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx]

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

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

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l →
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
rintro h; refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
    rw [hasConstantSpeedOnWith_iff_ordered] at h
    rcases le_total x y with (xy | yx)
    · rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]
      exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))
    · rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
      have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
      simp_all only [NNReal.val_eq_coe]; ring

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

Goal state before:
pp: case h₁.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝⁴ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
z : E
h₁ : ¬((toClosedBall a) D) z = 0
a✝³ : ¬a = 0
a✝² : ¬z = 0
a✝¹ : ¬a * ‖z‖⁻¹ = 1
a✝ : ¬a * ‖z‖⁻¹ = -1
⊢ ¬((toClosedBall b) D) z = 0

Tactic:
have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁

Goal state after:
case h₁.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝⁴ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
z : E
h₁ : ¬((toClosedBall a) D) z = 0
a✝³ : ¬a = 0
a✝² : ¬z = 0
a✝¹ : ¬a * ‖z‖⁻¹ = 1
a✝ : ¬a * ‖z‖⁻¹ = -1
this : z ∈ closedBall 0 |a|
⊢ ¬((toClosedBall b) D) z = 0
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)

Tactic:
← erase_biUnion

Goal state after:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)
⊢ #s' ≤ #((s'.biUnion fun x' ↦ t ↑x').erase a)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ (if i = a then some b else none) = some j ↔ some i = some j

Tactic:
if_pos (Subsingleton.elim i a),

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ Option.casesOn (some (f.symm j)) 0 (M i) = M.submatrix id (⇑f.symm) i j

Tactic:
Matrix.submatrix_apply,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ Option.casesOn (some (f.symm j)) 0 (M i) = M (id i) (f.symm j)
Module: Mathlib.Analysis.Convex.Birkhoff

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
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ↑(#A) * s ≤ ↑(#(A.biUnion f)) * s

Tactic:
rw [← h₁, ← h₂]

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
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i, ∑ j ∈ A.biUnion f, M i j
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 : P
h : x ≠ y
⊢ Sbtw R x (midpoint R x y) y

Tactic:
have h : midpoint R x y ≠ x := by simp [h]
  convert! sbtw_pointReflection_of_ne R h
  rw [pointReflection_midpoint_left]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
x : E
hx : x ∈ hull ℝ s
⊢ x ∈ ↑(Submodule.span ℝ s)

Tactic:
PointedCone.mem_hull_set

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
x : E
hx : ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x
⊢ x ∈ ↑(Submodule.span ℝ s)
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
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
⊢ ConvexIndependent 𝕜 Subtype.val

Tactic:
convert! hc.comp_embedding fe

Goal state after:
𝕜 : 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
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
⊢ Subtype.val = p ∘ ⇑fe
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
by
  rw [convexIndependent_set_iff_inter_convexHull_subset]
  constructor
  · rintro hs x hxs hx
    exact (hs _ Set.sdiff_subset ⟨hxs, hx⟩).2 (Set.mem_singleton _)
  · rintro hs t ht x ⟨hxs, hxt⟩
    by_contra h
    exact hs _ hxs (convexHull_mono (Set.subset_sdiff_singleton ht h) hxt)

Goal state after:
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
⊢ ∫ (x : α) in t, f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ

Tactic:
restrict_eq_zero.2 h₀,

Goal state after:
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
⊢ ∫ (x : α), f x ∂0 = μ.real t • ⨍ (x : α), f x ∂μ
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
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
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
⊢ ∑ x ∈ f.weights.support, ∑ x_1 ∈ x.weights.support, (f.weights x * x.weights x_1) • (x_1 -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)

Tactic:
have h_rhs : (∑ d ∈ f.weights.support, f.weights d • d.weights).sum h
      = ∑ d ∈ f.weights.support, (f.weights d • d.weights).sum h :=
    (Finsupp.sum_finsetSum_index (h := h) (fun _ => zero_smul _ _)
      (fun _ _ _ => add_smul _ _ _)).symm

Goal state after:
case e_a
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
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  (∑ d ∈ f.weights.support, f.weights d • d.weights).sum h = ∑ d ∈ f.weights.support, (f.weights d • d.weights).sum h
⊢ ∑ x ∈ f.weights.support, ∑ x_1 ∈ x.weights.support, (f.weights x * x.weights x_1) • (x_1 -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_5
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ↓∩ f ⁻¹' Ici t)

Tactic:
by
  rw [← Topology.IsInducing.subtypeVal.isPreconnected_image,
    image_preimage_eq_inter_range,
    Subtype.range_coe, inter_comm]
  exact (hfc t).isPreconnected

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

Goal state before:
pp: case e'_3.e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ convexCombPair s t hs ht h x y = iConvexComb f ![x, x, y]

Tactic:
delta convexCombPair
    congr 1
    ext a
    simp [StdSimplex.duple, StdSimplex.map, Finsupp.mapDomain,
      Finsupp.sum_fintype, Fin.sum_univ_succ, f, ← add_assoc]

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

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x : ↑(Set.Icc 0 1) × X × X
⊢ 0 ≤ 1 - ↑x.1

Tactic:
by simpa using x.1.prop.right

Goal state after:
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
x y : SimpleGraph V
v w : V
h : (x.Adj ⊔ y.Adj) v w
⊢ (x.Adj ⊔ y.Adj) w v

Tactic:
rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]

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

Goal state before:
pp: V : Type u
v w : V
⊢ (fromEdgeSet Set.univ).Adj v w ↔ ⊤.Adj v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_univ, true_and, top_adj]

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
⊢ Disjoint (interior S) (extremePoints ℝ S)

Tactic:
refine Set.disjoint_iff.mpr fun x ⟨x_int, x_ext⟩ ↦ ?_

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 : x ∈ interior S
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x✝ : A
hx : x✝ ∈ sphere a r
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)

Tactic:
← frontier_closedBall _ hr,

Goal state after:
A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x✝ : A
hx : x✝ ∈ frontier (closedBall a r)
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
u v : V
⊢ ⊥.commonNeighbors u v = ∅

Tactic:
simp [commonNeighbors, neighborSet_bot]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ insert v (G.neighborSet v) = Set.univ ↔ G.IsUniversal v

Tactic:
simp only [Set.ext_iff, Set.mem_insert_iff, mem_neighborSet, IsUniversal]

Goal state after:
V : Type u
G : SimpleGraph V
v : V
⊢ (∀ (x : V), x = v ∨ G.Adj v x ↔ x ∈ Set.univ) ↔ ∀ ⦃w : V⦄, v ≠ w → G.Adj v w
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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x -ᵥ p₁ = a • (p₂ -ᵥ p₁)
⊢ x ∈ s

Tactic:
← eq_vadd_iff_vsub_eq

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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : dist p₃ p < max (dist p₂ p) r
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
hp₃,

Goal state after:
case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < max (dist p₂ p) r
⊢ Wbtw ℝ p₁ p₂ p₃
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < max (dist p₃ p) (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
hp₃,

Goal state after:
case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < max r (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃
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, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Tactic:
obtain ⟨C, hsC, hmax⟩ :=
    zorn_subset_nonempty S
      (fun c hcS hc ⟨_, _⟩ =>
        ⟨⋃₀ c,
          ⟨hc.directedOn.convex_sUnion fun s hs => (hcS hs).1,
            disjoint_sUnion_left.2 fun c hc => (hcS hc).2⟩,
          fun s => subset_sUnion_of_mem⟩)
      s ⟨hs, hst⟩

Goal state after:
𝕜 : 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
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, ‖z i‖ ≤ r
⊢ ‖∑ k ∈ t, w k • z k‖ < r

Tactic:
by
  simp_rw [← mem_closedBall_zero_iff] at hz
  rw [← mem_ball_zero_iff]
  exact sum_mem_ball_of_strictConvexSpace h0 h1 hi hj hij hi0 hj0 hz

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

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist ((affineCombination ℝ t p) w) p₀ < r

Tactic:
affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ h1 p₀,

Goal state after:
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist ((t.weightedVSubOfPoint p p₀) w +ᵥ p₀) p₀ < r
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ p : P
hp : p ∈ s.closedInterior
hp' : ∀ (i : Fin (n + 1)), p ≠ s.points i
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
⊢ dist p p₀ < r

Tactic:
rcases hp with ⟨w, hw, hw01, rfl⟩

Goal state after:
V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
⊢ dist ((affineCombination ℝ univ s.points) w) p₀ < r
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
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity [hφ _ hxy.ne']

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 : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity [hφ _ hxy.ne']

Goal state after: