Theorem: SimpleGraph.Menger.AB_Walk.push_lift (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
f : V → V'
hf : Adapted G f
⊢ LeftInverse (push f) (lift f hf)
Tactic:
rintro ⟨a, b, ha, hb, p⟩
State after:
case mk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p }) =
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }

State before:
case mk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p }) =
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }
Tactic:
ext <;> try simp [push, lift]
State after:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p

State before:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have h1 := Classical.choose_spec (mem_image.mp ha) |>.2
State after:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p

State before:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have h2 := Classical.choose_spec (mem_image.mp hb) |>.2
State after:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p

State before:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have : HEq (p.copy rfl rfl) p := by rfl
State after:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
this : HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p

State before:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
this : HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
convert this
State after:
no goals

State before:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq (push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p })).to_Walk
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.to_Walk
Tactic:
simp [push, lift]
State after:
case mk.to_Walk
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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p

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
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
Tactic:
rfl
State after:
no goals