awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u : α
⊢ eccent ⊥ u = ⊤

Tactic:
eccent_eq_top_of_not_connected not_connected_bot u

Premises used: SimpleGraph.eccent_eq_top_of_not_connected, SimpleGraph.not_connected_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u : α
apply : eccent ⊤ u ≤ 1
⊢ eccent ⊤ u = 1

Tactic:
apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u

Premises used: Iff.mpr, SimpleGraph.eccent_ne_zero, le_antisymm, pos_iff_ne_zero, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u : α
rw : ∀ (i : α), edist ⊤ u i ≤ 1
⊢ eccent ⊤ u ≤ 1

Tactic:
rw [eccent, iSup_le_iff]

Premises used: iSup_le_iff, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u v : α
inl : u = v → edist ⊤ u v ≤ 1
inr : u ≠ v → edist ⊤ u v ≤ 1
⊢ edist ⊤ u v ≤ 1

Tactic:
cases eq_or_ne u v

Premises used: eq_or_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u v : α
h : u = v
⊢ edist ⊤ u v ≤ 1

Tactic:
simp_all [edist_top_of_ne]

Premises used: SimpleGraph.edist_top_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
u v : α
h : u ≠ v
⊢ edist ⊤ u v ≤ 1

Tactic:
simp_all [edist_top_of_ne]

Premises used: SimpleGraph.edist_top_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G = ⊤ ↔ ∀ (u : α), G.eccent u = 1

Tactic:
⟨fun h ↦ h ▸ eccent_top, fun h ↦ ?_⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, SimpleGraph.eccent_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
refine : ∀ (h : ∀ (u : α), G.eccent u = 1), G = ⊤
⊢ G = ⊤ ↔ ∀ (u : α), G.eccent u = 1

Tactic:
refine ⟨fun h ↦ h ▸ eccent_top, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
Adj : ∀ (u v : α), G.Adj u v ↔ SimpleGraph.Adj ⊤ u v
⊢ G = ⊤

Tactic:
ext u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
⊢ G.Adj u v ↔ Adj ⊤ u v

Tactic:
⟨Adj.ne, fun huv ↦ ?_⟩

Premises used: SimpleGraph.Adj.ne, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
Adj : ∀ (huv : SimpleGraph.Adj ⊤ u v), G.Adj u v
⊢ G.Adj u v ↔ SimpleGraph.Adj ⊤ u v

Tactic:
refine ⟨Adj.ne, fun huv ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : SimpleGraph.Adj ⊤ u v
Adj : G.edist u v = 1
⊢ G.Adj u v

Tactic:
rw [← edist_eq_one_iff_adj]

Premises used: SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : SimpleGraph.Adj ⊤ u v
Adj : 1 ≤ G.edist u v
⊢ G.edist u v = 1

Tactic:
apply le_antisymm ((h u).symm ▸ edist_le_eccent)

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : SimpleGraph.Adj ⊤ u v
Adj : u ≠ v
⊢ 1 ≤ G.edist u v

Tactic:
rw [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff.ne]

Premises used: Iff.ne, SimpleGraph.edist_eq_zero_iff, pos_iff_ne_zero, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : Adj ⊤ u v
⊢ u ≠ v

Tactic:
huv.ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : Adj ⊤ u v
⊢ u ≠ v

Tactic:
exact huv.ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
k : ℕ∞
⊢ G.eccent u ≤ k ↔ ∀ (v : α), G.edist u v ≤ k

Tactic:
iSup_le_iff

Premises used: iSup_le_iff, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
mp : G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v
mpr : (∀ (v : α), u ≠ v → G.Adj u v) → G.eccent u ≤ 1
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
⊢ G.edist u v ≤ 1

Tactic:
have hd : G.edist u v ≤ 1 := edist_le_eccent.trans h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
hd : G.edist u v ≤ 1
⊢ 1 ≤ G.edist u v

Tactic:
have hd' : 1 ≤ G.edist u v := Order.one_le_iff_pos.mpr (G.edist_pos_of_ne huv)
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
hd : G.edist u v ≤ 1
hd' : 1 ≤ G.edist u v
⊢ G.Adj u v

Tactic:
edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm

Premises used: le_antisymm, Iff.mp, Eq.symm, SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
hd : G.edist u v ≤ 1
hd' : 1 ≤ G.edist u v
⊢ G.Adj u v

Tactic:
exact edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm

Premises used: le_antisymm, Iff.mp, Eq.symm, SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
mpr : ∀ (v : α), G.edist u v ≤ 1
⊢ G.eccent u ≤ 1

Tactic:
rw [eccent_le_iff]

Premises used: SimpleGraph.eccent_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
mpr : G.Adj u v ∨ u = v
⊢ G.edist u v ≤ 1

Tactic:
rw [edist_le_one_iff_adj_or_eq]

Premises used: SimpleGraph.edist_le_one_iff_adj_or_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.Adj u v ∨ u = v

Tactic:
or_iff_not_imp_right.mpr (hall v)

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.Adj u v ∨ u = v

Tactic:
exact or_iff_not_imp_right.mpr (hall v)

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
⊢ 1 ≤ G.eccent u

Tactic:
have h : 1 ≤ G.eccent u := ENat.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
h : 1 ≤ G.eccent u
rw : G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
rw [← h.ge_iff_eq']

Premises used: LE.le.ge_iff_eq'
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
h : 1 ≤ G.eccent u
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
eccent_le_one_iff u

Premises used: SimpleGraph.eccent_le_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
h : 1 ≤ G.eccent u
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
exact eccent_le_one_iff u

Premises used: SimpleGraph.eccent_le_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ (u : α), ⨆ (v : α), G.edist u v

Tactic:
rfl

Premises used: SimpleGraph.ediam, rfl, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
rw : Eq (α := ℕ∞) (⨆ (u : α), G.eccent u) (⨆ (p : α × α), G.edist p.1 p.2)
rw₁ : Eq (α := ℕ∞) (⨆ (u : α), (fun (u : α) ↦ (⨆ (v : α), G.edist u v : ℕ∞)) u) (⨆ (p : α × α), G.edist p.1 p.2)
rw₂ rw₃ :
  Eq (α := ℕ∞) (⨆ (u : α), (fun (u : α) ↦ (⨆ (v : α), G.edist u v : ℕ∞)) u)
    (⨆ (i : α), ⨆ (j : α), G.edist (i, j).1 (i, j).2)
⊢ G.ediam = ⨆ (p : α × α), G.edist p.1 p.2

Tactic:
rw [ediam, eccent_def, iSup_prod]

Premises used: SimpleGraph.ediam, SimpleGraph.eccent_def, iSup_prod
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ G.ediam

Tactic:
le_iSup G.eccent u

Premises used: le_iSup, SimpleGraph.ediam, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v : α
⊢ G.edist u v ≤ G.ediam

Tactic:
le_iSup₂ (f := G.edist) u v

Premises used: le_iSup₂, SimpleGraph.ediam, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
k : ℕ∞
h : ∀ (u v : α), G.edist u v ≤ k
⊢ G.ediam ≤ k

Tactic:
iSup₂_le h

Premises used: iSup₂_le, SimpleGraph.ediam, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
k : ℕ∞
⊢ G.ediam ≤ k ↔ ∀ (u v : α), G.edist u v ≤ k

Tactic:
iSup₂_le_iff

Premises used: SimpleGraph.ediam, iSup₂_le_iff, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ (u : α) (v : α), b < G.edist u v

Tactic:
simp only [ediam, eccent, iSup_eq_top, lt_iSup_iff]

Premises used: iSup_eq_top, SimpleGraph.ediam, SimpleGraph.eccent, lt_iSup_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
⊢ G.ediam = 0

Tactic:
simp [ediam_def]

Premises used: SimpleGraph.ediam_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ 0
contrapose! : ∀ (h : Subsingleton α), G.ediam = 0
⊢ Nontrivial α

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.ediam = 0

Tactic:
ediam_eq_zero_of_subsingleton

Premises used: SimpleGraph.ediam_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.ediam = 0

Tactic:
exact ediam_eq_zero_of_subsingleton

Premises used: SimpleGraph.ediam_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
obtain : ∀ (u v : α) (huv : u ≠ v), G.ediam ≠ 0
⊢ G.ediam ≠ 0

Tactic:
obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_›

Premises used: exists_pair_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : u ≠ v
contrapose : ∀ (huv : G.ediam = 0), u = v
⊢ G.ediam ≠ 0

Tactic:
contrapose huv
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : G.ediam = 0
⊢ ∀ (i i_1 : α), i = i_1

Tactic:
simp only [ediam, eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv

Premises used: SimpleGraph.ediam, ENat.iSup_eq_zero, SimpleGraph.edist_eq_zero_iff, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : ∀ (i i_1 : α), i = i_1
⊢ u = v

Tactic:
huv u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : ∀ (i i_1 : α), i = i_1
⊢ u = v

Tactic:
exact huv u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
contrapose! : ∀ (h : Nontrivial α), G.ediam ≠ 0
⊢ Subsingleton α

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
ediam_ne_zero

Premises used: SimpleGraph.ediam_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
exact ediam_ne_zero

Premises used: SimpleGraph.ediam_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam ≠ 0 ↔ Nontrivial α

Tactic:
⟨nontrivial_of_ediam_ne_zero, fun _ ↦ ediam_ne_zero⟩

Premises used: SimpleGraph.nontrivial_of_ediam_ne_zero, SimpleGraph.ediam_ne_zero, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = 0 ↔ Subsingleton α

Tactic:
⟨subsingleton_of_ediam_eq_zero, fun _ ↦ ediam_eq_zero_of_subsingleton⟩

Premises used: SimpleGraph.ediam_eq_zero_of_subsingleton, Iff.intro, SimpleGraph.subsingleton_of_ediam_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.Connected
⊢ ¬∃ (v : α), ∀ (w : α), G.Reachable v w

Tactic:
rw [connected_iff_exists_forall_reachable] at h

Premises used: SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w
⊢ ∀ (v : α), ∃ (w : α), ¬G.Reachable v w

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
obtain : ∀ (w : α) (hw : ¬G.Reachable Classical.ofNonempty w), G.ediam = ⊤
⊢ G.ediam = ⊤

Tactic:
obtain ⟨_, hw⟩ := h Classical.ofNonempty

Premises used: Classical.ofNonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
w : α
hw : ¬G.Reachable Classical.ofNonempty w
rw : G.edist Classical.ofNonempty w ≤ G.ediam
⊢ G.ediam = ⊤

Tactic:
rw [eq_top_iff, ← edist_eq_top_of_not_reachable hw]

Premises used: eq_top_iff, SimpleGraph.edist_eq_top_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
w : α
hw : ¬G.Reachable Classical.ofNonempty w
⊢ G.edist Classical.ofNonempty w ≤ G.ediam

Tactic:
edist_le_ediam

Premises used: SimpleGraph.edist_le_ediam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
w : α
hw : ¬G.Reachable Classical.ofNonempty w
⊢ G.edist Classical.ofNonempty w ≤ G.ediam

Tactic:
exact edist_le_ediam

Premises used: SimpleGraph.edist_le_ediam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
inl : IsEmpty α → G.ediam = ⊤
inr : Nonempty α → G.ediam = ⊤
⊢ G.ediam = ⊤

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : IsEmpty α
inl : False
⊢ G.ediam = ⊤

Tactic:
exfalso
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : IsEmpty α
⊢ False

Tactic:
h <| IsEmpty.forall_iff.mpr trivial

Premises used: Iff.mpr, trivial, IsEmpty.forall_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : IsEmpty α
⊢ False

Tactic:
exact h <| IsEmpty.forall_iff.mpr trivial

Premises used: Iff.mpr, trivial, IsEmpty.forall_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
inr : ¬G.Connected
⊢ G.ediam = ⊤

Tactic:
apply ediam_eq_top_of_not_connected

Premises used: SimpleGraph.ediam_eq_top_of_not_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
inr : ¬(G.Preconnected ∧ Nonempty α)
⊢ ¬G.Connected

Tactic:
rw [connected_iff]

Premises used: SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
inr : G.Preconnected → Nonempty α → False
⊢ ¬(G.Preconnected ∧ Nonempty α)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ ⊤
⊢ G.Preconnected

Tactic:
Not.imp_symm G.ediam_eq_top_of_not_preconnected h

Premises used: Not.imp_symm, SimpleGraph.ediam_eq_top_of_not_preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.ediam ≠ ⊤
⊢ G.Connected

Tactic:
G.connected_iff.mpr ⟨preconnected_of_ediam_ne_top h, ‹_›⟩

Premises used: Iff.mpr, SimpleGraph.preconnected_of_ediam_ne_top, And.intro, SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.ediam ≠ ⊤
⊢ ∃ (u : α), G.eccent u = G.ediam

Tactic:
ENat.exists_eq_iSup_of_lt_top h.lt_top

Premises used: ENat.exists_eq_iSup_of_lt_top, SimpleGraph.ediam, Ne.lt_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ ∃ (u : α), G.eccent u = G.ediam

Tactic:
exists_eq_ciSup_of_finite

Premises used: SimpleGraph.ediam, exists_eq_ciSup_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.ediam ≠ ⊤
⊢ ∃ (u : α) (v : α), G.edist u v = G.ediam

Tactic:
ENat.exists_eq_iSup₂_of_lt_top h.lt_top

Premises used: SimpleGraph.ediam, Ne.lt_top, ENat.exists_eq_iSup₂_of_lt_top, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ ∃ (u : α) (v : α), G.edist u v = G.ediam

Tactic:
Prod.exists'.mp <| ediam_def ▸ exists_eq_ciSup_of_finite

Premises used: Prod.exists', Eq.rec, Iff.mp, SimpleGraph.ediam_def, exists_eq_ciSup_of_finite, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ G.Connected ↔ G.ediam ≠ ⊤

Tactic:
have ⟨u, v, huv⟩ := G.exists_edist_eq_ediam_of_finite
  ⟨fun h ↦ huv ▸ edist_ne_top_iff_reachable.mpr (h u v),
   fun h ↦ G.connected_of_ediam_ne_top h⟩

Premises used: Iff.mpr, SimpleGraph.Connected.preconnected, _private.0.SimpleGraph.connected_iff_ediam_ne_top.match_1, SimpleGraph.connected_of_ediam_ne_top, SimpleGraph.edist_ne_top_iff_reachable, Eq.rec, SimpleGraph.ediam, Ne, SimpleGraph.Connected, Iff, Iff.intro, Top.top, SimpleGraph.exists_edist_eq_ediam_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G G' : SimpleGraph α
h : G ≤ G'
⊢ G'.ediam ≤ G.ediam

Tactic:
iSup₂_mono fun _ _ ↦ edist_anti h

Premises used: iSup₂_mono, SimpleGraph.ediam, SimpleGraph.edist_anti, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
⊢ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
ediam_eq_top_of_not_connected not_connected_bot

Premises used: SimpleGraph.not_connected_bot, SimpleGraph.ediam_eq_top_of_not_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
⊢ ediam.{u_1} (α := α) ⊤ = 1

Tactic:
simp [ediam]

Premises used: SimpleGraph.ediam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩

Premises used: Eq.rec, SimpleGraph.ediam_top, Iff.intro, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
refine : ∀ (h : G.ediam = 1), G = ⊤
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
rw : ∀ (u : α), G.eccent u = 1
⊢ G = ⊤

Tactic:
rw [eq_top_iff_forall_eccent_eq_one]

Premises used: SimpleGraph.eq_top_iff_forall_eccent_eq_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
apply : 1 ≤ G.eccent u
⊢ G.eccent u = 1

Tactic:
apply le_antisymm (h ▸ eccent_le_ediam)

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
rw : G.eccent u ≠ 0
⊢ 1 ≤ G.eccent u

Tactic:
rw [Order.one_le_iff_pos, pos_iff_ne_zero]

Premises used: pos_iff_ne_zero, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
⊢ G.eccent u ≠ 0

Tactic:
eccent_ne_zero u

Premises used: SimpleGraph.eccent_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
⊢ G.eccent u ≠ 0

Tactic:
exact eccent_ne_zero u

Premises used: SimpleGraph.eccent_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.ediam ≤ 2 * G.eccent u

Tactic:
ediam_le_of_edist_le fun v w ↦ ?_

Premises used: SimpleGraph.ediam_le_of_edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
refine : ∀ (v w : α), G.edist v w ≤ 2 * G.eccent u
⊢ G.ediam ≤ 2 * G.eccent u

Tactic:
refine ediam_le_of_edist_le fun v w ↦ ?_

Premises used: SimpleGraph.ediam_le_of_edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v w ≤ G.edist v u + G.edist u w

Tactic:
G.edist_triangle

Premises used: SimpleGraph.edist_triangle
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
rw rw₁ : G.edist u v + G.edist u w = G.edist u v + G.edist u w
⊢ G.edist v u + G.edist u w = G.edist u v + G.edist u w

Tactic:
rw [edist_comm]

Premises used: SimpleGraph.edist_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist u v + G.edist u w ≤ G.eccent u + G.eccent u

Tactic:
add_le_add edist_le_eccent edist_le_eccent

Premises used: add_le_add, SimpleGraph.edist_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.eccent u + G.eccent u = 2 * G.eccent u

Tactic:
(two_mul _).symm

Premises used: two_mul, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
v₁ : G.edist v u + G.edist u w = G.edist u v + G.edist u w
⊢ G.edist v w ≤ 2 * G.eccent u

Tactic:
calc
    G.edist v w
      ≤ G.edist v u + G.edist u w := G.edist_triangle
    _ = G.edist u v + G.edist u w := by rw [edist_comm]
    _ ≤ G.eccent u + G.eccent u := add_le_add edist_le_eccent edist_le_eccent
    _ = 2 * G.eccent u := (two_mul _).symm

Premises used: add_le_add, two_mul, SimpleGraph.edist_le_eccent, SimpleGraph.edist_triangle, SimpleGraph.edist, Eq.symm, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
rw : G.ediam.toNat = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
rw₁ rw₂ : ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2) = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
⊢ G.diam = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)

Tactic:
rw [diam, ediam_def]

Premises used: SimpleGraph.ediam_def, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ ⊤
u v : α
⊢ G.dist u v ≤ G.diam

Tactic:
ENat.toNat_le_toNat edist_le_ediam h

Premises used: SimpleGraph.dist, ENat.toNat_le_toNat, SimpleGraph.edist_le_ediam, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
contrapose! : ∀ (h : Subsingleton α), G.diam = 0
⊢ Nontrivial α

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.diam = 0

Tactic:
simp [diam, h]

Premises used: SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
inl : IsEmpty α → G.diam = 0
inr : Nonempty α → G.diam = 0
⊢ G.diam = 0

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty