awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg : ∀ (wG : G.Walk x.1 y.1) (hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg : ∀ (wH : H.Walk x.2 y.2) (hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
⊢ w_app.length = wG.length + wH.length
have unfold : ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
  wG.length + wH.length
Tactic: unfold w_app Walk.boxProdLeft Walk.boxProdRight
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have w_len : w_app.length = wG.length + wH.length
Tactic: have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg : (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
neg : (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg₁ : G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
have calc : (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)
Tactic: calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
calc : (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)
⊢ (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
have calc₁ : (↑w_app.length : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞)
Tactic: calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
calc : (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)
calc₁ : (↑w_app.length : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞)
⊢ (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
have calc₂ : HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞) = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
have neg : ∀ (w : (G □ H).Walk x y) (hw : (↑w.length : ℕ∞) = (G □ H).edist x y),
  G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
Tactic: have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : (↑w.length : ℕ∞) = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
have neg : G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (↑(w.ofBoxProdLeft.length + w.ofBoxProdRight.length) : ℕ∞)
Tactic: rw [← hw, Walk.length_boxProd]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have The : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
Tactic: classical
  -- The case `(G □ H).edist x y = ⊤` is used twice, so better to factor it out.
  have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
  by_cases h : (G □ H).edist x y = ⊤
  · rw [top_case] at h
    aesop
  · have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
    have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
    have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
    let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)
    have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
    refine le_antisymm ?_ ?_
    · calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
    · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
The : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have The₁ : ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: classical
  -- The case `(G □ H).edist x y = ⊤` is used twice, so better to factor it out.
  have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
  by_cases h : (G □ H).edist x y = ⊤
  · rw [top_case] at h
    aesop
  · have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
    have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
    have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
    let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)
    have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
    refine le_antisymm ?_ ?_
    · calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
    · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
The : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₁ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
The₂ : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₃ The₄ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have pos : ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤) (h : (G □ H).edist x y = ⊤),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: classical
  -- The case `(G □ H).edist x y = ⊤` is used twice, so better to factor it out.
  have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
  by_cases h : (G □ H).edist x y = ⊤
  · rw [top_case] at h
    aesop
  · have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
    have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
    have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
    let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)
    have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
    refine le_antisymm ?_ ?_
    · calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
    · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
The : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₁ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
The₂ : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₃ The₄ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
pos :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤) (h : (G □ H).edist x y = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg : ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤) (h : ¬(G □ H).edist x y = ⊤),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Tactic: classical
  -- The case `(G □ H).edist x y = ⊤` is used twice, so better to factor it out.
  have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
  by_cases h : (G □ H).edist x y = ⊤
  · rw [top_case] at h
    aesop
  · have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
    have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
    have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
    let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)
    have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
    refine le_antisymm ?_ ?_
    · calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
    · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
x x_1 : ℕ
h : x ≤ x_1
⊢ x * HPow.hPow (α := ℕ) 4 x ≤ x_1 * HPow.hPow (α := ℕ) 4 x_1
have h₂ : LE.le (α := ℕ) 1 4
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ (↑(n * HPow.hPow (α := ℕ) 4 n) : α) = (↑n : α) * HPow.hPow (α := α) 4 n
have norm_cast : Eq.{u_1 + 1} (α := α) (↑(n * HPow.hPow (α := ℕ) 4 n) : α) (↑(n * HPow.hPow (α := ℕ) 4 n) : α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts
have bc : LE.le (α := ℕ) 4 16
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ 0 < m
have sz_positivity : 0 < m → 0 < m
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ HPow.hPow (α := ℝ) 4 #P.parts ≤ (↑m : ℝ)
have norm_cast : HPow.hPow (α := ℕ) 4 #P.parts ≤ m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ HPow.hPow (α := ℕ) 4 #P.parts ≤ m
have rwa : HPow.hPow (α := ℕ) 4 #P.parts * stepBound #P.parts ≤ Fintype.card α
Tactic: rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
rwa : HPow.hPow (α := ℕ) 4 #P.parts * stepBound #P.parts ≤ Fintype.card α
⊢ HPow.hPow (α := ℕ) 4 #P.parts ≤ m
have rwa₁ : HPow.hPow (α := ℕ) 4 #P.parts * (#P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
Tactic: rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
rwa : HPow.hPow (α := ℕ) 4 #P.parts * stepBound #P.parts ≤ Fintype.card α
rwa₁ : HPow.hPow (α := ℕ) 4 #P.parts * (#P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
⊢ HPow.hPow (α := ℕ) 4 #P.parts ≤ m
have rwa₂ : #P.parts * (HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
Tactic: rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
rwa : HPow.hPow (α := ℕ) 4 #P.parts * stepBound #P.parts ≤ Fintype.card α
rwa₁ : HPow.hPow (α := ℕ) 4 #P.parts * (#P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
rwa₂ : #P.parts * (HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
⊢ HPow.hPow (α := ℕ) 4 #P.parts ≤ m
have rwa₃ : #P.parts * HMul.hMul (α := ℕ) 4 4 ^ #P.parts ≤ Fintype.card α
Tactic: rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε : ε ≤ 1
⊢ 0 < HPow.hPow (β := ℕ) ε 5
have sz_positivity : 0 < m → 0 < HPow.hPow (β := ℕ) ε 5
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε : ε ≤ 1
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 < HPow.hPow (β := ℕ) ε 5
⊢ 0 < HPow.hPow (β := ℕ) ε 5
have sz_positivity₄ : 0 < m → 0 < ε → 0 < HPow.hPow (β := ℕ) ε 5
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε : ε ≤ 1
⊢ 0 ≤ ε
have sz_positivity : 0 < m → 0 ≤ ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε : ε ≤ 1
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ ε
⊢ 0 ≤ ε
have sz_positivity₄ : 0 < m → 0 < ε → 0 ≤ ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
⊢ a + 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
have h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
Tactic: have h : 1 ≤ 4 ^ #P.parts := one_le_pow₀ (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
⊢ a + 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
have rw : Fintype.card α / #P.parts - Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
    1 ≤
  HPow.hPow (α := ℕ) 4 #P.parts
Tactic: rw [stepBound, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
| HPow.hPow (α := ℕ) 4 #P.parts
have rw : HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1
Tactic: rw [← Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
⊢ Fintype.card α / #P.parts -
        Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts
have conv_rhs : Fintype.card α / #P.parts - Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
    1 ≤
  HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1
Tactic: conv_rhs => rw [← Nat.sub_add_cancel h]