mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inl.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A * A⁻¹)) ≤ K ^ 3 * ↑(#A)

pp: case inr.inr.inr.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

pp: case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
·

Goal state after:
case inr.inr.inl.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A * A⁻¹)) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inr.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

pp: case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
·

Goal state after:
case inr.inr.inr.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
·

Goal state after:
case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) → ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)

pp: case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)) → ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝

Tactic:
·

Goal state after:
case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) → ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)) → ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝

Tactic:
·

Goal state after:
case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)) → ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v → ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v → ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v) → u ∈ ⇑f '' G.neighborSet v

pp: case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v) → u ∈ ⇑f '' G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ (SimpleGraph.map (⇑f) G).support = ⇑f '' G.support

Tactic:
ext; simp [mem_support]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset

Tactic:
← sum_degrees_eq_twice_card_edges,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = ∑ v, 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
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}

pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1

Tactic:
·

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ G.support
⊢ v ∈ s

pp: case refine_2
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe.Adj u v

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ G.support
⊢ v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe.Adj u v

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1

Tactic:
·

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case inl
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 : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding v) ↔ G.Adj v v

pp: case inr
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
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
·

Goal state after:
case inl
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 : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding v) ↔ G.Adj v v
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case inr
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
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
·

Goal state after:
case inr
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
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v 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)} - 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)
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
⊢ 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
⊢ v ∈ {w | Odd (G.degree w)}
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

pp: case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
·

Goal state after:
case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case pos
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

pp: case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∃ y ∈ s, f y < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: case inl
α : 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
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ Function.onFun Disjoint f a b

pp: case inr
α : 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
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b

Tactic:
·

Goal state after:
case inl
α : 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
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ Function.onFun Disjoint f a b
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: case inr
α : 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
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b

Tactic:
·

Goal state after:
case inr
α : 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
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b
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 ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

pp: case neg
α : 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 ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 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 ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
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, G.minDegree = G.degree v

Tactic:
by
  grind [minDegree, WithTop.untopD_coe, min_mem_image_coe <| univ_nonempty.image (G.degree ·)]

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
·

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : IsEmpty V
⊢ G.minDegree ≤ H.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
·

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : IsEmpty V
⊢ G.maxDegree ≤ k

pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : Nonempty V
⊢ G.maxDegree ≤ k

Tactic:
·

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : IsEmpty V
⊢ G.maxDegree ≤ k
Module: Mathlib.Combinatorics.SimpleGraph.Finite

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

Tactic:
·

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : Nonempty V
⊢ G.maxDegree ≤ k
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
⊢ G = ⊥

pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ G.maxDegree = 0

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
⊢ G = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ G.maxDegree = 0

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ G.maxDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.maxDegree = Fintype.card V - 1

pp: case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.maxDegree = Fintype.card V - 1

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.maxDegree = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : IsEmpty V
⊢ G.minDegree ≤ G.maxDegree

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : IsEmpty V
⊢ G.minDegree ≤ G.maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
·

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree
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
inst✝ : Nonempty V
h : G.minDegree = 0
⊢ ∃ v, G.IsIsolated v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
x✝ : ∃ v, G.IsIsolated v
v : V
hv : G.IsIsolated v
⊢ G.minDegree = 0

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
h : G.minDegree = 0
⊢ ∃ v, G.IsIsolated v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
x✝ : ∃ v, G.IsIsolated v
v : V
hv : G.IsIsolated v
⊢ G.minDegree = 0

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
x✝ : ∃ v, G.IsIsolated v
v : V
hv : G.IsIsolated v
⊢ G.minDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.minDegree = Fintype.card V - 1

pp: case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.minDegree = Fintype.card V - 1

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.minDegree = Fintype.card V - 1
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).toFinset

pp: case refine_2
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

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).toFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset 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
v : V
h : G.degree v = Fintype.card V - 1
⊢ G.IsUniversal v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1

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
⊢ G.IsUniversal v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1