awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
⊢ G.Colorable (r + 2)
have There₁ : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
  H.Colorable (r + 2)
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
There₁ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    H.Colorable (r + 2)
⊢ G.Colorable (r + 2)
have There₂ : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
  (hnotcol : ¬H.Colorable (r + 2)), False
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
There₁ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    H.Colorable (r + 2)
There₂ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)), False
⊢ G.Colorable (r + 2)
have There₃ : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
  (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite), False
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
There₁ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    H.Colorable (r + 2)
There₂ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)), False
There₃ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite), False
⊢ G.Colorable (r + 2)
have There₄ : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
  (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite) (k : ℕ) (w w_1 w_2 : α) (w_3 w_4 : Finset α)
  (hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4) (hlt : k < r + 1)
  (hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j), False
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
There₁ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    H.Colorable (r + 2)
There₂ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)), False
There₃ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite), False
There₄ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite) (k : ℕ) (w w_1 w_2 : α) (w_3 w_4 : Finset α)
    (hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4) (hlt : k < r + 1)
    (hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j), False
⊢ G.Colorable (r + 2)
have There₅ : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
  (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite) (k : ℕ) (w w_1 w_2 : α) (w_3 w_4 : Finset α)
  (hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4) (hlt : k < r + 1)
  (hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j)
  (hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)), False
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) ↔ ¬G.IsAcyclic
have refine_1 : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) → ¬G.IsAcyclic
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
refine_1 : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) → ¬G.IsAcyclic
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) ↔ ¬G.IsAcyclic
have refine_2 : ∀ (h : ¬G.IsAcyclic), ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)
have refine_2 : ∀ (h : Nonempty.{u_1 + 1} ((i : α) × Subtype (α := G.Walk i i) Walk.IsCycle)),
  ∃ (x : (a : α) × { a_1 : G.Walk a a // a_1.IsCycle }),
    Eq (α := ℕ∞) (↑(↑(x.snd (β := fun (a : α) ↦ { a_1 : G.Walk a a // a_1.IsCycle })) : G.Walk x.fst x.fst).length : ℕ∞)
      (⨅ (x : (i : α) × Subtype (α := G.Walk i i) Walk.IsCycle),
        (↑(↑(x.snd (β := fun (i : α) ↦ Subtype (α := G.Walk i i) Walk.IsCycle)) : G.Walk x.fst x.fst).length : ℕ∞))
Tactic: simp_rw [← egirth_eq_top, ← Ne.eq_def, egirth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top,
      ← exists_prop, Subtype.exists', Sigma.exists', eq_comm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) → ¬G.IsAcyclic
have tauto : ∀ (w : α) (w_1 : G.Walk w w), w_1.IsCycle → G.girth = w_1.length → ¬G.IsAcyclic
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic
have refine : ∀ (h : ¬G.IsAcyclic), ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
Tactic: refine ⟨by tauto, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
have obtain : ∀ (w : α) (w_1 : G.Walk w w),
  w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞) → ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
Tactic: obtain ⟨_, _, _⟩ := exists_egirth_eq_length.mpr h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w : α
w_1 : G.Walk w w
h_1 : w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞)
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
have simp_all : ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
Tactic: simp_all only [girth, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w : α
w_1 : G.Walk w w
h_1 : w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞)
⊢ ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
have tauto : w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w : α
w_1 : G.Walk w w
h_1 : w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
⊢ ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
have h₁ : w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → ∃ (w_2 : G.Walk w w), w_2.IsCycle ∧ w_1.length = w_2.length
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Girth (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w : α
w_1 : G.Walk w w
h_1 : w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
h₁ : w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → ∃ (w_2 : G.Walk w w), w_2.IsCycle ∧ w_1.length = w_2.length
⊢ ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
have w : w_1.IsCycle → G.egirth = (↑w_1.length : ℕ∞) → α
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h :
  if h : v ∈ p then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h) = w
  else if h : w ∈ p then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h) = v else False
⊢ G.Adj v w
have pos : ∀ (h : v ∈ p) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h) = w), G.Adj v w
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h :
  if h : v ∈ p then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h) = w
  else if h : w ∈ p then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h) = v else False
pos : ∀ (h : v ∈ p) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h) = w), G.Adj v w
⊢ G.Adj v w
have pos₁ : v ∉ p → ∀ (h : w ∈ p) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h) = v), G.Adj v w
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
⊢ s.card ≤ Finset.card (α := V) (s.biUnion fun (x : (↑p₁ : Type u_1)) ↦ G.neighborFinset (↑x : V))
have this : (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V).ncard ≤
  Set.ncard.{u_1} (α := V)
    (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)
Tactic: have := h₂ (s.image Subtype.val) (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
this :
  (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V).ncard ≤
    Set.ncard.{u_1} (α := V)
      (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)
⊢ s.card ≤ Finset.card (α := V) (s.biUnion fun (x : (↑p₁ : Type u_1)) ↦ G.neighborFinset (↑x : V))
have this₁ : s.card ≤
  Set.ncard.{u_1} (α := V)
    (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)
Tactic: rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have obtain : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
  ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
Tactic: obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
Tactic: have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have h : p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this sorry) ∧
  Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this sorry)
Tactic: use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
⊢ p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
    Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)
have h : ∀ (v : V) (hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this sorry)),
  ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this sorry) v w
Tactic: refine ⟨by simp, fun v hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v : V
hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)
⊢ ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this ⋯) v w
have hv₁ : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v
Tactic: simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v : V
hv : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v
⊢ ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
have h : ∀ (h' : v ∈ p₁),
  ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
Tactic: rcases hv with h' | ⟨x, hx₁, hx₂⟩
Cleared hypotheses: hv