α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), ¬x ∈ nonUniforms ⊥ G ε
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ nonUniforms ⊥ G ε = ∅
rw [eq_empty_iff_forall_not_mem]
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ¬(u, v) ∈ nonUniforms ⊥ G ε
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), ¬x ∈ nonUniforms ⊥ G ε
rintro ⟨u, v⟩
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = u →
      ∀ (x : α),
        x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = v →
          u ≠ v → SimpleGraph.IsUniform G ε u v
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ¬(u, v) ∈ nonUniforms ⊥ G ε
simp only [Finpartition.mk_mem_nonUniforms_iff, Finpartition.parts_bot, mem_map, not_and,
  Classical.not_not, exists_imp]
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α), x ∈ A ∧ {x} = u → ∀ (x : α), x ∈ A ∧ {x} = v → ¬u = v → SimpleGraph.IsUniform G ε u v
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = u →
      ∀ (x : α),
        x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = v →
          u ≠ v → SimpleGraph.IsUniform G ε u v
dsimp
case mk.intro.intro
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε u v
case mk
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α), x ∈ A ∧ {x} = u → ∀ (x : α), x ∈ A ∧ {x} = v → ¬u = v → SimpleGraph.IsUniform G ε u v
rintro x ⟨_,xu⟩  y ⟨_,yv⟩ _
case mk.intro.intro
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε {x} {y}
case mk.intro.intro
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε u v
rw [←xu, ←yv]
no goals
case mk.intro.intro
α : Type u_2
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε {x} {y}
exact G.isUniform_singleton hε