awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
refine_2 : ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)
rw : ∀ (hy : y ∈ (f x).support), False
⊢ ((f y).firstDart ⋯).toProd = (y, x)

Tactic:
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]

Premises used: Iff.mpr, SimpleGraph.Adj.symm, SimpleGraph.Walk.cons, And.intro, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
this : (f x).takeUntil y hy = cons h nil
⊢ (((f x).takeUntil y hy).append ((f x).dropUntil y hy)).length ≤ (f y).length

Tactic:
rw [← take_spec _ hy] at h'

Premises used: SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
this : (f x).takeUntil y hy = cons h nil
h'₁ : (((f x).takeUntil y hy).append ((f x).dropUntil y hy)).length ≤ (f y).length
⊢ (f x).takeUntil y hy = cons h nil

Tactic:
rw [← take_spec _ hy] at h'

Premises used: SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
hy : y ∈ (f x).support
h' : (((f x).takeUntil y hy).append ((f x).dropUntil y hy)).length ≤ (f y).length
this : (f x).takeUntil y hy = cons h nil
⊢ False

Tactic:
simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'

Premises used: SimpleGraph.Walk.IsPath.dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
suffices : (f x).takeUntil y hy = cons h nil
⊢ False

Tactic:
suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ (f x).takeUntil y hy = cons h nil

Tactic:
(hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_

Premises used: SimpleGraph.IsTree.existsUnique_path, ExistsUnique.unique, SimpleGraph.Walk.IsPath.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
refine : (cons h nil).IsPath
⊢ (f x).takeUntil y hy = cons h nil

Tactic:
refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_

Premises used: SimpleGraph.IsTree.existsUnique_path, ExistsUnique.unique, SimpleGraph.Walk.IsPath.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ (cons h nil).IsPath

Tactic:
simp [h.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
case case₁ case₂ : (f x).takeUntil y hy = cons h nil
case₃ : (cons h nil).IsPath
⊢ False

Tactic:
case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]

Premises used: SimpleGraph.Adj.ne, SimpleGraph.IsTree.existsUnique_path, ExistsUnique.unique, SimpleGraph.Walk.IsPath.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
case₂ case₃ :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
refine_1 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ¬y = default
refine_2 refine_2₁ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((f y).firstDart ⋯).toProd = (y, x)
refine_2₂ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)
case₄ case₅ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length) (hy : y ∈ (f x).support), False
⊢ ∀ b ∈ G.edgeFinset,
    ∃ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a),
      (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha = b

Tactic:
case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro x y h
    wlog h' : (f x).length ≤ (f y).length generalizing x y
    · rw [Sym2.eq_swap]
      exact this y x h.symm (le_of_not_ge h')
    refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
    · rintro rfl
      rw [← hf' _ nil IsPath.nil, length_nil,
          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
          length_cons, length_nil] at h'
      simp at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]

Premises used: Finset.mem_singleton, Finset.mem_compl, Sym2.forall, Sym2.eq_swap, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_nil, SimpleGraph.mem_edgeFinset, SimpleGraph.Walk.IsPath.nil, SimpleGraph.IsTree.existsUnique_path, ExistsUnique.unique, SimpleGraph.Walk.length_cons, SimpleGraph.Walk.IsPath.takeUntil, SimpleGraph.mem_edgeSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
rw : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
⊢ G.IsTree

Tactic:
rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge, SimpleGraph.isTree_iff, Minimal.prop, and_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
x x_1 : V
h_1 : G.Adj x x_1
hbr : ¬G.IsBridge s(x, x_1)
⊢ G.deleteEdges {s(x, x_1)} < G

Tactic:
simpa [deleteEdges, ← edgeSet_ssubset_edgeSet]

Premises used: SimpleGraph.deleteEdges, SimpleGraph.edgeSet_ssubset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

Tactic:
exact fun _ _ _ ↦ by_contra fun hbr ↦ h.not_prop_of_lt
    (by simpa [deleteEdges, ← edgeSet_ssubset_edgeSet])
    <| h.prop.connected_delete_edge_of_not_isBridge hbr

Premises used: SimpleGraph.Connected.connected_delete_edge_of_not_isBridge, Minimal.not_prop_of_lt, Minimal.prop, by_contra
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Minimal Connected G

Tactic:
⟨fun htree ↦ ⟨htree.connected, fun G' h' hle u v hadj ↦ ?_⟩, isTree_of_minimal_connected⟩

Premises used: And.intro, Iff.intro, SimpleGraph.IsTree.connected, SimpleGraph.isTree_of_minimal_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
refine :
  ∀ (htree : G.IsTree) (G' : SimpleGraph V) (h' : G'.Connected) (hle : G' ≤ G) (u v : V) (hadj : G.Adj u v), G'.Adj u v
⊢ G.IsTree ↔ Minimal Connected G

Tactic:
refine ⟨fun htree ↦ ⟨htree.connected, fun G' h' hle u v hadj ↦ ?_⟩, isTree_of_minimal_connected⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
have : ∀ (p : G'.Walk u v) (hp : p.IsPath), G'.Adj u v
⊢ G'.Adj u v

Tactic:
have ⟨p, hp⟩ := h'.exists_isPath u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
⊢ (↑(Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) (mapLe hle p) ⋯) : G.Walk u v).edges =
    (↑(Path.singleton hadj) : G.Walk u v).edges

Tactic:
have := congrArg Walk.edges <| congrArg Subtype.val <|
    htree.isAcyclic.path_unique ⟨p.mapLe hle, hp.mapLe hle⟩ <| Path.singleton hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this :
  (↑(Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) (mapLe hle p) ⋯) : G.Walk u v).edges =
    (↑(Path.singleton hadj) : G.Walk u v).edges
⊢ p.edges = (↑(Path.singleton hadj) : G.Walk u v).edges

Tactic:
simp only [edges_map, Hom.coe_ofLE, Sym2.map_id, List.map_id_fun, id_eq] at this

Premises used: Sym2.map_id, List.map_id_fun, SimpleGraph.Walk.edges_map, SimpleGraph.Hom.coe_ofLE, id_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this : p.edges = (↑(Path.singleton hadj) : G.Walk u v).edges
⊢ G'.Adj u v

Tactic:
simp [this, p.adj_of_mem_edges]

Premises used: SimpleGraph.Walk.adj_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hnreach : ¬G.Reachable u v
hacyc : G.IsAcyclic
⊢ (G ⊔ edge u v).IsAcyclic

Tactic:
grind [isAcyclic_iff_forall_edge_isBridge, IsBridge.sup_edge_of_not_reachable,
    IsBridge.sup_edge_of_not_reachable_of_isBridge,
    edgeSet_sup, edgeSet_edge, IsBridge.of_not_reachable]

Premises used: SimpleGraph.IsBridge.of_not_reachable, SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridge, SimpleGraph.isAcyclic_iff_forall_edge_isBridge, SimpleGraph.edgeSet_edge, SimpleGraph.IsBridge.sup_edge_of_not_reachable, SimpleGraph.edgeSet_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
x y : V
hxy : ¬G.Reachable x y
⊢ (G ⊔ edge x y).IsAcyclic ↔ G.IsAcyclic

Tactic:
⟨.anti le_sup_left, .sup_edge_of_not_reachable hxy⟩

Premises used: le_sup_left, Iff.intro, SimpleGraph.IsAcyclic.sup_edge_of_not_reachable, SimpleGraph.IsAcyclic.anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)
neg : ∀ (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)

Tactic:
by_cases huv : u = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)

Tactic:
grind [sup_eq_left, edge_le, Sym2.mem_diagSet, Sym2.mk_isDiag_iff]

Premises used: sup_eq_left, SimpleGraph.edge_le, Sym2.mk_isDiag_iff, Sym2.mem_diagSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)
neg : ∀ (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)

Tactic:
by_cases hadj : G.Adj u v

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

Tactic:
grind [sup_eq_left, edge_le, mem_edgeSet]

Premises used: sup_eq_left, SimpleGraph.edge_le, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
h : G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
hacyc : G.IsAcyclic
hreach : G.Reachable u v → u = v ∨ G.Adj u v
⊢ ¬G.Reachable u v

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
neg : (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)

Tactic:
refine ⟨?_, fun ⟨hacyc, hreach⟩ ↦ hacyc.sup_edge_of_not_reachable <| by grind⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)

Tactic:
fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩

Premises used: le_sup_left, False.elim, And.intro, SimpleGraph.IsAcyclic.anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
neg : ∀ (hacyc : (G ⊔ edge u v).IsAcyclic) (hreach : G.Reachable u v), False
⊢ (G ⊔ edge u v).IsAcyclic → G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)

Tactic:
refine fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ s(u, v) ∈ (G ⊔ edge u v).edgeSet

Tactic:
simp [huv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
neg : ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
⊢ False

Tactic:
refine (isAcyclic_iff_forall_edge_isBridge.mp (e := s(u, v)) hacyc <| by simp [huv]).right ?_

Premises used: SimpleGraph.isAcyclic_iff_forall_edge_isBridge, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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.Reachable u v

Tactic:
hreach
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
h : (G ⊔ edge u v).deleteEdges {s(u, v)} = G
⊢ ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2

Tactic:
convert! hreach
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)} = G

Tactic:
simpa [deleteEdges_sup]

Premises used: SimpleGraph.deleteEdges_sup
-- 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
h₁ : ∀ (u v : V), F.Reachable u v ↔ G.Reachable u v
⊢ F.Reachable = G.Reachable

Tactic:
ext u v
-- 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
⊢ F.Reachable u v ↔ G.Reachable u v

Tactic:
⟨.mono h.prop.left, fun ⟨p⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.reachable_eq_of_maximal_isAcyclic.match_1, Maximal.prop, And.left, SimpleGraph.Reachable.mono, Iff.intro, SimpleGraph.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₁ : G.Reachable u v → ∀ (p : G.Walk u v), F.Reachable u v
⊢ F.Reachable u v ↔ G.Reachable u v

Tactic:
refine ⟨.mono h.prop.left, fun ⟨p⟩ ↦ ?_⟩
-- 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
h₁ : ∀ (this : ¬F.Reachable u v), False
⊢ F.Reachable u v

Tactic:
by_contra
-- 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 : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
⊢ v ∉ s

Tactic:
have : v ∉ s := this ∘ s.reachable_of_mem_supp rfl
-- 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 : v ∉ s
⊢ ∃ 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
-- 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
this : ∃ d ∈ p.darts, d.toProd.1 ∈ s ∧ d.toProd.2 ∉ s
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
⊢ False

Tactic:
rcases this with ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩
-- 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 : 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
⊢ ¬F.Reachable v' u'

Tactic:
have : ¬F.Reachable v' u' := mt ConnectedComponent.sound <| s.mem_supp_iff u' |>.mp hu ▸ hv
-- 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_3 : ¬F.Reachable v' u'
this : F ⊔ edge v' u' ≤ F
⊢ False

Tactic:
grind [Adj.reachable, sup_le_iff, le_iff_adj, edge_adj]

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.le_iff_adj, sup_le_iff, SimpleGraph.edge_adj
-- 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' ≤ F
⊢ False

Tactic:
suffices F ⊔ edge v' u' ≤ F by
    grind [Adj.reachable, sup_le_iff, le_iff_adj, edge_adj]