case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))

case refine'_2
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : ∀ ⦃H : SimpleGraph V⦄, H ≤ G → p H → r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
s : Finset (Sym2 V)
hs : s ⊆ edgeFinset G
hG : p (deleteEdges G ↑s)
⊢ r ≤ ↑(card s)
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
⊢ DeleteFar G p r ↔ ∀ ⦃H : SimpleGraph V⦄, H ≤ G → p H → r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
refine' ⟨fun h H hHG hH => _, fun h s hs hG => _⟩
case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
this : p (deleteEdges G ↑(edgeFinset G \ edgeFinset H)) → r ≤ ↑(card (edgeFinset G \ edgeFinset H))
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
have := h (sdiff_subset G.edgeFinset H.edgeFinset)
case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
this : p H → r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
this : p (deleteEdges G ↑(edgeFinset G \ edgeFinset H)) → r ≤ ↑(card (edgeFinset G \ edgeFinset H))
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
simp only [deleteEdges_sdiff_eq_of_le _ hHG, edgeFinset_mono hHG, card_sdiff,
  card_le_of_subset, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
no goals
case refine'_1
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : DeleteFar G p r
H : SimpleGraph V
hHG : H ≤ G
hH : p H
this : p H → r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
⊢ r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
exact this hH
no goals
case refine'_2
ι : Sort ?u.169924
𝕜 : Type u_1
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝⁴ : OrderedRing 𝕜
inst✝³ : Fintype V
inst✝² : Fintype (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
p : SimpleGraph V → Prop
r r₁ r₂ : 𝕜
h : ∀ ⦃H : SimpleGraph V⦄, H ≤ G → p H → r ≤ ↑(card (edgeFinset G)) - ↑(card (edgeFinset H))
s : Finset (Sym2 V)
hs : s ⊆ edgeFinset G
hG : p (deleteEdges G ↑s)
⊢ r ≤ ↑(card s)
simpa [card_sdiff hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
  card_le_of_subset hs] using h (G.deleteEdges_le s) hG