mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
ι : Sort u_2
f : ι → Set (Sym2 V)
⊢ fromEdgeSet (⋂ i, f i) = ⨅ i, fromEdgeSet (f i)

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: 𝕜 : 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 (Set E)
h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ F).Nonempty

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide x y ↔ s.WOppSide y x

Tactic:
by

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

Goal state before:
pp: V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ fromEdgeSet s ≤ fromEdgeSet t

Tactic:
by

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

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

Tactic:
by

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:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid A
inst✝¹ : Module 𝕜 A
inst✝ : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
x✝ : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
⊢ y = z

Tactic:
by

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

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

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.SOppSide x y ↔ s.SOppSide y x

Tactic:
by

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
s : Set (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑s
⊢ Fintype ↑(fromEdgeSet s).edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ Disjoint G H ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ⋃ v, G.incidenceSet v = G.edgeSet

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid A
inst✝¹ : Module 𝕜 A
inst✝ : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
⊢ C \ interior C ⊆ extremePoints 𝕜 C

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ s.WSameSide x y

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ s.WOppSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.incidenceSet v) (H.incidenceSet v)) ↔ Disjoint G H

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : Nontrivial A
x : A
r : ℝ
⊢ extremePoints ℝ (closedBall x r) ⊆ sphere x r

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
e : Sym2 V
h : a ≠ b
ha : e ∈ G.incidenceSet a
hb : e ∈ G.incidenceSet b
⊢ G.Adj a b

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ extremePoints ℝ (closedBall x r) = sphere x r

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a : V
⊢ a ∉ G.neighborSet a

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ⊆ {v}ᶜ

Tactic:
by

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

Goal state before:
pp: a b : ℝ
hab : a ≤ b
⊢ extremePoints ℝ (Icc a b) = {a, b}

Tactic:
by

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
s : ι → SimpleGraph V
v : V
⊢ (⨆ i, s i).neighborSet v = ⋃ i, (s i).neighborSet v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
inst✝ : Nonempty ι
s : ι → SimpleGraph V
v : V
⊢ (⨅ i, s i).neighborSet v = ⋂ i, (s i).neighborSet v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
⊢ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}

Tactic:
by

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

Goal state before:
pp: V : Type u
v : V
⊢ ⊤.neighborSet v = {v}ᶜ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V), Disjoint (G.commonNeighbors u v) (H.commonNeighbors u v)) ↔ Disjoint G H

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
v w : V
⊢ ⊤.commonNeighbors v w = Set.univ \ {v, w}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ e ∈ G.incidenceSet (G.otherVertexOfIncident h)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ e ∈ G.incidenceSet (G.otherVertexOfIncident h)

Tactic:
by
  use h.1
  simp [otherVertexOfIncident, Sym2.other_mem']

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ G.neighborSet v

Tactic:
by

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
inst✝ : DecidableEq V
v : V
x : ↑(G.incidenceSet v)
⊢ (fun w ↦ ⟨s(v, ↑w), ⋯⟩) ((fun e ↦ ⟨G.otherVertexOfIncident ⋯, ⋯⟩) x) = x

Tactic:
by

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
inst✝ : DecidableEq V
v : V
x✝ : ↑(G.neighborSet v)
w : V
hw : w ∈ G.neighborSet v
⊢ (fun e ↦ ⟨G.otherVertexOfIncident ⋯, ⋯⟩) ((fun w ↦ ⟨s(v, ↑w), ⋯⟩) ⟨w, hw⟩) = ⟨w, hw⟩

Tactic:
by

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

Goal state before:
pp: V : Type u
⊢ Subsingleton (SimpleGraph V) ↔ Subsingleton V

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y

Tactic:
by

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

Goal state before:
pp: V : Type u
⊢ Nontrivial (SimpleGraph V) ↔ Nontrivial V

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v = ∅ ↔ G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ (G.neighborSet v).Nonempty ↔ ¬G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ v ∈ G.support ↔ ¬G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ v ∉ G.support ↔ G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ (∃ u, G.Adj v u) ↔ ¬G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊥ ↔ ∀ (v : V), G.IsIsolated v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y

Tactic:
by

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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v = {v}ᶜ ↔ G.IsUniversal v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.IsUniversal v ↔ G.IsIsolated v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ Gᶜᶜ.IsUniversal v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.IsIsolated v ↔ G.IsUniversal v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊤ ↔ ∀ (v : V), G.IsUniversal v

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hx : x ∈ s
⊢ s.WSameSide y z

Tactic:
by

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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hy : y ∈ s
⊢ s.WOppSide x z

Tactic:
by

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 : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p

Tactic:
by

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✝⁵ : CommRing 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₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : 0 ≤ c₁ * c₂
⊢ s.WSameSide x y

Tactic:
by

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✝⁵ : CommRing 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₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
⊢ p₂ -ᵥ y = -c₂ • m

Tactic:
by

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✝⁵ : CommRing 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₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ 0 ≤ c₁ * -c₂

Tactic:
by

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✝⁵ : CommRing 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₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
⊢ s.WOppSide x y

Tactic:
by

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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1

Tactic:
by

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 : Sbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
by

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 : P
⊢ s.WOppSide x x ↔ x ∈ s

Tactic:
by

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 : P
⊢ ¬s.SOppSide x x

Tactic:
by

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 : Wbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ∑ j ∈ t, w j = 0
ws : ∀ j ∈ t, w j = 0
⊢ i' ∈ t ∨ j' ∈ t

Tactic:
by

Goal state after:
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
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 : bz = 1
⊢ v ∈ segment 𝕜 u v

Tactic:
by

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

Goal state before:
pp: 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
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₁
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
by_cases hp₃p₂ : p₃ = p₂
    · simp [hp₃p₂]
    have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
    have hs' := hs.dist_lt_max_dist p
    rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false] at hs'
    exact False.elim (hp₂.not_gt hs')

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
⊢ s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
by

Goal state after: