awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : (cons h p_1).IsPath
⊢ (Walk.map f (cons h p_1)).IsPath
have hp₁ : p_1.IsPath ∧ u_1 ∉ p_1.support
Tactic: rw [Walk.cons_isPath_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
⊢ (Walk.map f (cons h p_1)).IsPath
have cons : ∀ x ∈ p_1.support, ¬Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
Tactic: simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
      true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
x : V
hx : x ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
⊢ False
have hx₁ : u_1 ∈ p_1.support
Tactic: cases hinj hf
Cleared hypotheses: x, hx, hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
x : V
hx : x ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
hx₁ : u_1 ∈ p_1.support
⊢ False
have hf₁ : Eq.{v + 1} (α := V') ((f : (a : V) → V') u_1 : V') ((f : (a : V) → V') u_1 : V')
Tactic: cases hinj hf
Cleared hypotheses: x, hx, hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
hp : p.IsPath
⊢ (Walk.map f p).IsPath
have nil : ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) nil), IsPath (u := (f : (a : V) → V') u) (Walk.map f nil)
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [Walk.cons_isPath_iff] at hp
    simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
      true_and]
    intro x hx hf
    cases hinj hf
    exact hp.2 hx
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
hp : p.IsPath
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil),
    IsPath (u := (f : (a : V) → V') u) (Walk.map f Walk.nil)
⊢ (Walk.map f p).IsPath
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (hp : p.IsPath), (Walk.map f p).IsPath) (hp : (cons h p).IsPath),
  (Walk.map f (cons h p)).IsPath
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [Walk.cons_isPath_iff] at hp
    simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
      true_and]
    intro x hx hf
    cases hinj hf
    exact hp.2 hx
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f : G →g G'
hp : (Walk.map f p).IsPath
⊢ p.IsPath
have nil : ∀ {u : V} (hp : IsPath (u := (f : (a : V) → V') u) (Walk.map f Walk.nil)),
  IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
Tactic: induction p with
  | nil => simp
  | cons _ _ ih => grind [map_cons, Walk.cons_isPath_iff, support_map]
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f : G →g G'
hp : (Walk.map f p).IsPath
nil :
  ∀ {u : V} (hp : IsPath (u := (f : (a : V) → V') u) (Walk.map f Walk.nil)),
    IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ p.IsPath
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (hp : (Walk.map f p).IsPath), p.IsPath)
  (hp : (Walk.map f (cons h p)).IsPath), (cons h p).IsPath
Tactic: induction p with
  | nil => simp
  | cons _ _ ih => grind [map_cons, Walk.cons_isPath_iff, support_map]
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
⊢ (Walk.map f (cons h p_1)).IsTrail ↔ (cons h p_1).IsTrail
have cons : p_1.IsTrail ∧ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔
  p_1.IsTrail ∧ s(u_1, v_1) ∉ p_1.edges
Tactic: rw [map_cons, isTrail_cons, ih, isTrail_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
⊢ p_1.IsTrail ∧ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔
    p_1.IsTrail ∧ s(u_1, v_1) ∉ p_1.edges
have cons : (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
Tactic: apply and_congr_right'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
⊢ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
have cons : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
Tactic: rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
cons : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
⊢ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
have cons₁ : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges ↔ s(u_1, v_1) ∉ p_1.edges
Tactic: rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
cons : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
cons₁ :
  Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges ↔ s(u_1, v_1) ∉ p_1.edges
⊢ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
have cons₂ : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges ↔
  Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges
Tactic: rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
⊢ (Walk.map f p).IsTrail ↔ p.IsTrail
have nil : ∀ {u : V}, IsTrail (u := (f : (a : V) → V') u) (Walk.map f nil) ↔ IsTrail.{u} (V := V) (G := G) (u := u) nil
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [map_cons, isTrail_cons, ih, isTrail_cons]
    apply and_congr_right'
    rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
nil :
  ∀ {u : V}, IsTrail (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) ↔ IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ (Walk.map f p).IsTrail ↔ p.IsTrail
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : (Walk.map f p).IsTrail ↔ p.IsTrail),
  (Walk.map f (cons h p)).IsTrail ↔ (cons h p).IsTrail
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [map_cons, isTrail_cons, ih, isTrail_cons]
    apply and_congr_right'
    rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₁ : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
  p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₇ : p.IsTrail ∧ ¬p.Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₇ : p.IsTrail ∧ ¬p.Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₈ : p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.tail (List.map (⇑f : (a : V) → V') p.support)) ↔
  p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₇ : p.IsTrail ∧ ¬p.Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₈ :
  p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.tail (List.map (⇑f : (a : V) → V') p.support)) ↔
    p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₉ : p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.map (⇑f : (a : V) → V') p.support.tail) ↔
  p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₇ : p.IsTrail ∧ ¬p.Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₈ :
  p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.tail (List.map (⇑f : (a : V) → V') p.support)) ↔
    p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₉ :
  p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.map (⇑f : (a : V) → V') p.support.tail) ↔
    p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle
have rw₁₀ : p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Tactic: rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h :
  Path.map f hinj (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p hp) =
    Path.map f hinj (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p' hp')
⊢ Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p' hp'
have h₁ : Walk.map f p = Walk.map f p'
Tactic: simp only [Path.map, Subtype.mk.injEq] at h
Cleared hypotheses: h