mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
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
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ (F i0 ∩ ⋂ i, F i).Nonempty

Tactic:
]

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
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
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
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ (F i0 ∩ ⋂ i, F i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
⊢ G.Adj w x ↔ G.Adj w x

Tactic:
]

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
⊢ G.Adj w x ↔ G.Adj w x

Tactic:
]

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
⊢ max (x.Adj v w) (y.Adj v w)

Tactic:
]

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

Tactic:
]

Goal state after:
ι : 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
⊢ min (x.Adj v w) (y.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 : SimpleGraph V
v w : V
x✝ : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
right✝ : ¬G.Adj v w
⊢ ¬G.Adj v w

Tactic:
]

Goal state after:
ι : Sort u_1
V : Type u
G✝ H : SimpleGraph V
a b c u v✝ w✝ : V
e : Sym2 V
G : SimpleGraph V
v w : V
x✝ : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
right✝ : ¬G.Adj 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
x y : SimpleGraph V
v w : V
h : (x.Adj \ y.Adj) v w
⊢ x.Adj v w ∧ ¬y.Adj v w

Tactic:
]

Goal state after:
ι : 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 v w ∧ ¬y.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
a b : V
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (∀ (i : ι), (f i).Adj a b) ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
]

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

Goal state before:
pp: case neg
ι : 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_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
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
h_card : finrank 𝕜 E + 1 ≤ Fintype.card ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι

Tactic:
]

Goal state after:
case neg
ι : 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_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
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
h_card : finrank 𝕜 E + 1 ≤ Fintype.card ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
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_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
⊢ (⋂ X, ↑X).Nonempty

Tactic:
]

Goal state after:
𝕜 : 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_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
⊢ (⋂ X, ↑X).Nonempty
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_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
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image Subtype.val G
⊢ (⋂₀ ↑G').Nonempty

Tactic:
]

Goal state after:
𝕜 : 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_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
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image Subtype.val G
⊢ (⋂₀ ↑G').Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁ ⊓ G₂ ≤ ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥

Tactic:
]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)
⊢ s.WSameSide x y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : ∀ ⦃a : V⦄, (∃ w, G.Adj a w) → ¬∃ w, H.Adj a w
⊢ ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet

Tactic:
]

Goal state after:
V : Type u
G H : SimpleGraph V
h : ∀ ⦃a : V⦄, (∃ w, G.Adj a w) → ¬∃ w, H.Adj a w
⊢ ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1

Tactic:
]

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊥ ↔ G = ⊥

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G ≠ ⊥ ↔ G ≠ ⊥

Tactic:
]

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
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ ↑J.toFinset).Nonempty

Tactic:
]

Goal state after:
𝕜 : 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
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ ↑J.toFinset).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 : e = s(v, w)
⊢ G.Adj v w

Tactic:
]

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: V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : G.Adj v w
⊢ G.Adj v w

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : G.Adj v w
⊢ G.Adj v w
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (fp₂ -ᵥ f y)
⊢ s.WOppSide x y

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
fp₁ : P'
hfp₁ : ∃ y ∈ s, f y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, f y = fp₂
h : SameRay R (f x -ᵥ fp₁) (fp₂ -ᵥ f y)
⊢ s.WOppSide x y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
v : V
h : v ∈ e
he : s(Sym2.Mem.other h, v) ∈ G.edgeSet
⊢ Sym2.Mem.other h ≠ v

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
e : Sym2 V
v : V
h : v ∈ e
he : s(Sym2.Mem.other h, v) ∈ G.edgeSet
⊢ Sym2.Mem.other h ≠ v
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
⊢ Fintype ↑∅

Tactic:
]

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
⊢ Fintype ↑∅
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₁.edgeSet ∪ G₂.edgeSet)

Tactic:
]

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: ι : 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)

Tactic:
]

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: ι : 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_inf]

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: ι : 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)

Tactic:
]

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.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: this : ⇑sqrt = fun x ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ (1 / 2)

Tactic:
]

Goal state after:
this : ⇑sqrt = fun x ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ (1 / 2)
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.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Ici 0) fun x ↦ (fun x ↦ x ^ (1 / 2)) x

Tactic:
]

Goal state after:
⊢ StrictConcaveOn ℝ (Ici 0) fun x ↦ (fun x ↦ x ^ (1 / 2)) x
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case a
𝕜 : 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
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_fin : Fintype ↑J
hJ_card : #J.toFinset = finrank 𝕜 E + 1
J' : Finset (Set E) := J.toFinset
⊢ #J' = finrank 𝕜 E + 1

Tactic:
]

Goal state after:
case a
𝕜 : 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
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_fin : Fintype ↑J
hJ_card : #J.toFinset = finrank 𝕜 E + 1
J' : Finset (Set E) := J.toFinset
⊢ #J' = finrank 𝕜 E + 1
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
]

Goal state after:
case mp
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)

Tactic:
]

Goal state after:
case mpr
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ t \ Sym2.diagSet ⊆ t

Tactic:
]

Goal state after:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ t \ Sym2.diagSet ⊆ t
Module: Mathlib.Combinatorics.SimpleGraph.Basic

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

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (s \ Sym2.diagSet) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
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 : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅

Tactic:
]

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: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint s G.edgeSet ↔ Disjoint s G.edgeSet

Tactic:
]

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 ↑(s \ Sym2.diagSet)

Tactic:
]

Goal state after:
ι : 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 ↑(s \ Sym2.diagSet)
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 y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ x ∉ s ∧ y ∉ s

Tactic:
]

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 : y = x
hyz : y = z
⊢ y = x

Tactic:
]

Goal state after:
𝕜 : 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 : y = x
hyz : y = z
⊢ y = x
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
⊢ SameRay R 0 (y -ᵥ x)

Tactic:
]

Goal state after:
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
⊢ SameRay R 0 (y -ᵥ x)
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
⊢ SameRay R 0 (x -ᵥ y)

Tactic:
]

Goal state after:
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
⊢ SameRay R 0 (x -ᵥ y)
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) ⊆ closedBall x r ∧
    Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : Nontrivial A
x : A
r : ℝ
⊢ extremePoints ℝ (closedBall x r) ⊆ closedBall x r ∧
    Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))
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
⊢ e ∈ G.incidenceSet a

Tactic:
]

Goal state after:
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
⊢ e ∈ G.incidenceSet a
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✝ ∈ closedBall a r \ interior (closedBall a r)
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)

Tactic:
]

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✝ ∈ closedBall a r \ interior (closedBall a r)
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)
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
⊢ sphere x r = sphere x r

Tactic:
]

Goal state after: