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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
by
    obtain rfl | hvw := eq_or_ne v w
    · simp
    · simpa [hvw, not_iff_not] using f.map_adj_iff (v := v) (w := w)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
w : V
⊢ Odd (G.degree w) ∧ w ≠ v ↔ Odd (G.degree w) ∧ w ≠ v

Tactic:
]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ≃g G'
⊢ ⇑f '' ⇑f.toEmbedding ⁻¹' G'.neighborSet (f.toEmbedding v) = G'.neighborSet (f v)

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ≃g G'
⊢ ⇑f '' ⇑f.toEmbedding ⁻¹' G'.neighborSet (f.toEmbedding v) = G'.neighborSet (f v)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (#{w | Odd (G.degree w)} - 1)

pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (#{w | Odd (G.degree w)} - 1)

V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #{w | Odd (G.degree w) ∧ w ≠ v}

Tactic:
rw [← filter_filter, filter_ne', card_erase_of_mem]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (#{w | Odd (G.degree w)} - 1)

V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card W = Fintype.card W

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card W = Fintype.card W
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (G.degree v)

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (G.degree v)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < 2 * k + 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < 2 * k + 1
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ f y + 1 ≤ f y + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ (f y).succ

Tactic:
]

Goal state after:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ (f y).succ
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' ↑s).PairwiseDisjoint f

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' ↑s).PairwiseDisjoint f
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
d : ι'
ha : a ∈ ↑(g d)
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ a ∈ ↑(g d)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
d : ι'
ha : a ∈ ↑(g d)
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ a ∈ ↑(g d)
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : {a | a ∈ l}.Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : {a | a ∈ l}.Pairwise r
hn : l.Nodup
⊢ Pairwise r l
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hn : l.Nodup
⊢ Pairwise r l ↔ Pairwise r l

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1

Tactic:
]

Goal state after:
case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ #s * ?m.204 ≤ #s * (b + 1)

pp: case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = ?m.204

pp: α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ℕ

Tactic:
]

Goal state after:
case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = b + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G = ⊥ ↔ G = ⊥

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G ≠ ⊥ ↔ G ≠ ⊥

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ #⊤.edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ #⊤.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ (∃ w, G.Adj v w) ↔ ∃ w, G.Adj v w

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.degree v = 0 ↔ G.degree v = 0

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ (∃! a, a ∈ G.neighborFinset v) ↔ ∃! w, G.Adj v w

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ (∃! a, a ∈ G.neighborFinset v) ↔ ∃! w, G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Finite

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

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ G.degree v = G.degree v

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card ↑(G.incidenceSet v)

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card ↑(G.incidenceSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑G.edgeSet
⊢ #(G.incidenceFinset v) ≤ #G.edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑G.edgeSet
⊢ #(G.incidenceFinset v) ≤ #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
⊢ Fintype.card V - 1 - k = Fintype.card V - 1 - k

Tactic:
]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ Fintype.card V - 1 = Fintype.card V - 1

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ ∀ (v : V), G.IsIsolated v

Tactic:
]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ ∀ (v : V), G.IsIsolated v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_1
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w

Tactic:
]

Goal state after:
case refine_1
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ #(insert v (G.neighborFinset v)) = Fintype.card V

Tactic:
]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ #(insert v (G.neighborFinset v)) = Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
x : V
inst✝¹ : Fintype ↑(G.neighborSet x)
inst✝ : Fintype ↑(G'.neighborSet (f x))
⊢ Fintype.card ↑(G'.neighborSet (f x)) = Fintype.card ↑(G'.neighborSet (f x))

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithTop.untopD 0 (image (fun x ↦ G'.degree x) univ).min = WithTop.untopD 0 (image (fun v ↦ G'.degree v) univ).min

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithBot.unbotD 0 (image (fun x ↦ G'.degree x) univ).max = WithBot.unbotD 0 (image (fun v ↦ G'.degree v) univ).max

Tactic:
]

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2

Tactic:
]

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ #(induce s G).edgeFinset = #(induce s G).edgeFinset

Tactic:
]

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v

Tactic:
]

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hb : x✝¹ ∈ Finset.map (↑e).toEmbedding P.parts
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
⊢ x✝ ≤ ⊥

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hb : x✝¹ ∈ Finset.map (↑e).toEmbedding P.parts
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
⊢ x✝ ≤ ⊥
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
this : e.symm x✝ ≤ e.symm ⊥
⊢ x✝ ≤ ⊥

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
this : e.symm x✝ ≤ e.symm ⊥
⊢ x✝ ≤ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.degree ↑v ≤ G.degree ↑v

pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.neighborSet ↑v ⊆ s

Tactic:
]

Goal state after:
case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.neighborSet ↑v ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ s ⊆ s

Tactic:
]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ u.sup (id ∘ ⇑(↑e).symm.toEmbedding) = u.sup (⇑e.symm ∘ id)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ u.sup (id ∘ ⇑(↑e).symm.toEmbedding) = u.sup (⇑e.symm ∘ id)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ (↑e).symm ⊥ ∉ P.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ (↑e).symm ⊥ ∉ P.parts