awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
pos : ∀ (huv : u = v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have neg : ∀ (huv : ¬u = v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Tactic: by_cases huv : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have pos : ∀ (hadj : G.Adj u v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Tactic: by_cases hadj : G.Adj u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
pos : ∀ (hadj : G.Adj u v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have neg : ∀ (hadj : ¬G.Adj u v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Tactic: by_cases hadj : G.Adj u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have neg : (G ⊔ edge u v).IsAcyclic → G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Tactic: refine ⟨?_, fun ⟨hacyc, hreach⟩ ↦ hacyc.sup_edge_of_not_reachable <| by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
⊢ (G ⊔ edge u v).IsAcyclic → G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have neg : ∀ (hacyc : (G ⊔ edge u v).IsAcyclic) (hreach : G.Reachable u v), False
Tactic: refine fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ False
have neg : ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
Tactic: refine (isAcyclic_iff_forall_edge_isBridge.mp (e := s(u, v)) hacyc <| by simp [huv]).right ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
have h : (G ⊔ edge u v).deleteEdges {s(u, v)} = G
Tactic: convert! hreach
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
⊢ F.Reachable = G.Reachable
have h₁ : ∀ (u v : V), F.Reachable u v ↔ G.Reachable u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
⊢ F.Reachable u v ↔ G.Reachable u v
have h₁ : G.Reachable u v → ∀ (p : G.Walk u v), F.Reachable u v
Tactic: refine ⟨.mono h.prop.left, fun ⟨p⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
⊢ F.Reachable u v
have h₁ : ∀ (this : ¬F.Reachable u v), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
⊢ False
have this₁ : v ∉ s
Tactic: have : v ∉ s := this ∘ s.reachable_of_mem_supp rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this_1 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this : v ∉ s
⊢ False
have this₁ : ∃ d ∈ p.darts, d.toProd.1 ∈ s ∧ d.toProd.2 ∉ s
Tactic: have : ∃ d ∈ p.darts, d.fst ∈ s ∧ d.snd ∉ s := p.exists_boundary_dart s rfl this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this_1 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this_2 : v ∉ s
this : ∃ d ∈ p.darts, d.toProd.1 ∈ s ∧ d.toProd.2 ∉ s
⊢ False
have h₁ : ∀ (u' v' : V) (huv : G.Adj (u', v').1 (u', v').2),
  { fst := u', snd := v', adj := huv : G.Dart } ∈ p.darts →
    ∀ (hu : { fst := u', snd := v', adj := huv : G.Dart }.toProd.1 ∈ s)
      (hv : { fst := u', snd := v', adj := huv : G.Dart }.toProd.2 ∉ s), False
Tactic: rcases this with ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this_1 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left : { fst := u', snd := v', adj := huv : G.Dart } ∈ p.darts
hu : { fst := u', snd := v', adj := huv : G.Dart }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv : G.Dart }.toProd.2 ∉ s
⊢ False
have this₁ : ¬F.Reachable v' u'
Tactic: have : ¬F.Reachable v' u' := mt ConnectedComponent.sound <| s.mem_supp_iff u' |>.mp hu ▸ hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this_1 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this_2 : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left : { fst := u', snd := v', adj := huv : G.Dart } ∈ p.darts
hu : { fst := u', snd := v', adj := huv : G.Dart }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv : G.Dart }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ False
have h₁ : F ⊔ edge v' u' ≤ F
Tactic: suffices F ⊔ edge v' u' ≤ F by
    grind [Adj.reachable, sup_le_iff, le_iff_adj, edge_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
h_1 : G.Reachable u v
p : G.Walk u v
this_1 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this_2 : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left : { fst := u', snd := v', adj := huv : G.Dart } ∈ p.darts
hu : { fst := u', snd := v', adj := huv : G.Dart }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv : G.Dart }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ F ⊔ edge v' u' ≤ F
have h₁ : F ⊔ edge v' u' ≤ G
Tactic: refine h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
⊢ Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F ↔ F.Reachable = G.Reachable
have refine : ∀ (h : F.Reachable = G.Reachable), Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
Tactic: refine ⟨reachable_eq_of_maximal_isAcyclic F, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
⊢ Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
have by_contra : ∀ (this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
⊢ False
have have : ∀ (H : SimpleGraph V) (hFH : F < H) (hHG : H ≤ G) (hH : H.IsAcyclic), False
Tactic: have ⟨H, hFH, hHG, hH⟩ := exists_gt_of_not_maximal ⟨hle, hF⟩ this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
⊢ False
have have : ∀ (e : Sym2 V) (heH : e ∈ H.edgeSet) (heF : e ∉ F.edgeSet), False
Tactic: have ⟨e, heH, heF⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hFH
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ (F ⊔ fromEdgeSet {e}).IsBridge e
have refine : (F ⊔ fromEdgeSet {e}).IsAcyclic
Tactic: refine isAcyclic_iff_forall_edge_isBridge.mp ?_ <| by simp [H.not_isDiag_of_mem_edgeSet heH]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ False
have h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e
Tactic: have h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e := by
    refine isAcyclic_iff_forall_edge_isBridge.mp ?_ <| by simp [H.not_isDiag_of_mem_edgeSet heH]
    exact hH.anti <| sup_le_iff.mpr ⟨hFH.le, H.fromEdgeSet_le.mpr <| by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e
⊢ False
have this₁ : (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F
Tactic: have : (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F := by simpa using heF
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this_1 : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e
this : (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F
⊢ False
have h₁ : ∀ (x y : V) (heH : s(x, y) ∈ H.edgeSet) (heF : s(x, y) ∉ F.edgeSet)
  (h_bridge : (F ⊔ fromEdgeSet {s(x, y)}).IsBridge s(x, y))
  (this : (F ⊔ fromEdgeSet {s(x, y)}).deleteEdges {s(x, y)} = F), False
Tactic: cases e
Cleared hypotheses: e, heH, heF, h_bridge, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this_1 : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
x y : V
heH : s(x, y) ∈ H.edgeSet
heF : s(x, y) ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {s(x, y)}).IsBridge s(x, y)
this : (F ⊔ fromEdgeSet {s(x, y)}).deleteEdges {s(x, y)} = F
⊢ False
have h_bridge₁ : (F ⊔ fromEdgeSet {s(x, y)}).Adj x y ∧ ¬G.Reachable x y
Tactic: rw [isBridge_iff, this, h] at h_bridge
Cleared hypotheses: h_bridge, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree
have this : Nonempty V
Tactic: have := hG.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree
have refine_1 : ∀ (h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T) (u v : V), T.Reachable u v
Tactic: refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
refine_1 : ∀ (h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T) (u v : V), T.Reachable u v
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree
have refine_2 : ∀ (hT' : T.IsTree), Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
Tactic: refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
have refine_2 : T.Reachable = G.Reachable
Tactic: rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
refine_2 : T.Reachable = G.Reachable
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
have refine_2₁ : ⊤ = G.Reachable
Tactic: rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
refine_2 : T.Reachable = G.Reachable
refine_2₁ : ⊤ = G.Reachable
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
have refine_2₂ : Eq.{u_1 + 1} (α := (u v : V) → Prop) ⊤ ⊤
Tactic: rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G
have refine : ∀ (h : G.IsTree), Nonempty V ∧ Maximal IsAcyclic G
Tactic: refine ⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
⊢ Nonempty V ∧ Maximal IsAcyclic G
have this : Nonempty V
Tactic: have := h.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
have obtain : ∀ (F : SimpleGraph V) (hF : H ≤ F ∧ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) F),
  ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
Tactic: obtain ⟨F, hF⟩ := G.exists_maximal_isAcyclic_of_le_isAcyclic hH_le hH_isAcyclic
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable
have obtain : ∀ (F : SimpleGraph V) (hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable),
  ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable
Tactic: obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree
have obtain : ∀ (F : SimpleGraph V) (hF : H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable),
  ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree
Tactic: obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic hH_le hH_isAcyclic
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
⊢ ∃ T ≤ G, T.IsTree
have obtain : ∀ (F : SimpleGraph V) (hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable), ∃ T ≤ G, T.IsTree
Tactic: obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
have inl : ∀ (hV : Infinite V), Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
Tactic: obtain hV | hV := (finite_or_infinite V).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
inl : ∀ (hV : Infinite V), Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
have inr : ∀ (hV : Finite V), Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
Tactic: obtain hV | hV := (finite_or_infinite V).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
have inr : ∀ (this : (α : Type u_1) → [Finite α] → Fintype α), Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
Tactic: have := Fintype.ofFinite
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
have inr : ∀ (T : SimpleGraph V) (hle : T ≤ G) (hT : T.IsTree), Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
Tactic: obtain ⟨T, hle, hT⟩ := h.exists_isTree_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1
have inr : T.edgeFinset.card ≤ G.edgeFinset.card
Tactic: rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, add_le_add_iff_right,
    Nat.card_eq_fintype_card, ← edgeFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have have : ∀ (this : Fintype V), G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
Tactic: have := Fintype.ofFinite V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have refine : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
  ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V), G.IsAcyclic
Tactic: refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
⊢ G.IsAcyclic
have simp_rw : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
Tactic: simp_rw [isAcyclic_iff_forall_adj_isBridge]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
have refine : ∀ (x y : V) (h : G.Adj x y) (hbr : ¬G.IsBridge s(x, y)),
  Nat.card.{u_1} (↑(G.deleteEdges {s(x, y)}).edgeSet : Type u_1) + 1 < Nat.card V
Tactic: refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h_1 : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ Nat.card.{u_1} (↑(G.deleteEdges {s(x, y)}).edgeSet : Type u_1) + 1 < Nat.card V
have rw : (G.deleteEdges {s(x, y)}).edgeFinset.card < G.edgeFinset.card
Tactic: rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have refine : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
  ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V), G.IsAcyclic
Tactic: classical
  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
  rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
refine :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V), G.IsAcyclic
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have refine₁ : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
  ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) ⦃v w : V⦄,
    G.Adj v w → G.IsBridge s(v, w)
Tactic: classical
  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
  rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]