Theorem: SimpleGraph.Minus.card_edge (Untitled/Graphs/Minus.lean)

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
let φ (f : (G -ₑ e).edgeSet) : G.edgeSet := ⟨f, edgeSet_subset_edgeSet.mpr Minus_le f.2⟩
State after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
have φ_inj : Injective φ := by intro e₁ e₂ h ; ext1 ; simpa using h
State after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
apply Fintype.card_lt_of_injective_of_not_mem (b := ⟨_, h⟩) φ φ_inj
State after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := e, property := h } ∉ Set.range φ

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := e, property := h } ∉ Set.range φ
Tactic:
rcases e with ⟨x, y⟩
State after:
case mk.mk
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
x y : V
h : Quot.mk (Sym2.Rel V) (x, y) ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ Quot.mk (Sym2.Rel V) (x, y))) → ↑(edgeSet G) :=
  fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := Quot.mk (Sym2.Rel V) (x, y), property := h } ∉ Set.range φ

State before:
case mk.mk
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
x y : V
h : Quot.mk (Sym2.Rel V) (x, y) ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ Quot.mk (Sym2.Rel V) (x, y))) → ↑(edgeSet G) :=
  fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := Quot.mk (Sym2.Rel V) (x, y), property := h } ∉ Set.range φ
Tactic:
simp [Minus]
State after:
no goals

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Injective φ
Tactic:
intro e₁ e₂ h
State after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ e₁ = e₂

State before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ e₁ = e₂
Tactic:
ext1
State after:
case a
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ ↑e₁ = ↑e₂

State before:
case a
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ ↑e₁ = ↑e₂
Tactic:
simpa using h
State after:
no goals