Theorem: SimpleGraph.Menger.isMenger_bot (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
⊢ isMenger ⊥
Tactic:
rintro A B
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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut ⊥ A B

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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut ⊥ A B
Tactic:
rw [bot_min_cut]
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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)

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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
let φ (z : (A ∩ B : Finset V)) : AB_Walk ⊥ A B :=
  let h := mem_inter.mp z.prop ; ⟨z, z, h.1, h.2, Walk.nil⟩
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
have φ_inj : Injective φ := by intro u v h ; ext ; simp [φ] at h ; exact h.1
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
refine ⟨image φ univ, ?_, by simp [card_image_of_injective, φ_inj]⟩
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ pwd (image φ univ)

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ pwd (image φ univ)
Tactic:
rintro ⟨a, b, _, _, p⟩ hp ⟨a', b', _, _, q⟩ hq h
State after:
case mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
hp : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ∈ ↑(image φ univ)
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hq : { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q } ∈ ↑(image φ univ)
h : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ≠ { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }

State before:
case mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
hp : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ∈ ↑(image φ univ)
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hq : { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q } ∈ ↑(image φ univ)
h : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ≠ { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
simp at hp hq h
State after:
case mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hp : a = b ∧ (a ∈ A ∧ a ∈ B) ∧ HEq Walk.nil p
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
h : a = a' → b = b' → ¬HEq p q
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }

State before:
case mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hp : a = b ∧ (a ∈ A ∧ a ∈ B) ∧ HEq Walk.nil p
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
h : a = a' → b = b' → ¬HEq p q
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
rcases hp with ⟨rfl, -, h4⟩
State after:
case mk.mk.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' b' : V
ha✝ : a' ∈ A
hb✝¹ : b' ∈ B
q : Walk ⊥ a' b'
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
hb✝ : a ∈ B
p : Walk ⊥ a a
h : a = a' → a = b' → ¬HEq p q
h4 : HEq Walk.nil p
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝¹, to_Walk := q }

State before:
case mk.mk.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' b' : V
ha✝ : a' ∈ A
hb✝¹ : b' ∈ B
q : Walk ⊥ a' b'
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
hb✝ : a ∈ B
p : Walk ⊥ a a
h : a = a' → a = b' → ¬HEq p q
h4 : HEq Walk.nil p
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝¹, to_Walk := q }
Tactic:
rcases hq with ⟨rfl, -, h8⟩
State after:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
p : Walk ⊥ a a
h4 : HEq Walk.nil p
hb✝ : a' ∈ B
q : Walk ⊥ a' a'
h : a = a' → a = a' → ¬HEq p q
h8 : HEq Walk.nil q
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := q }

State before:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
p : Walk ⊥ a a
h4 : HEq Walk.nil p
hb✝ : a' ∈ B
q : Walk ⊥ a' a'
h : a = a' → a = a' → ¬HEq p q
h8 : HEq Walk.nil q
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
subst_vars
State after:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := Walk.nil }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := Walk.nil }

State before:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := Walk.nil }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := Walk.nil }
Tactic:
simp [AB_Walk.Disjoint]
State after:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ ¬a' = a

State before:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ ¬a' = a
Tactic:
rintro rfl
State after:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a' : V
ha✝¹ : a' ∈ A
hb✝¹ : a' ∈ B
ha✝ : a' ∈ A
hb✝ : a' ∈ B
h : a' = a' → a' = a' → ¬HEq Walk.nil Walk.nil
⊢ False

State before:
case mk.mk.intro.intro.intro.intro
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a' : V
ha✝¹ : a' ∈ A
hb✝¹ : a' ∈ B
ha✝ : a' ∈ A
hb✝ : a' ∈ B
h : a' = a' → a' = a' → ¬HEq Walk.nil Walk.nil
⊢ False
Tactic:
simp at h
State after:
no goals

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ Injective φ
Tactic:
intro u v h
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ u = v

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ u = v
Tactic:
ext
State after:
case a
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ ↑u = ↑v

State before:
case a
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ ↑u = ↑v
Tactic:
simp [φ] at h
State after:
case a
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : ↑u = ↑v ∧ HEq Walk.nil Walk.nil
⊢ ↑u = ↑v

State before:
case a
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : ↑u = ↑v ∧ HEq Walk.nil Walk.nil
⊢ ↑u = ↑v
Tactic:
exact h.1
State after:
no goals

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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ card (image φ univ) = card (A ∩ B)
Tactic:
simp [card_image_of_injective, φ_inj]
State after:
no goals