awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : IsEmpty α
inl : ENat.toNat 0 = 0
⊢ G.diam = 0

Tactic:
rw [diam, ediam, ciSup_of_empty, bot_eq_zero']

Premises used: SimpleGraph.ediam, ciSup_of_empty, SimpleGraph.diam, bot_eq_zero'
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : IsEmpty α
⊢ ENat.toNat 0 = 0

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : Nonempty α
inr : G.ediam.toNat = 0
inr₁ : ENat.toNat ⊤ = 0
inr₂ inr₃ : Eq (α := ℕ) 0 0
⊢ G.diam = 0

Tactic:
rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]

Premises used: SimpleGraph.ediam_eq_top_of_not_connected, ENat.toNat_top, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
rw : G.ediam.toNat = 0
rw₁ : ENat.toNat ⊤ = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ G.diam = 0

Tactic:
rw [diam, h, ENat.toNat_top]

Premises used: ENat.toNat_top, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ G.ediam ≠ ⊤

Tactic:
mt diam_eq_zero_of_ediam_eq_top h

Premises used: SimpleGraph.diam_eq_zero_of_ediam_eq_top, mt
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
pos : ∀ (h : G.diam = 0), ∃ (u : α) (v : α), G.dist u v = G.diam
neg : ∀ (h : ¬G.diam = 0), ∃ (u : α) (v : α), G.dist u v = G.diam
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam

Tactic:
by_cases h : G.diam = 0

Premises used: SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.diam = 0
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
neg : ∀ (u v : α) (huv : G.edist u v = G.ediam), ∃ (u : α) (v : α), G.dist u v = G.diam
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam

Tactic:
obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h

Premises used: SimpleGraph.exists_edist_eq_ediam_of_ne_top, SimpleGraph.ediam_ne_top_of_diam_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
h₁ : G.dist u v = G.diam
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam

Tactic:
use u, v
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
h₁ : G.dist u v = G.ediam.toNat
h₂ : (G.edist u v).toNat = G.ediam.toNat
h₃ h₄ : G.ediam.toNat = G.ediam.toNat
⊢ G.dist u v = G.diam

Tactic:
rw [diam, dist, congrArg ENat.toNat huv]

Premises used: SimpleGraph.dist, congrArg, ENat.toNat, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam ≠ ⊤
⊢ G.diam ≠ 0

Tactic:
have ⟨_, _, hne⟩ := exists_pair_ne ‹_›
  pos_iff_ne_zero.mp <|
    lt_of_lt_of_le ((connected_of_ediam_ne_top h).pos_dist_of_ne hne) <| dist_le_diam h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G G' : SimpleGraph α
h : G ≤ G'
hn : G.ediam ≠ ⊤
⊢ G'.diam ≤ G.diam

Tactic:
ENat.toNat_le_toNat (ediam_anti h) hn

Premises used: SimpleGraph.ediam_anti, ENat.toNat_le_toNat, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
rw : ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
⊢ diam.{u_1} (α := α) ⊥ = 0

Tactic:
rw [diam, ENat.toNat_eq_zero]

Premises used: ENat.toNat_eq_zero, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inl : Subsingleton α → ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
inr : Nontrivial α → ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
Or.inl ediam_eq_zero_of_subsingleton

Premises used: SimpleGraph.ediam_eq_zero_of_subsingleton, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
exact Or.inl ediam_eq_zero_of_subsingleton

Premises used: SimpleGraph.ediam_eq_zero_of_subsingleton, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
Or.inr ediam_bot

Premises used: SimpleGraph.ediam_bot, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤

Tactic:
exact Or.inr ediam_bot

Premises used: SimpleGraph.ediam_bot, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
rw : (ediam.{u_1} (α := α) ⊤).toNat = 1
rw₁ : ENat.toNat 1 = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ diam.{u_1} (α := α) ⊤ = 1

Tactic:
rw [diam, ediam_top, ENat.toNat_one]

Premises used: ENat.toNat_one, SimpleGraph.ediam_top, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
rw : G.ediam.toNat = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
rw₁ : G.ediam = 0 ∨ G.ediam = ⊤ ↔ G.ediam = ⊤ ∨ Subsingleton α
rw₂ : G.ediam = ⊤ ∨ G.ediam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
rw₃ rw₄ : G.ediam = ⊤ ∨ Subsingleton α ↔ G.ediam = ⊤ ∨ Subsingleton α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]

Premises used: SimpleGraph.ediam_eq_zero_iff_subsingleton, ENat.toNat_eq_zero, or_comm, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : G.ediam.toNat = 1 ↔ G = ⊤
rw₁ : G.ediam = (↑1 : ℕ∞) ↔ G = ⊤
rw₂ : G.ediam = 1 ↔ G = ⊤
rw₃ rw₄ : G = ⊤ ↔ G = ⊤
⊢ G.diam = 1 ↔ G = ⊤

Tactic:
rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]

Premises used: ENat.toNat_eq_iff, SimpleGraph.ediam_eq_one, one_ne_zero, Nat.cast_one, SimpleGraph.diam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : ¬G.diam = 0 ↔ ¬G.ediam = ⊤
⊢ G.diam = 0 ↔ G.ediam = ⊤

Tactic:
rw [← not_iff_not]

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

Tactic:
⟨ediam_ne_top_of_diam_ne_zero, diam_ne_zero_of_ediam_ne_top⟩

Premises used: SimpleGraph.diam_ne_zero_of_ediam_ne_top, Iff.intro, SimpleGraph.ediam_ne_top_of_diam_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ ¬G.diam = 0 ↔ ¬G.ediam = ⊤

Tactic:
exact ⟨ediam_ne_top_of_diam_ne_zero, diam_ne_zero_of_ediam_ne_top⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Finite α
inst_1 : Nontrivial α
rw : G.ediam ≠ ⊤ ↔ G.diam ≠ 0
rw₁ : G.ediam = ⊤ ↔ G.diam = 0
rw₂ rw₃ : G.ediam = ⊤ ↔ G.ediam = ⊤
⊢ G.Connected ↔ G.diam ≠ 0

Tactic:
rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]

Premises used: not_iff_not, SimpleGraph.connected_iff_ediam_ne_top, SimpleGraph.diam_eq_zero_iff_ediam_eq_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.radius = ⨅ (u : α), ⨆ (v : α), G.edist u v

Tactic:
rfl

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

Tactic:
iInf_le G.eccent u

Premises used: SimpleGraph.radius, iInf_le, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ ∃ (u : α), G.eccent u = G.radius

Tactic:
ENat.exists_eq_iInf G.eccent

Premises used: ENat.exists_eq_iInf, SimpleGraph.radius, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
obtain : ∀ (w : α) (hw : G.eccent w = G.radius), ∃ (u : α) (v : α), G.edist u v = G.radius
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius

Tactic:
obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius

Premises used: SimpleGraph.exists_eccent_eq_radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
w : α
hw : G.eccent w = G.radius
obtain : ∀ (v : α) (hv : G.edist w v = G.eccent w), ∃ (u : α) (v : α), G.edist u v = G.radius
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius

Tactic:
obtain ⟨v, hv⟩ := G.exists_edist_eq_eccent_of_finite w

Premises used: SimpleGraph.exists_edist_eq_eccent_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
h : G.edist w v = G.radius
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius

Tactic:
use w, v
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
h : G.eccent w = G.radius
h₁ h₂ : G.radius = G.radius
⊢ G.edist w v = G.radius

Tactic:
rw [hv, hw]
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
⊢ G.radius = ⊤

Tactic:
simp [radius, eccent_eq_top_of_not_connected h]

Premises used: SimpleGraph.eccent_eq_top_of_not_connected, SimpleGraph.radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : IsEmpty α
⊢ G.radius = ⊤

Tactic:
iInf_of_empty G.eccent

Premises used: iInf_of_empty, SimpleGraph.radius, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ G.radius ≠ ⊤ ↔ G.Connected

Tactic:
⟨Not.imp_symm radius_eq_top_of_not_connected, fun h ↦ ?_⟩

Premises used: Not.imp_symm, Iff.intro, SimpleGraph.radius_eq_top_of_not_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
refine : ∀ (h : G.Connected), G.radius ≠ ⊤
⊢ G.radius ≠ ⊤ ↔ G.Connected

Tactic:
refine ⟨Not.imp_symm radius_eq_top_of_not_connected, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
obtain : ∀ (u v : α) (huv : G.edist u v = G.radius), G.radius ≠ ⊤
⊢ G.radius ≠ ⊤

Tactic:
obtain ⟨u, v, huv⟩ := G.exists_edist_eq_radius_of_finite

Premises used: SimpleGraph.exists_edist_eq_radius_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
rw : G.Reachable u v
⊢ G.radius ≠ ⊤

Tactic:
rw [← huv, edist_ne_top_iff_reachable]

Premises used: SimpleGraph.edist_ne_top_iff_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
⊢ G.Reachable u v

Tactic:
h u v

Premises used: SimpleGraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
⊢ G.Reachable u v

Tactic:
exact h u v

Premises used: SimpleGraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : 1 ≤ G.radius
⊢ G.radius ≠ 0

Tactic:
rw [← ENat.one_le_iff_ne_zero]

Premises used: ENat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (i : α), 1 ≤ G.eccent i
⊢ 1 ≤ G.radius

Tactic:
apply le_iInf

Premises used: le_iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ ∀ (i : α), 1 ≤ G.eccent i

Tactic:
simp [ENat.one_le_iff_ne_zero, G.eccent_ne_zero]

Premises used: SimpleGraph.eccent_ne_zero, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α

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

Premises used: _private.0.SimpleGraph.radius_eq_zero_iff.match_1, SimpleGraph.radius, And.intro, Iff.intro, OfNat.ofNat, Eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
refine_1 : ∀ (h : G.radius = 0), Nonempty α
refine_2 : ∀ (h : G.radius = 0), Subsingleton α
refine_3 : Nonempty α ∧ Subsingleton α → Nonempty α → Subsingleton α → G.radius = 0
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
refine_1 : ∀ (h : IsEmpty α), G.radius ≠ 0
⊢ Nonempty α

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

Tactic:
simp [radius]

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

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

Tactic:
simp [radius_ne_zero_of_nontrivial]

Premises used: SimpleGraph.radius_ne_zero_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α ∧ Subsingleton α
left : Nonempty α
right : Subsingleton α
refine_3 : ∃ (i : α), G.eccent i = 0
⊢ G.radius = 0

Tactic:
rw [radius, ENat.iInf_eq_zero]

Premises used: SimpleGraph.radius, ENat.iInf_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h_1 : Nonempty α ∧ Subsingleton α
left : Nonempty α
right : Subsingleton α
h : G.eccent Classical.ofNonempty = 0
⊢ ∃ (i : α), G.eccent i = 0

Tactic:
use Classical.ofNonempty

Premises used: Classical.ofNonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α ∧ Subsingleton α
left : Nonempty α
right : Subsingleton α
⊢ G.eccent Classical.ofNonempty = 0

Tactic:
simpa [eccent] using Subsingleton.elim _

Premises used: Subsingleton.elim, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.radius ≤ G.ediam

Tactic:
iInf_le_iSup

Premises used: SimpleGraph.ediam, SimpleGraph.radius, iInf_le_iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.ediam = ⊤ ↔ G.radius = ⊤

Tactic:
⟨?_, fun hr ↦ eq_top_iff.mpr (hr ▸ radius_le_ediam)⟩

Premises used: Iff.mpr, eq_top_iff, Eq.rec, Iff.intro, SimpleGraph.radius_le_ediam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
refine : G.ediam = ⊤ → G.radius = ⊤
⊢ G.ediam = ⊤ ↔ G.radius = ⊤

Tactic:
refine ⟨?_, fun hr ↦ eq_top_iff.mpr (hr ▸ radius_le_ediam)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
contrapose : ¬G.radius = ⊤ → ¬G.ediam = ⊤
⊢ G.ediam = ⊤ → G.radius = ⊤

Tactic:
contrapose
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
obtain : ∀ (w : α) (hw : G.eccent w = G.radius), ¬G.ediam = ⊤
⊢ ¬G.ediam = ⊤

Tactic:
obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius

Premises used: SimpleGraph.exists_eccent_eq_radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
⊢ G.ediam ≤ 2 * G.eccent w

Tactic:
have hdiam : G.ediam ≤ 2 * G.eccent w := ediam_le_two_mul_eccent w
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
hdiam : G.ediam ≤ 2 * G.eccent w
⊢ ¬G.ediam = ⊤

Tactic:
ne_top_of_lt <| lt_of_le_of_lt hdiam <| WithTop.mul_lt_top (ENat.coe_lt_top 2) <|
    lt_top_iff_ne_top.mpr (hw ▸ hr)

Premises used: Iff.mpr, lt_of_le_of_lt, Eq.rec, lt_top_iff_ne_top, WithTop.mul_lt_top, OfNat.ofNat, Eq.symm, ne_top_of_lt, ENat.coe_lt_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
hdiam : G.ediam ≤ 2 * G.eccent w
⊢ ¬G.ediam = ⊤

Tactic:
exact ne_top_of_lt <| lt_of_le_of_lt hdiam <| WithTop.mul_lt_top (ENat.coe_lt_top 2) <|
    lt_top_iff_ne_top.mpr (hw ▸ hr)

Premises used: Iff.mpr, lt_of_le_of_lt, lt_top_iff_ne_top, WithTop.mul_lt_top, OfNat.ofNat, ne_top_of_lt, ENat.coe_lt_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inl : IsEmpty α → G.ediam ≤ 2 * G.radius
inr : Nonempty α → G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : IsEmpty α
inl : G.ediam ≤ HMul.hMul (α := ℕ∞) 2 ⊤
⊢ G.ediam ≤ 2 * G.radius

Tactic:
rw [radius_eq_top_of_isEmpty]

Premises used: SimpleGraph.radius_eq_top_of_isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : IsEmpty α
⊢ G.ediam ≤ HMul.hMul (α := ℕ∞) 2 ⊤

Tactic:
le_top

Premises used: le_top, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : IsEmpty α
⊢ G.ediam ≤ HMul.hMul (α := ℕ∞) 2 ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
pos : ∀ (hdiam : G.ediam = ⊤), G.ediam ≤ 2 * G.radius
neg : ∀ (hdiam : ¬G.ediam = ⊤), G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
by_cases hdiam : G.ediam = ⊤

Premises used: SimpleGraph.ediam
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
hdiam : G.ediam = ⊤
⊢ G.ediam ≤ 2 * G.radius

Tactic:
simp [hdiam, ediam_eq_top_iff_radius_eq_top.mp hdiam]

Premises used: SimpleGraph.ediam_eq_top_iff_radius_eq_top, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
hdiam : ¬G.ediam = ⊤
neg : ∀ (w : α) (hw : G.eccent w = G.radius), G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius

Premises used: SimpleGraph.exists_eccent_eq_radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
neg : ∀ (w w_1 : α) (h : G.edist w w_1 = G.ediam), G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top hdiam

Premises used: SimpleGraph.exists_edist_eq_ediam_of_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h_1 : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w_1 w_2 : α
h : G.edist w_1 w_2 = G.ediam
neg : G.edist w_1 w + G.edist w w_2 ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
apply le_trans (h ▸ G.edist_triangle (v := w))

Premises used: le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h_1 : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w_1 w_2 : α
h : G.edist w_1 w_2 = G.ediam
neg : G.edist w_1 w + G.edist w w_2 ≤ G.radius + G.radius
⊢ G.edist w_1 w + G.edist w w_2 ≤ 2 * G.radius

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h_1 : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w_1 w_2 : α
h : G.edist w_1 w_2 = G.ediam
⊢ G.edist w_1 w + G.edist w w_2 ≤ G.radius + G.radius

Tactic:
hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent

Premises used: add_le_add, Eq.rec, SimpleGraph.edist_le_eccent, SimpleGraph.edist_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h_1 : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w_1 w_2 : α
h : G.edist w_1 w_2 = G.ediam
⊢ G.edist w_1 w + G.edist w w_2 ≤ G.radius + G.radius

Tactic:
exact hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.radius = G.ediam ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

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

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
refine_1 : ∀ (h : G.radius = G.ediam), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
refine_2 : ∀ (h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e), G.radius = G.ediam
⊢ G.radius = G.ediam ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.radius = G.ediam
h₁ : ∀ (u : α), G.eccent u = G.radius
⊢ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

Tactic:
use G.radius

Premises used: SimpleGraph.radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.radius = G.ediam
u : α
⊢ G.eccent u = G.radius

Tactic:
le_antisymm (h ▸ eccent_le_ediam) radius_le_eccent

Premises used: le_antisymm, SimpleGraph.radius_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.radius = G.ediam
u : α
⊢ G.eccent u = G.radius

Tactic:
exact le_antisymm (h ▸ eccent_le_ediam) radius_le_eccent

Premises used: le_antisymm, SimpleGraph.radius_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
refine_2 : ∀ (e : ℕ∞) (h : ∀ (u : α), G.eccent u = e), G.radius = G.ediam
⊢ G.radius = G.ediam

Tactic:
obtain ⟨e, h⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
⊢ G.ediam = e

Tactic:
have ediam_eq : G.ediam = e :=
      le_antisymm (iSup_le fun u ↦ (h u).le) ((h Classical.ofNonempty) ▸ eccent_le_ediam)
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
refine_2 : G.radius = e
⊢ G.radius = G.ediam

Tactic:
rw [ediam_eq]
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = e

Tactic:
le_antisymm ((h Classical.ofNonempty) ▸ radius_le_eccent) (le_iInf fun u ↦ (h u).ge)

Premises used: Eq.ge, le_iInf, le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = e

Tactic:
exact le_antisymm ((h Classical.ofNonempty) ▸ radius_le_eccent) (le_iInf fun u ↦ (h u).ge)

Premises used: Eq.ge, le_iInf, le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inst : Nontrivial α
⊢ radius.{u_1} (α := α) ⊥ = ⊤

Tactic:
radius_eq_top_of_not_connected not_connected_bot

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

Tactic:
simp [radius]

Premises used: SimpleGraph.radius