-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem nonuniformWitness_spec (h₁ : s ≠ t) (h₂ : ¬G.IsUniform ε s t) : ε ≤ |G.edgeDensity
    (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|

Proof state:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s|

Tactic:
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|

Tactic:
unfold nonuniformWitness

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Proof state:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]

Result:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s|

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|

Tactic:
exact G.nonuniformWitnesses_spec h₂

Result:
no goals

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rw [if_pos lt, if_neg (asymm lt)]

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
h₁ : s ≠ s
h₂ : ¬G.IsUniform ε s s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
            (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
          G.edgeDensity s s|

case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Proof state:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
h₁ : s ≠ s
h₂ : ¬G.IsUniform ε s s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
            (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
          G.edgeDensity s s|

Tactic:
cases h₁ rfl

Result:
no goals