-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x'_1 : V
hx'_1 : Membership.mem (γ := Finset V) {x, b} x'_1
p : cycles.Walk a x'_1
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
x' : V
hx' : Membership.mem (γ := Set V) {x, b} x'
c' : V
hc : c' ≠ a
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
w : V
hw : ∀ (y : V), (fun (w : V) ↦ M1.Adj x' w) y → y = w
inl :
  ∀ {M1 : (G ⊔ edge x' b).Subgraph} (hxa : G.Adj x' a) (hnGxb : ¬G.Adj x' b) (hnxb : x' ≠ b) (hnxc : x' ≠ c)
    (hM1 : M1.IsPerfectMatching) (hM1xb : M1.Adj x' b) (hM1nac : ¬M1.Adj a c)
    (hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b),
    let cycles := M1.spanningCoe ∆ M2.spanningCoe;
    ∀ (hcalt : cycles.IsAlternating M2.spanningCoe) (hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles)
      (hcac : cycles.Adj a c) (hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b)
      (induce_le :
        (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
          G ⊔ edge a c ⊔ edge x' b)
      (hxc : x' ∈ (cycles.connectedComponentMk c).supp) (hacc : a ∈ (cycles.connectedComponentMk c).supp)
      (hx' : Membership.mem (γ := Finset V) {x', b} x'_1) (p : cycles.Walk a x'_1) (hp : p.IsPath)
      (hpac : p.toSubgraph.Adj a c) (hnpxb : ¬p.toSubgraph.Adj x' b) (hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c)
      (hadj : p.toSubgraph.Adj c' x') (hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x')
      (hw : ∀ (y : V), (fun (w : V) ↦ M1.Adj x' w) y → y = w), p.toSubgraph.Adj x' b
⊢ p.toSubgraph.Adj x b
have inr : ∀ {M1 : (G ⊔ edge x x').Subgraph} (hab : G.Adj a x') (hnGxb : ¬G.Adj x x') (hnxb : x ≠ x') (hnbc : x' ≠ c)
  (hM1 : M1.IsPerfectMatching) (hM1xb : M1.Adj x x') (hM1nac : ¬M1.Adj a c)
  (hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'),
  let cycles := M1.spanningCoe ∆ M2.spanningCoe;
  ∀ (hcalt : cycles.IsAlternating M2.spanningCoe) (hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles)
    (hcac : cycles.Adj a c) (hM1sub : M1.spanningCoe ≤ G ⊔ edge x x')
    (induce_le :
      (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
        G ⊔ edge a c ⊔ edge x x')
    (hxc : x ∈ (cycles.connectedComponentMk c).supp) (hacc : a ∈ (cycles.connectedComponentMk c).supp)
    (hx' : Membership.mem (γ := Finset V) {x, x'} x'_1) (p : cycles.Walk a x'_1) (hp : p.IsPath)
    (hpac : p.toSubgraph.Adj a c) (hnpxb : ¬p.toSubgraph.Adj x x') (hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c)
    (hadj : p.toSubgraph.Adj c' x') (hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x')
    (hw : ∀ (y : V), (fun (w : V) ↦ M1.Adj x' w) y → y = w), p.toSubgraph.Adj x x'
Tactic: obtain rfl | rfl := hx'
Cleared hypotheses: b, M1, hab, hnGxb, hnxb, hnbc, hM1, hM1xb, hM1nac, hsupG, cycles, hcalt, hcycles, hcac, hM1sub, induce_le, hxc, hacc, hx'_1, p, hp, hpac, hnpxb, hle, hx', hadj, hl, hw