awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

Tactic:
h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left

Premises used: Maximal.le_of_ge, le_sup_left, Maximal.prop, And.right, And.intro, SimpleGraph.IsAcyclic.sup_edge_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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'
h₁ : F ⊔ edge v' u' ≤ G
⊢ F ⊔ edge v' u' ≤ F

Tactic:
refine h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left

Premises used: Maximal.le_of_ge, le_sup_left, Maximal.prop, And.right, And.intro, SimpleGraph.IsAcyclic.sup_edge_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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' ≤ G

Tactic:
grind [Maximal, sup_le, le_iff_adj, edge_adj, huv.symm]

Premises used: SimpleGraph.Adj.symm, SimpleGraph.le_iff_adj, SimpleGraph.edge_adj, Maximal, sup_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

Tactic:
⟨reachable_eq_of_maximal_isAcyclic F, fun h ↦ ?_⟩

Premises used: SimpleGraph.reachable_eq_of_maximal_isAcyclic, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
refine : ∀ (h : F.Reachable = G.Reachable), Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F
⊢ Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F ↔ F.Reachable = G.Reachable

Tactic:
refine ⟨reachable_eq_of_maximal_isAcyclic F, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
by_contra : ∀ (this : ¬Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F), False
⊢ Maximal (fun (F : SimpleGraph V) ↦ F ≤ G ∧ F.IsAcyclic) F

Tactic:
by_contra
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
have : ∀ (H : SimpleGraph V) (hFH : F < H) (hHG : H ≤ G) (hH : H.IsAcyclic), False
⊢ False

Tactic:
have ⟨H, hFH, hHG, hH⟩ := exists_gt_of_not_maximal ⟨hle, hF⟩ this
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
have : ∀ (e : Sym2 V) (heH : e ∈ H.edgeSet) (heF : e ∉ F.edgeSet), False
⊢ False

Tactic:
have ⟨e, heH, heF⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hFH
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ e ∈ (F ⊔ fromEdgeSet {e}).edgeSet

Tactic:
simp [H.not_isDiag_of_mem_edgeSet heH]

Premises used: SimpleGraph.not_isDiag_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
refine : (F ⊔ fromEdgeSet {e}).IsAcyclic
⊢ (F ⊔ fromEdgeSet {e}).IsBridge e

Tactic:
refine isAcyclic_iff_forall_edge_isBridge.mp ?_ <| by simp [H.not_isDiag_of_mem_edgeSet heH]

Premises used: SimpleGraph.isAcyclic_iff_forall_edge_isBridge, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ {e} \ Sym2.diagSet ⊆ H.edgeSet

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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}).IsAcyclic

Tactic:
exact hH.anti <| sup_le_iff.mpr ⟨hFH.le, H.fromEdgeSet_le.mpr <| by grind⟩

Premises used: Iff.mpr, LT.lt.le, SimpleGraph.fromEdgeSet_le, sup_le_iff, And.intro, SimpleGraph.IsAcyclic.anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

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⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F

Tactic:
simpa using heF
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F

Tactic:
have : (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F := by simpa using heF
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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
⊢ False

Tactic:
cases e
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ (F ⊔ fromEdgeSet {s(x, y)}).Adj x y ∧ ¬G.Reachable x y

Tactic:
rw [isBridge_iff, this, h] at h_bridge

Premises used: SimpleGraph.isBridge_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
h_bridge₁ : (F ⊔ fromEdgeSet {s(x, y)}).Adj x y ∧ ¬G.Reachable x y
⊢ (F ⊔ fromEdgeSet {s(x, y)}).deleteEdges {s(x, y)} = F

Tactic:
rw [isBridge_iff, this, h] at h_bridge

Premises used: SimpleGraph.isBridge_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)}).Adj x y ∧ ¬G.Reachable x y
this : (F ⊔ fromEdgeSet {s(x, y)}).deleteEdges {s(x, y)} = F
⊢ False

Tactic:
h_bridge.right <| hHG heH |>.reachable

Premises used: SimpleGraph.Adj.reachable, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)}).Adj x y ∧ ¬G.Reachable x y
this : (F ⊔ fromEdgeSet {s(x, y)}).deleteEdges {s(x, y)} = F
⊢ False

Tactic:
exact h_bridge.right <| hHG heH |>.reachable

Premises used: SimpleGraph.Adj.reachable, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
⊢ Nonempty V

Tactic:
have := hG.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

Tactic:
⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩

Premises used: SimpleGraph.Connected.mk, And.right, And.left, Iff.intro, SimpleGraph.IsTree.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
refine_2 : ∀ (hT' : T.IsTree), Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

Tactic:
refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
u v : V
⊢ T.Reachable u v

Tactic:
G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v

Premises used: SimpleGraph.Connected.preconnected, Eq.rec, SimpleGraph.reachable_eq_of_maximal_isAcyclic, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
h : Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T
u v : V
⊢ T.Reachable u v

Tactic:
exact G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
refine_2₂ refine_2₃ : Eq.{u_1 + 1} (α := (u v : V) → Prop) ⊤ ⊤
⊢ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) T

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]

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.preconnected_iff_reachable_eq_top, SimpleGraph.maximal_isAcyclic_iff_reachable_eq, SimpleGraph.IsTree.connected, Iff.mp, SimpleGraph.IsTree.isAcyclic
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
inst : Nonempty V
T : SimpleGraph V
⊢ Maximal IsAcyclic T ↔ T.IsTree

Tactic:
simp [← connected_top.maximal_le_isAcyclic_iff_isTree le_top]

Premises used: SimpleGraph.connected_top, SimpleGraph.Connected.maximal_le_isAcyclic_iff_isTree, le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩

Premises used: SimpleGraph.IsTree, _private.0.SimpleGraph.isTree_iff_maximal_isAcyclic.match_1, Iff.intro, SimpleGraph.maximal_isAcyclic_iff_isTree, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
refine : ∀ (h : G.IsTree), Nonempty V ∧ Maximal IsAcyclic G
⊢ G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
⊢ Nonempty V

Tactic:
have := h.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
this : Nonempty V
⊢ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
⟨this, G.maximal_isAcyclic_iff_isTree.mpr h⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.maximal_isAcyclic_iff_isTree
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
this : Nonempty V
⊢ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
exact ⟨this, G.maximal_isAcyclic_iff_isTree.mpr h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
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
⊢ ∃ (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

Premises used: SimpleGraph.exists_maximal_isAcyclic_of_le_isAcyclic
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
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:
grind [maximal_isAcyclic_iff_reachable_eq, Maximal]

Premises used: SimpleGraph.maximal_isAcyclic_iff_reachable_eq, Maximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
obtain :
  ∀ (F : SimpleGraph V) (hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable),
    ∃ 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

Premises used: SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic, SimpleGraph.isAcyclic_bot, bot_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G F : SimpleGraph V
hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
obtain :
  ∀ (F : SimpleGraph V) (hF : H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable),
    ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree
⊢ ∃ (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

Premises used: SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
F : SimpleGraph V
hF : H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree

Tactic:
grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

Premises used: SimpleGraph.preconnected_iff_reachable_eq_top, SimpleGraph.IsTree, SimpleGraph.Connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
obtain : ∀ (F : SimpleGraph V) (hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable), ∃ T ≤ G, T.IsTree
⊢ ∃ T ≤ G, T.IsTree

Tactic:
obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot

Premises used: SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic, SimpleGraph.isAcyclic_bot, bot_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
F : SimpleGraph V
hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ T ≤ G, T.IsTree

Tactic:
grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

Premises used: SimpleGraph.preconnected_iff_reachable_eq_top, SimpleGraph.IsTree, SimpleGraph.Connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
inr : ∀ (hV : Finite 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

Tactic:
obtain hV | hV := (finite_or_infinite V).symm

Premises used: finite_or_infinite, Or.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Infinite V
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
inr : ∀ (this : (α : Type u_1) → [Finite α] → Fintype α), 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

Tactic:
have := Fintype.ofFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
inr : ∀ (T : SimpleGraph V) (hle : T ≤ G) (hT : T.IsTree), 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

Tactic:
obtain ⟨T, hle, hT⟩ := h.exists_isTree_le

Premises used: SimpleGraph.Connected.exists_isTree_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
inr : T.edgeFinset.card ≤ G.edgeFinset.card
⊢ Nat.card V ≤ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1

Tactic:
rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, add_le_add_iff_right,
    Nat.card_eq_fintype_card, ← edgeFinset_card]

Premises used: add_le_add_iff_right, SimpleGraph.edgeFinset_card, Nat.card_eq_fintype_card, SimpleGraph.IsTree.card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ T.edgeFinset ≤ G.edgeFinset

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ T.edgeFinset.card ≤ G.edgeFinset.card

Tactic:
exact Finset.card_mono <| by simpa

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
have : ∀ (this : Fintype V), G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V

Tactic:
have := Fintype.ofFinite V
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h : G.IsTree
⊢ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V

Tactic:
simpa [edgeFinset] using h.card_edgeFinset

Premises used: SimpleGraph.edgeFinset, SimpleGraph.IsTree.card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

Tactic:
refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
simp_rw : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
⊢ G.IsAcyclic

Tactic:
simp_rw [isAcyclic_iff_forall_adj_isBridge]

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)

Tactic:
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 ?_

Premises used: SimpleGraph.Connected.connected_delete_edge_of_not_isBridge, SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one, LE.le.not_gt, by_contra
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

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 ?_

Premises used: SimpleGraph.Connected.connected_delete_edge_of_not_isBridge, SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one, LE.le.not_gt, by_contra