-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
@[simp] lemma isUniform_singleton : G.IsUniform ε {a} {b} ↔ 0 < ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
⊢ G.IsUniform ε {a} {b} ↔ 0 < ε

Tactic:
refine ⟨IsUniform.pos, fun hε s' hs' t' ht' hs ht ↦ ?_⟩

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(#{a}) * ε ≤ ↑(#s')
ht : ↑(#{b}) * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
⊢ |↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'

Result:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(#{b})
⊢ |↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(#s')
ht : ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
⊢ |↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
exact (hε.not_le hs).elim

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
simpa using hs

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(#{a}) * ε ≤ ↑(#s')
ht : ↑(#{b}) * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
rw [card_singleton, Nat.cast_one, one_mul] at hs ht

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(#s')
ht : ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
exact (hε.not_le ht).elim

Result:
no goals

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
replace hs : ε ≤ 0 := by simpa using hs

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(#{b})
⊢ |↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
rwa [sub_self, abs_zero]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
replace ht : ε ≤ 0 := by simpa using ht

Result:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
simpa using ht

Result:
no goals