awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
⊢ G ⊔ edge s t = G
have rwa : edge s t ≤ G
Tactic: rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff,
    mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
rwa : edge s t ≤ G
⊢ G ⊔ edge s t = G
have rwa₁ : (edge s t).edgeSet ⊆ G.edgeSet
Tactic: rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff,
    mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
rwa : edge s t ≤ G
rwa₁ : (edge s t).edgeSet ⊆ G.edgeSet
⊢ G ⊔ edge s t = G
have rwa₂ : {s(s, t)} ⊆ G.edgeSet
Tactic: rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff,
    mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
rwa : edge s t ≤ G
rwa₁ : (edge s t).edgeSet ⊆ G.edgeSet
rwa₂ : {s(s, t)} ⊆ G.edgeSet
⊢ G ⊔ edge s t = G
have rwa₃ : s(s, t) ∈ G.edgeSet
Tactic: rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff,
    mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v
have pos : ∀ (h : u = v), Disjoint G (edge u v) ↔ ¬G.Adj u v
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
pos : ∀ (h : u = v), Disjoint G (edge u v) ↔ ¬G.Adj u v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v
have neg : ∀ (h : ¬u = v), Disjoint G (edge u v) ↔ ¬G.Adj u v
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v
have pos : Disjoint G (edge u u) ↔ ¬G.Adj u u
Tactic: subst h
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
⊢ G.Adj v w
have this : (G ⊔ edge s t).Adj v w
Tactic: have := hvw.adj_sub
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
this : (G ⊔ edge s t).Adj v w
⊢ G.Adj v w
have this₁ : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Tactic: simp only [Subgraph.spanningCoe_adj, SimpleGraph.sup_adj, SimpleGraph.edge_adj] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ G.Adj v w
have pos : ∀ (hs : s(v, w) = s(s, t)), G.Adj v w
Tactic: by_cases hs : s(v, w) = s(s, t)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
pos : ∀ (hs : s(v, w) = s(s, t)), G.Adj v w
⊢ G.Adj v w
have neg : ∀ (hs : ¬s(v, w) = s(s, t)), G.Adj v w
Tactic: by_cases hs : s(v, w) = s(s, t)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯
have rw : (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset
Tactic: rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset
have simp_rw : Set.toFinset {s(s, t)} ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset
Tactic: simp_rw [edgeFinset, edgeSet_edge_of_ne h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1
have rw : #(cons s(s, t) G.edgeFinset sorry) = #G.edgeFinset + 1
Tactic: rw [G.edgeFinset_sup_edge hn h, card_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
rw : #(cons s(s, t) G.edgeFinset ⋯) = #G.edgeFinset + 1
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1
have rw₁ : #G.edgeFinset + 1 = #G.edgeFinset + 1
Tactic: rw [G.edgeFinset_sup_edge hn h, card_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ P.partOfVertex v ∈ P.parts
have h : Exists.choose (p := fun (x : Set V) ↦
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) sorry ∈
  P.parts
Tactic: obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ v ∈ P.partOfVertex v
have right : ∀ (y : Set V),
  (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
    y =
      Exists.choose (p := fun (x : Set V) ↦
        (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) sorry
Tactic: obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
⊢ v ∈ P.partOfVertex v
have left : Exists.choose (p := fun (x : Set V) ↦
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) sorry ∈
  P.parts
Tactic: obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
left :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
⊢ v ∈ P.partOfVertex v
have h : v ∈
  Exists.choose (p := fun (x : Set V) ↦
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) sorry
Tactic: obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ False
have hw : w ∈ P.partOfVertex w
Tactic: have hw := P.mem_partOfVertex w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ False
have hw₁ : w ∈ P.partOfVertex v
Tactic: rw [← hn] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
hvw : G.Adj v w
⊢ Ne.{u + 1} (α := (↑P.parts : Type u))
    ((fun (v : V) ↦ Subtype.mk (p := fun (x : Set V) ↦ x ∈ P.parts) (P.partOfVertex v) ⋯) v)
    ((fun (v : V) ↦ Subtype.mk (p := fun (x : Set V) ↦ x ∈ P.parts) (P.partOfVertex v) ⋯) w)
have rw : ¬P.partOfVertex v = P.partOfVertex w
Tactic: rw [Ne, Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n ↔ G.Colorable n
have mp : G.Partitionable n → G.Colorable n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
mp : G.Partitionable n → G.Colorable n
⊢ G.Partitionable n ↔ G.Colorable n
have mpr : G.Colorable n → G.Partitionable n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset (s := P.parts).card ≤ n
⊢ G.Colorable n
have mp : ∀ (this : Fintype (↑P.parts : Type u)), G.Colorable n
Tactic: have : Fintype P.parts := hf.fintype
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset (s := P.parts).card ≤ n
this : Fintype (↑P.parts : Type u)
⊢ G.Colorable n
have hc₁ : Fintype.card.{u} (↑P.parts : Type u) ≤ n
Tactic: rw [Set.Finite.card_toFinset hf] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ G.Partitionable n
have mpr : sorry.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
Tactic: refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ ⋯.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
have h : C.toPartition.parts.Finite
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
have h₁ : C.colorClasses.Finite
Tactic: change Set.Finite (Coloring.colorClasses C) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
⊢ h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
have mpr : ∀ (this : Fintype (↑C.colorClasses : Type u)), h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
Tactic: have : Fintype C.colorClasses := C.colorClasses_finite.fintype
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Partition (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype (↑C.colorClasses : Type u)
⊢ h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
have mpr : Fintype.card.{u} (↑C.colorClasses : Type u) ≤ Fintype.card (Fin n)
Tactic: rw [h.card_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ (G □ H).neighborSet x =
    SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)
have h : ∀ (a' : α) (b' : β),
  (a', b') ∈ (G □ H).neighborSet x ↔
    (a', b') ∈ SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)
Tactic: ext ⟨a', b'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ (a', b') ∈ (G □ H).neighborSet x ↔
    (a', b') ∈ SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)
have h : G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'
Tactic: simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w
have rw : cons sorry (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w
Tactic: rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
rw : cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w
⊢ (Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w
have hc : G.Adj (x, b).1 (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).1 ∧
  (x, b).2 = (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).2
Tactic: rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w
have rw : cons sorry (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w
Tactic: rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
rw : cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w
have hc : G.Adj (a, x).2 (((G.boxProdRight G a).toHom : (a : α) → α × α) y).2 ∧
  (a, x).1 = (((G.boxProdRight G a).toHom : (a : α) → α × α) y).1
Tactic: rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ (cons x w').length =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
have rw : w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
  length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
      (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons sorry w'.ofBoxProdLeft)
        fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
        Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft sorry) +
    length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
      (sorry.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons sorry w'.ofBoxProdRight)
        fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
        Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight sorry)
Tactic: rw [length_cons, length_boxProd w']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
have disj : G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1
Tactic: have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
disj : G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
have inl : ∀ (h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2),
  w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons sorry w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft sorry) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (sorry.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons sorry w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight sorry)
Tactic: rcases disj with h₁ | h₂
Cleared hypotheses: disj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
disj : G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1
inl :
  ∀ (h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2),
    w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
      length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
          (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
            fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
            Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
        length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
          (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
            fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
            Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
have inr : ∀ (h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1),
  w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons sorry w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft sorry) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (sorry.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons sorry w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight sorry)
Tactic: rcases disj with h₁ | h₂
Cleared hypotheses: disj