Theorem: SimpleGraph.Menger.transportable_of_not_dart (Untitled/Graphs/Menger.lean)

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
⊢ Walk.transportable_to (G -ₑ Dart.edge e) p
Tactic:
intro f hf
State after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ Adj (G -ₑ Dart.edge e) f.toProd.1 f.toProd.2

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ Adj (G -ₑ Dart.edge e) f.toProd.1 f.toProd.2
Tactic:
simp [Minus, f.is_adj, Dart.edge]
State after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ ¬(f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd)

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ ¬(f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd)
Tactic:
intro hef
State after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
hef : f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd
⊢ False

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
hef : f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd
⊢ False
Tactic:
cases hef with
| inl h1 => exact h <| Dart.ext _ _ h1 ▸ hf
| inr h2 => rw [← Dart.symm_toProd] at h2 ; exact h' <| Dart.ext _ _ h2 ▸ hf
State after:
no goals

State before:
case inl
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h1 : f.toProd = e.toProd
⊢ False
Tactic:
exact h <| Dart.ext _ _ h1 ▸ hf
State after:
no goals

State before:
case inr
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = Prod.swap e.toProd
⊢ False
Tactic:
rw [← Dart.symm_toProd] at h2
State after:
case inr
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = (Dart.symm e).toProd
⊢ False

State before:
case inr
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = (Dart.symm e).toProd
⊢ False
Tactic:
exact h' <| Dart.ext _ _ h2 ▸ hf
State after:
no goals