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

Goal state before:
pp: case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }

Tactic:
·

Goal state after:
case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }
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 u v ↔ G.Adj w x

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

Tactic:
·

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
⊢ G.Adj u v ↔ G.Adj w x
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 u v ↔ G.Adj w x

Tactic:
·

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case pos
ι : 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
h : Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

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_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
h : ¬Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
·

Goal state after:
case pos
ι : 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
h : Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case pos
ι : 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
hvw : { Adj := Ne, symm := ⋯, loopless := ⋯ }.Adj v w
h : G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

pp: case neg
ι : 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
hvw : { Adj := Ne, symm := ⋯, loopless := ⋯ }.Adj v w
h : ¬G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
·

Goal state after:
case pos
ι : 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
hvw : { Adj := Ne, symm := ⋯, loopless := ⋯ }.Adj v w
h : G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case neg
ι : 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
hvw : { Adj := Ne, symm := ⋯, loopless := ⋯ }.Adj v w
h : ¬G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
·

Goal state after:
case neg
ι : 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
hvw : { Adj := Ne, symm := ⋯, loopless := ⋯ }.Adj v w
h : ¬G.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w
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_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
h : ¬Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

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_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
h : ¬Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
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, F i).Nonempty

Tactic:
by
  apply helly_theorem_compact' h_convex h_compact
  intro I hI_card
  have hJ : ∃ J : Finset ι, I ⊆ J ∧ #J = finrank 𝕜 E + 1 := by
    by_cases h : Infinite ι
    · exact Infinite.exists_superset_card_eq _ _ hI_card
    · have : Finite ι := Finite.of_not_infinite h
      have : Fintype ι := Fintype.ofFinite ι
      apply exists_superset_card_eq hI_card
      simp only [ENat.card_eq_coe_fintype_card] at h_card
      rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card
  obtain ⟨J, hJ_ss, hJ_card⟩ := hJ
  apply Set.Nonempty.mono <| biInter_mono hJ_ss (by intro _ _; rfl)
  exact h_inter J hJ_card

Goal state after:
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_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) := ⋯
⊢ ↑G' ⊆ F

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_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) := ⋯
⊢ #G' ≤ 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_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) := ⋯
⊢ ↑G' ⊆ F
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_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) := ⋯
⊢ #G' ≤ 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_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) := ⋯
⊢ #G' ≤ finrank 𝕜 E + 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
⊢ u ∈ s

pp: case refine_2
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
e : Sym2 V
hadj : e ∈ G.edgeSet
⊢ e ∈ s.sym2

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
⊢ u ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
e : Sym2 V
hadj : e ∈ G.edgeSet
⊢ e ∈ s.sym2

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
e : Sym2 V
hadj : e ∈ G.edgeSet
⊢ e ∈ s.sym2
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_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := ⋯
⊢ ↑J' ⊆ F

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_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := ⋯
⊢ #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_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := ⋯
⊢ ↑J' ⊆ F
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:
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.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ 0

pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
·

Goal state after:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ 1

pp: case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
·

Goal state after:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ 1
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_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := ⋯
⊢ #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_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := ⋯
⊢ #J' = finrank 𝕜 E + 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 0

pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
·

Goal state after:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 1

pp: case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
·

Goal state after:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 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
⊢ s.WOppSide x y → s.WOppSide y x

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
⊢ s.WOppSide y x → s.WOppSide x 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
⊢ s.WOppSide x y → s.WOppSide y x
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
⊢ s.WOppSide y x → s.WOppSide x y

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
⊢ s.WOppSide y x → s.WOppSide x y
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:
simp_rw [← disjoint_edgeSet, ← iUnion_incidenceSet, Set.disjoint_iUnion_left,
    Set.disjoint_iUnion_right, Set.disjoint_left, Sym2.forall]

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (v x y : V), s(x, y) ∈ G.incidenceSet v → s(x, y) ∉ H.incidenceSet v) ↔
    ∀ (i i_1 x y : V), s(x, y) ∈ G.incidenceSet i → s(x, y) ∉ H.incidenceSet i_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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y → s.WSameSide x y

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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y → s.WSameSide (v +ᵥ x) 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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y → s.WSameSide x 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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y → s.WSameSide (v +ᵥ x) y

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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y → s.WSameSide (v +ᵥ x) y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e

pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide (v +ᵥ x) y → s.WOppSide x y

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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y → s.WOppSide (v +ᵥ x) 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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide (v +ᵥ x) y → s.WOppSide x 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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y → s.WOppSide (v +ᵥ x) y

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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y → s.WOppSide (v +ᵥ x) y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

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

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

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
v : V
inst✝ : Nontrivial V
h : G.IsUniversal v
w : V
h' : v = w
⊢ ¬G.IsIsolated w
Module: Mathlib.Combinatorics.SimpleGraph.Basic

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

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
v : V
inst✝ : Nontrivial V
h : G.IsUniversal v
w : V
h' : ¬v = w
⊢ ¬G.IsIsolated w
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsUniversal v
x : V
hx : G.Adj v x
⊢ False

pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsIsolated v
x : V
hx : v ≠ x
⊢ Gᶜ.Adj v x

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsUniversal v
x : V
hx : G.Adj v x
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsIsolated v
x : V
hx : v ≠ x
⊢ Gᶜ.Adj v x

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsIsolated v
x : V
hx : v ≠ x
⊢ Gᶜ.Adj v x
Module: Mathlib.Combinatorics.SimpleGraph.Basic

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

pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ Gᶜ.IsIsolated v

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsIsolated v
⊢ G.IsUniversal v
Module: Mathlib.Combinatorics.SimpleGraph.Basic

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

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ Gᶜ.IsIsolated v