internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
⊢ isMenger G
Tactic:
by_cases h' : Fintype.card G.Dart = 0
Proof state after:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : Fintype.card (Dart G) = 0
⊢ isMenger G

case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ isMenger G
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : Fintype.card (Dart G) = 0
⊢ isMenger G
Tactic:
simp [bot_iff_no_edge.mp h']
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ isMenger G
Tactic:
have h2 : ¬ IsEmpty G.Dart := by simpa [← Fintype.card_eq_zero_iff]
Proof state after:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
⊢ isMenger G
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
⊢ isMenger G
Tactic:
obtain ⟨e⟩ := not_isEmpty_iff.mp h2
Proof state after:
case neg.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
e : Dart G
⊢ isMenger G
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case neg.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
e : Dart G
⊢ isMenger G
Tactic:
refine induction_step e (ih _ contract_edge.fewer_edges rfl) (ih _ (Minus.card_edge e.edge_mem) rfl)
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Menger
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ ¬IsEmpty (Dart G)
Tactic:
simpa [← Fintype.card_eq_zero_iff]
Proof state after:
no goals
Theorem: Measure_theory.L2.integrable_mul
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ ∀ (f g : ↥(Lp ℝ 2)), Integrable fun x => ↑↑f x * ↑↑g x
Tactic:
apply L2.integrable_inner
Proof state after:
no goals
Theorem: Measure_theory.Lp_trim_to_Lp.ae_eq
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
f : ↥(Lp ℝ p)
⊢ ↑↑(Lp_trim_to_Lp p μ hm f) =ᵐ[μ] ↑↑f
Tactic:
apply lpTrimToLpMeas_ae_eq
Proof state after:
no goals
Theorem: Measure_theory.Lp_trim_to_Lp.isometry
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
⊢ Isometry (Lp_trim_to_Lp p μ hm)
Tactic:
rintro f g
Proof state after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ edist (Lp_trim_to_Lp p μ hm f) (Lp_trim_to_Lp p μ hm g) = edist f g
Theorem: Measure_theory.Lp_trim_to_Lp.isometry
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ edist (Lp_trim_to_Lp p μ hm f) (Lp_trim_to_Lp p μ hm g) = edist f g
Tactic:
rw [Lp.edist_def, Lp.edist_def]
Proof state after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p (Measure.trim μ hm)
Theorem: Measure_theory.Lp_trim_to_Lp.isometry
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p (Measure.trim μ hm)
Tactic:
rw [snorm_trim_ae hm ((Lp.aestronglyMeasurable f).sub (Lp.aestronglyMeasurable g))]
Proof state after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p μ
Theorem: Measure_theory.Lp_trim_to_Lp.isometry
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p μ
Tactic:
exact snorm_congr_ae (ae_eq.sub ae_eq)
Proof state after:
no goals
Theorem: Measure_theory.continuous_integral_trim
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => integral μ ↑↑f
Tactic:
simp_rw [← integral_congr_ae Lp_trim_to_Lp.ae_eq]
Proof state after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => ∫ (a : α), ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ
Theorem: Measure_theory.continuous_integral_trim
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => ∫ (a : α), ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ
Tactic:
exact continuous_integral.comp Lp_trim_to_Lp.isometry.continuous
Proof state after:
no goals
Theorem: Measure_theory.continuous_set_integral_trim
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
S : Set α
⊢ Continuous fun f => ∫ (a : α) in S, ↑↑f a ∂μ
Tactic:
simp_rw [← integral_congr_ae Lp_trim_to_Lp.ae_eq.restrict]
Proof state after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
S : Set α
⊢ Continuous fun f => ∫ (a : α) in S, ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ
Theorem: Measure_theory.continuous_set_integral_trim
Proof state before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
S : Set α
⊢ Continuous fun f => ∫ (a : α) in S, ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ
Tactic:
exact (continuous_set_integral S).comp Lp_trim_to_Lp.isometry.continuous
Proof state after:
no goals
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
let φ (f : (G -ₑ e).edgeSet) : G.edgeSet := ⟨f, edgeSet_subset_edgeSet.mpr Minus_le f.2⟩
Proof state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
have φ_inj : Injective φ := by intro e₁ e₂ h ; ext1 ; simpa using h
Proof state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ Fintype.card ↑(edgeSet (G -ₑ e)) < Fintype.card ↑(edgeSet G)
Tactic:
apply Fintype.card_lt_of_injective_of_not_mem (b := ⟨_, h⟩) φ φ_inj
Proof state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := e, property := h } ∉ Set.range φ
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := e, property := h } ∉ Set.range φ
Tactic:
rcases e with ⟨x, y⟩
Proof state after:
case mk.mk
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
x y : V
h : Quot.mk (Sym2.Rel V) (x, y) ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ Quot.mk (Sym2.Rel V) (x, y))) → ↑(edgeSet G) :=
  fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := Quot.mk (Sym2.Rel V) (x, y), property := h } ∉ Set.range φ
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
case mk.mk
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
x y : V
h : Quot.mk (Sym2.Rel V) (x, y) ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ Quot.mk (Sym2.Rel V) (x, y))) → ↑(edgeSet G) :=
  fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
φ_inj : Injective φ
⊢ { val := Quot.mk (Sym2.Rel V) (x, y), property := h } ∉ Set.range φ
Tactic:
simp [Minus]
Proof state after:
no goals
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
⊢ Injective φ
Tactic:
intro e₁ e₂ h
Proof state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ e₁ = e₂
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ e₁ = e₂
Tactic:
ext1
Proof state after:
case a
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ ↑e₁ = ↑e₂
Theorem: SimpleGraph.Minus.card_edge
Proof state before:
case a
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
e : Sym2 V
h✝ : e ∈ edgeSet G
φ : ↑(edgeSet (G -ₑ e)) → ↑(edgeSet G) := fun f => { val := ↑f, property := (_ : ↑f ∈ edgeSet G) }
e₁ e₂ : ↑(edgeSet (G -ₑ e))
h : φ e₁ = φ e₂
⊢ ↑e₁ = ↑e₂
Tactic:
simpa using h
Proof state after:
no goals
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l <+: l'
⊢ init l <+: init l'
Tactic:
have h1 : length l ≤ length l' := List.IsPrefix.length_le h
Proof state after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
⊢ init l <+: init l'
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
⊢ init l <+: init l'
Tactic:
have h2 : length l - 1 ≤ length l' - 1 := Nat.sub_le_sub_right h1 1
Proof state after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
⊢ init l <+: init l'
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
⊢ init l <+: init l'
Tactic:
have h3 : (length l - 1) ≤ (length l') := h2.trans <| Nat.sub_le (length l') 1
Proof state after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Tactic:
rw [List.prefix_iff_eq_take] at h
Proof state after:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Tactic:
rw [h, List.prefix_iff_eq_take]
Proof state after:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init (take (length l) l') = take (length (init (take (length l) l'))) (init l')
Theorem: List.init_prefix
Proof state before:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init (take (length l) l') = take (length (init (take (length l) l'))) (init l')
Tactic:
simp [init, h1, List.take_take, List.take_take, min_eq_left h3, min_eq_left h2]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.init₀_copy
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
h1 : a = c
h2 : b = d
⊢ init₀ (Walk.copy p h1 h2) = init₀ p
Tactic:
subst_vars
Proof state after:
V : Type u_1
V' : Type u_2
c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G c d
⊢ init₀ (Walk.copy p (_ : c = c) (_ : d = d)) = init₀ p
Theorem: SimpleGraph.Walk.init₀_copy
Proof state before:
V : Type u_1
V' : Type u_2
c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G c d
⊢ init₀ (Walk.copy p (_ : c = c) (_ : d = d)) = init₀ p
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail₀_cons
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
e : Adj G c a
⊢ tail₀ (cons e p) = support p
Tactic:
induction p generalizing c with
| nil => rfl
| cons h p ih => simpa [tail₀] using ih (e := h)
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail₀_cons
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b d : V
G G' : SimpleGraph V
f : V → V'
u✝ c : V
e : Adj G c u✝
⊢ tail₀ (cons e nil) = support nil
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail₀_cons
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b d : V
G G' : SimpleGraph V
f : V → V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {c : V} {e : Adj G c v✝}, tail₀ (cons e p) = support p
c : V
e : Adj G c u✝
⊢ tail₀ (cons e (cons h p)) = support (cons h p)
Tactic:
simpa [tail₀] using ih (e := h)
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_init₀_union_last
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ support p = init₀ p ++ [b]
Tactic:
induction p with
| nil => rfl
| cons _ p ih => simp [ih]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_init₀_union_last
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ support nil = init₀ nil ++ [u✝]
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_init₀_union_last
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : support p = init₀ p ++ [w✝]
⊢ support (cons h✝ p) = init₀ (cons h✝ p) ++ [w✝]
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_head_union_tail₀
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ support p = a :: tail₀ p
Tactic:
induction p with
| nil => rfl
| cons _ p ih => simp [ih, Walk.tail₀]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_head_union_tail₀
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ support nil = u✝ :: tail₀ nil
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.support_eq_head_union_tail₀
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : support p = v✝ :: tail₀ p
⊢ support (cons h✝ p) = u✝ :: tail₀ (cons h✝ p)
Tactic:
simp [ih, Walk.tail₀]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail_eq_tail_support
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ tail₀ p = List.tail (support p)
Tactic:
induction p with
| nil => rfl
| cons _ p ih => simp [ih]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail_eq_tail_support
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ tail₀ nil = List.tail (support nil)
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.tail_eq_tail_support
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : tail₀ p = List.tail (support p)
⊢ tail₀ (cons h✝ p) = List.tail (support (cons h✝ p))
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.init_eq_take_support
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ init₀ p = init (support p)
Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp [ih, _root_.List.init]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.init_eq_take_support
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ init₀ nil = init (support nil)
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Walk.init_eq_take_support
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : init₀ p✝ = init (support p✝)
⊢ init₀ (cons h✝ p✝) = init (support (cons h✝ p✝))
Tactic:
simp [ih, _root_.List.init]
Proof state after:
no goals
Theorem: SimpleGraph.Walk.init₀_prefix
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
p' : Walk G a c
h : support p' <+: support p
⊢ init₀ p' <+: init₀ p
Tactic:
simpa [init_eq_take_support] using init_prefix h
Proof state after:
no goals
Theorem: SimpleGraph.support_push_Walk
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
Tactic:
induction p with
| nil => simp [push_Walk]
| cons h p ih =>
  rename_i u v w
  by_cases h : f u = f v <;> simpa [push_Walk, h] using ih.trans <| List.subset_cons _ _
Proof state after:
no goals
Theorem: SimpleGraph.support_push_Walk
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ Walk.support (push_Walk f Walk.nil) ⊆ List.map f (Walk.support Walk.nil)
Tactic:
simp [push_Walk]
Proof state after:
no goals
Theorem: SimpleGraph.support_push_Walk
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))
Tactic:
rename_i u v w
Proof state after:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))
Theorem: SimpleGraph.support_push_Walk
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))
Tactic:
by_cases h : f u = f v <;> simpa [push_Walk, h] using ih.trans <| List.subset_cons _ _
Proof state after:
no goals
Theorem: SimpleGraph.push_append
Proof state before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
q : Walk G b c
⊢ push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
Tactic:
induction p with
| nil => rfl
| cons h p ih =>
  rename_i u v w
  by_cases huv : f u = f v <;> simp [push_Walk, huv, ih q]
  rw [← Walk.append_copy_copy]
  congr
Proof state after:
no goals
Theorem: SimpleGraph.push_append
Proof state before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
q : Walk G u✝ c
⊢ push_Walk f (Walk.append Walk.nil q) = Walk.append (push_Walk f Walk.nil) (push_Walk f q)
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.push_append
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w✝ c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)
Tactic:
rename_i u v w
Proof state after:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)
Theorem: SimpleGraph.push_append
Proof state before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)
Tactic:
by_cases huv : f u = f v <;> simp [push_Walk, huv, ih q]
Proof state after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.copy (Walk.append (push_Walk f p) (push_Walk f q)) (_ : f v = f u) (_ : f c = f c) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)