awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜 ∨ u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ht : s ∩ u ⊆ s
inl : ∀ (hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have inr : ∀ (hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: obtain hu | hu := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos : ∀ (ha : a ∈ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
pos : ∀ (ha : a ∈ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have neg : ∀ (ha : a ∉ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos : ∀ (v : Finset α) (hv : v ∈ 𝓓 a 𝒜) (hsv : s ∩ v = insert a (s ∩ u)), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝓓 a 𝒜
hsv : s ∩ v = insert a (s ∩ u)
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have hv₁ : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
Tactic: rw [Down.mem_compression] at hv
Cleared hypotheses: hv, hsv
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
hsv : s ∩ v = insert a (s ∩ u)
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos : ∀ (hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: obtain hv | hv := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
hsv : s ∩ v = insert a (s ∩ u)
pos : ∀ (hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos₁ : ∀ (hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: obtain hv | hv := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos : s ∩ v.erase a = s ∩ u
Tactic: refine ⟨erase v a, hv.2, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ s ∩ v.erase a = s ∩ u
have pos : a ∉ s ∩ u
Tactic: rw [inter_erase, hsv, erase_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha_1 : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
ha : a ∈ s ∩ u
⊢ False
have pos : ∀ (hu : u ∉ 𝒜 ∧ u ∈ 𝒜) (ha : a ∈ s) (v : Finset α) (hsv : s ∩ v = insert a (s ∩ u)) (hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜)
  (ha : a ∈ s ∩ u), False
Tactic: rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
Cleared hypotheses: hu, ha_1, v, hsv, hv, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have pos : ∀ (hv : v ∉ 𝒜 ∧ v ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Tactic: rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
pos : ∀ (hv : v ∉ 𝒜 ∧ v ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have rw : a ∈ s ∩ v
Tactic: rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ a ∈ s ∩ v
have rw : a ∈ insert a (s ∩ u)
Tactic: rw [hsv]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
have neg : s ∩ insert a u = s ∩ u
Tactic: refine ⟨insert a u, hu.2, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ s ∩ insert a u = s ∩ u
have neg : s ∩ u = s ∩ u
Tactic: rw [inter_insert_of_notMem ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer
have simp : ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x
Tactic: simp only [subset_iff, mem_shatterer]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k
have simp_rw : #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, card.{u_1} (α := Finset α) (powersetCard x univ)
Tactic: simp_rw [← card_univ, ← card_powersetCard]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, card.{u_1} (α := Finset α) (powersetCard x univ)
have refine : ∀ (s : Finset α) (hs : s ∈ 𝒜.shatterer),
  #s ∈ Iic 𝒜.vcDim ∧ Membership.mem (γ := Finset (Finset α)) (powersetCard (#s) univ) s
Tactic: refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet
have cons : ∀ (H₁ : SimpleGraph V) (hH₁ : H₁ ∈ Hs) (ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet),
  ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet
Tactic: obtain ⟨H₁, hH₁, ih⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet
have cons : ∀ (H₂ : SimpleGraph V) (hH₂ : H₂ ∈ Hs) (h_adj : H₂.Adj u v), ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (cons sorry p), e ∈ H.edgeSet
Tactic: obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
Cleared hypotheses: h_adj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
H₂ : SimpleGraph V
hH₂ : H₂ ∈ Hs
h_adj : H₂.Adj u v
⊢ ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (cons ⋯ p), e ∈ H.edgeSet
have cons : ∀ (H : SimpleGraph V) (hH : H ∈ Hs) (h₁ : H₁ ≤ H) (h₂ : H₂ ≤ H),
  ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (cons sorry p), e ∈ H.edgeSet
Tactic: obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u v : V
p : (sSup Hs).Walk u v
⊢ ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
have nil : ∀ {u : V},
  ∃ H ∈ Hs, ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := sSup Hs) (u := u) nil) e → e ∈ H.edgeSet
Tactic: induction p with
  | nil => exact ⟨hHs.some, hHs.some_mem, by simp⟩
  | @cons u v w h_adj p ih =>
    obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u v : V
p : (sSup Hs).Walk u v
nil :
  ∀ {u : V},
    ∃ H ∈ Hs,
      ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := sSup Hs) (u := u) Walk.nil) e → e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
have cons : ∀ {u v w : V} (h_adj : (sSup Hs).Adj u v) (p : (sSup Hs).Walk v w) (ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet),
  ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet
Tactic: induction p with
  | nil => exact ⟨hHs.some, hHs.some_mem, by simp⟩
  | @cons u v w h_adj p ih =>
    obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
⊢ (sSup Hs).IsAcyclic
have inl : ∀ (h_acyc : ∀ (H : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) ∅ H → H.IsAcyclic)
  (h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) ∅), IsAcyclic.{u_1} (V := V) (sSup ∅)
Tactic: rcases Hs.eq_empty_or_nonempty with rfl | hnemp
Cleared hypotheses: Hs, h_acyc, h_dir
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
inl :
  ∀ (h_acyc : ∀ (H : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) ∅ H → H.IsAcyclic)
    (h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) ∅), IsAcyclic.{u_1} (V := V) (sSup ∅)
⊢ (sSup Hs).IsAcyclic
have inr : ∀ (hnemp : Hs.Nonempty), (sSup Hs).IsAcyclic
Tactic: rcases Hs.eq_empty_or_nonempty with rfl | hnemp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
⊢ False
have inr : ∀ (H : SimpleGraph V) (hH : H ∈ Hs) (hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet), False
Tactic: obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
⊢ ∃ (H' : SimpleGraph V), H ≤ H' ∧ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) H'
have refine : ∀ (c : Set (SimpleGraph V)) (hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic})
  (hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c) (y : SimpleGraph V) (hy : y ∈ c),
  ∃ (ub : SimpleGraph V),
    Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: refine zorn_le_nonempty₀ {H | H ≤ G ∧ H.IsAcyclic} (fun c hcs hc y hy ↦ ?_) _ ⟨hHG, hH⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ ∃ (ub : SimpleGraph V),
    Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1 : sSup c ≤ G
Tactic: refine ⟨sSup c, ⟨?_, ?_⟩, fun _ ↦ le_sSup⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
refine_1 : sSup c ≤ G
⊢ ∃ (ub : SimpleGraph V),
    Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_2 : (sSup c).IsAcyclic
Tactic: refine ⟨sSup c, ⟨?_, ?_⟩, fun _ ↦ le_sSup⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ False
have this : 3 ≤ p.length
Tactic: have := hp.three_le_length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this : 3 ≤ p.length
⊢ False
have this₁ : p.support.tail.length ≤ 2
Tactic: have := Nat.cast_le.mp <| hp.support_nodup.length_le_enatCard.trans h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this_1 : 3 ≤ p.length
this : p.support.tail.length ≤ 2
⊢ False
have this₁ : p.length + 1 - 1 ≤ 2
Tactic: rw [List.length_tail, p.length_support] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).coe.IsTree
have refine : ∀ (w : (↑(G.subgraphOfAdj h).verts : Type u_1)) (p : (G.subgraphOfAdj h).coe.Walk w w) (hp : p.IsCycle), False
Tactic: refine ⟨Subgraph.subgraphOfAdj_connected h, fun w p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
⊢ False
have this : s(u, v) = s((↑w : V), (↑p.snd : V))
Tactic: have : _ = _ := p.adj_snd hp.not_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this : s(u, v) = s((↑w : V), (↑p.snd : V))
⊢ False
have this₁ : s(u, v) = s((↑p.penultimate : V), (↑w : V))
Tactic: have : _ = _ := p.adj_penultimate hp.not_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
⊢ False
have hp₁ : p.IsCycle
Tactic: simp_all
Cleared hypotheses: hp, this_1, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
hp₁ : p.IsCycle
⊢ False
have this₁ : (↑p.penultimate : V) = (↑w : V) ∧ (↑w : V) = (↑p.snd : V) ∨ (↑p.penultimate : V) = (↑p.snd : V)
Tactic: simp_all
Cleared hypotheses: hp, this_1, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
hp₁ : p.IsCycle
this₁ : (↑p.penultimate : V) = (↑w : V) ∧ (↑w : V) = (↑p.snd : V) ∨ (↑p.penultimate : V) = (↑p.snd : V)
⊢ False
have this₂ : u = (↑p.penultimate : V) ∧ v = (↑w : V) ∨ u = (↑w : V) ∧ v = (↑p.penultimate : V)
Tactic: simp_all
Cleared hypotheses: hp, this_1, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
have simp_rw : G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
Tactic: simp_rw [isBridge_iff_adj_and_forall_cycle_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
have mp : G.IsAcyclic → ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
mp : G.IsAcyclic → ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
have mpr : (∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges) → G.IsAcyclic
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
⊢ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
have mp : ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
Tactic: apply And.intro hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v_1 : V
ha : G.Adj v v_1
p : G.Walk v_1 v
hp : (cons ha p).IsCycle
⊢ False
have mpr : s(v, v_1) ∈ (cons ha p).edges
Tactic: apply (hb ha).2 _ hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v_1 : V
ha : G.Adj v v_1
p : G.Walk v_1 v
hp : (cons ha p).IsCycle
⊢ s(v, v_1) ∈ (cons ha p).edges
have mpr : s(v, v_1) ∈ s(v, v_1) :: p.edges
Tactic: rw [Walk.edges_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p q : G.Path v w
⊢ p = q
have obtain : ∀ (p : G.Walk v w) (hp : p.IsPath), Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
Tactic: obtain ⟨p, hp⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
q : G.Path v w
p : G.Walk v w
hp : p.IsPath
⊢ Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
have obtain : ∀ (q : G.Walk v w) (hq : q.IsPath),
  Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) q hq
Tactic: obtain ⟨q, hq⟩ := q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
⊢ Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) q hq
have rw : p = q
Tactic: rw [Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w u : V
hp : IsPath.{u_1} (V := V) (G := G) (u := u) nil
q : G.Walk u u
hq : q.IsPath
⊢ nil = q
have nil : ∀ (hq : IsPath.{u_1} (V := V) (G := G) (u := u) nil), Eq.{u_1 + 1} (α := G.Walk u u) nil nil
Tactic: cases (Walk.isPath_iff_eq_nil _).mp hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
⊢ cons ph p = q
have cons : ∀ (h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)) {v w u v w : V} (ph : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ (hp : p.IsPath) (q : G.Walk v w) (hq : q.IsPath), p = q) (hp : (cons ph p).IsPath) (q : G.Walk u w)
  (hq : q.IsPath), cons ph p = q
Tactic: rw [isAcyclic_iff_forall_adj_isBridge] at h
Cleared hypotheses: h, v, w, u, v_1, w_1, ph, p, ih, hp, q, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
⊢ cons ph p = q
have h₁ : G.IsBridge s(u, v_1)
Tactic: specialize h ph
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : G.IsBridge s(u, v_1)
⊢ cons ph p = q
have h₁ : G.Adj u v_1 ∧ ∀ (p : G.Walk u v_1), s(u, v_1) ∈ p.edges
Tactic: rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : G.Adj u v_1 ∧ ∀ (p : G.Walk u v_1), s(u, v_1) ∈ p.edges
⊢ cons ph p = q
have h₁ : s(u, v_1) ∈ (q.append p.reverse).edges
Tactic: replace h := h.2 (q.append p.reverse)
Cleared hypotheses: h