awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inl : Subsingleton α → ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
have inr : Nontrivial α → ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
⊢ diam.{u_1} (α := α) ⊤ = 1
have rw : (ediam.{u_1} (α := α) ⊤).toNat = 1
Tactic: rw [diam, ediam_top, ENat.toNat_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
rw : (ediam.{u_1} (α := α) ⊤).toNat = 1
⊢ diam.{u_1} (α := α) ⊤ = 1
have rw₁ : ENat.toNat 1 = 1
Tactic: rw [diam, ediam_top, ENat.toNat_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
rw : (ediam.{u_1} (α := α) ⊤).toNat = 1
rw₁ : ENat.toNat 1 = 1
⊢ diam.{u_1} (α := α) ⊤ = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [diam, ediam_top, ENat.toNat_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
have rw : G.ediam.toNat = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
Tactic: rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
rw : G.ediam.toNat = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
have rw₁ : G.ediam = 0 ∨ G.ediam = ⊤ ↔ G.ediam = ⊤ ∨ Subsingleton α
Tactic: rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
rw : G.ediam.toNat = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
rw₁ : G.ediam = 0 ∨ G.ediam = ⊤ ↔ G.ediam = ⊤ ∨ Subsingleton α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
have rw₂ : G.ediam = ⊤ ∨ G.ediam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
Tactic: rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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 α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
have rw₃ : G.ediam = ⊤ ∨ Subsingleton α ↔ G.ediam = ⊤ ∨ Subsingleton α
Tactic: rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.diam = 1 ↔ G = ⊤
have rw : G.ediam.toNat = 1 ↔ G = ⊤
Tactic: rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : G.ediam.toNat = 1 ↔ G = ⊤
⊢ G.diam = 1 ↔ G = ⊤
have rw₁ : G.ediam = (↑1 : ℕ∞) ↔ G = ⊤
Tactic: rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : G.ediam.toNat = 1 ↔ G = ⊤
rw₁ : G.ediam = (↑1 : ℕ∞) ↔ G = ⊤
⊢ G.diam = 1 ↔ G = ⊤
have rw₂ : G.ediam = 1 ↔ G = ⊤
Tactic: rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
rw : G.ediam.toNat = 1 ↔ G = ⊤
rw₁ : G.ediam = (↑1 : ℕ∞) ↔ G = ⊤
rw₂ : G.ediam = 1 ↔ G = ⊤
⊢ G.diam = 1 ↔ G = ⊤
have rw₃ : G = ⊤ ↔ G = ⊤
Tactic: rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.diam = 0 ↔ G.ediam = ⊤
have rw : ¬G.diam = 0 ↔ ¬G.ediam = ⊤
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Finite α
inst_1 : Nontrivial α
⊢ G.Connected ↔ G.diam ≠ 0
have rw : G.ediam ≠ ⊤ ↔ G.diam ≠ 0
Tactic: rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Finite α
inst_1 : Nontrivial α
rw : G.ediam ≠ ⊤ ↔ G.diam ≠ 0
⊢ G.Connected ↔ G.diam ≠ 0
have rw₁ : G.ediam = ⊤ ↔ G.diam = 0
Tactic: rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Finite α
inst_1 : Nontrivial α
rw : G.ediam ≠ ⊤ ↔ G.diam ≠ 0
rw₁ : G.ediam = ⊤ ↔ G.diam = 0
⊢ G.Connected ↔ G.diam ≠ 0
have rw₂ : G.ediam = ⊤ ↔ G.ediam = ⊤
Tactic: rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius
have obtain : ∀ (w : α) (hw : G.eccent w = G.radius), ∃ (u : α) (v : α), G.edist u v = G.radius
Tactic: obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
w : α
hw : G.eccent w = G.radius
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius
have obtain : ∀ (v : α) (hv : G.edist w v = G.eccent w), ∃ (u : α) (v : α), G.edist u v = G.radius
Tactic: obtain ⟨v, hv⟩ := G.exists_edist_eq_eccent_of_finite w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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
⊢ ∃ (u : α) (v : α), G.edist u v = G.radius
have h : G.edist w v = G.radius
Tactic: use w, v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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
⊢ G.edist w v = G.radius
have h₁ : G.radius = G.radius
Tactic: rw [hv, hw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
⊢ G.radius ≠ ⊤ ↔ G.Connected
have refine : ∀ (h : G.Connected), G.radius ≠ ⊤
Tactic: refine ⟨Not.imp_symm radius_eq_top_of_not_connected, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
⊢ G.radius ≠ ⊤
have obtain : ∀ (u v : α) (huv : G.edist u v = G.radius), G.radius ≠ ⊤
Tactic: obtain ⟨u, v, huv⟩ := G.exists_edist_eq_radius_of_finite
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
inst_1 : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
⊢ G.radius ≠ ⊤
have rw : G.Reachable u v
Tactic: rw [← huv, edist_ne_top_iff_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.radius ≠ 0
have rw : 1 ≤ G.radius
Tactic: rw [← ENat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ 1 ≤ G.radius
have h : ∀ (i : α), 1 ≤ G.eccent i
Tactic: apply le_iInf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α
have refine_1 : ∀ (h : G.radius = 0), Nonempty α
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
refine_1 : ∀ (h : G.radius = 0), Nonempty α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α
have refine_2 : ∀ (h : G.radius = 0), Subsingleton α
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
refine_1 : ∀ (h : G.radius = 0), Nonempty α
refine_2 : ∀ (h : G.radius = 0), Subsingleton α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α
have refine_3 : Nonempty α ∧ Subsingleton α → Nonempty α → Subsingleton α → G.radius = 0
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
⊢ Nonempty α
have refine_1 : ∀ (h : IsEmpty α), G.radius ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
⊢ Subsingleton α
have refine_2 : ∀ (h : Nontrivial α), G.radius ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α ∧ Subsingleton α
left : Nonempty α
right : Subsingleton α
⊢ G.radius = 0
have refine_3 : ∃ (i : α), G.eccent i = 0
Tactic: rw [radius, ENat.iInf_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α ∧ Subsingleton α
left : Nonempty α
right : Subsingleton α
⊢ ∃ (i : α), G.eccent i = 0
have h : G.eccent Classical.ofNonempty = 0
Tactic: use Classical.ofNonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.ediam = ⊤ ↔ G.radius = ⊤
have refine : G.ediam = ⊤ → G.radius = ⊤
Tactic: refine ⟨?_, fun hr ↦ eq_top_iff.mpr (hr ▸ radius_le_ediam)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.ediam = ⊤ → G.radius = ⊤
have contrapose : ¬G.radius = ⊤ → ¬G.ediam = ⊤
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
⊢ ¬G.ediam = ⊤
have obtain : ∀ (w : α) (hw : G.eccent w = G.radius), ¬G.ediam = ⊤
Tactic: obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
⊢ ¬G.ediam = ⊤
have hdiam : G.ediam ≤ 2 * G.eccent w
Tactic: have hdiam : G.ediam ≤ 2 * G.eccent w := ediam_le_two_mul_eccent w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam ≤ 2 * G.radius
have inl : IsEmpty α → G.ediam ≤ 2 * G.radius
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inl : IsEmpty α → G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius
have inr : Nonempty α → G.ediam ≤ 2 * G.radius
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : IsEmpty α
⊢ G.ediam ≤ 2 * G.radius
have inl : G.ediam ≤ HMul.hMul (α := ℕ∞) 2 ⊤
Tactic: rw [radius_eq_top_of_isEmpty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
⊢ G.ediam ≤ 2 * G.radius
have pos : ∀ (hdiam : G.ediam = ⊤), G.ediam ≤ 2 * G.radius
Tactic: by_cases hdiam : G.ediam = ⊤
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
pos : ∀ (hdiam : G.ediam = ⊤), G.ediam ≤ 2 * G.radius
⊢ G.ediam ≤ 2 * G.radius
have neg : ∀ (hdiam : ¬G.ediam = ⊤), G.ediam ≤ 2 * G.radius
Tactic: by_cases hdiam : G.ediam = ⊤
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
hdiam : ¬G.ediam = ⊤
⊢ G.ediam ≤ 2 * G.radius
have neg : ∀ (w : α) (hw : G.eccent w = G.radius), G.ediam ≤ 2 * G.radius
Tactic: obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
⊢ G.ediam ≤ 2 * G.radius
have neg : ∀ (w w_1 : α) (h : G.edist w w_1 = G.ediam), G.ediam ≤ 2 * G.radius
Tactic: obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top hdiam
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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.ediam ≤ 2 * G.radius
have neg : G.edist w_1 w + G.edist w w_2 ≤ 2 * G.radius
Tactic: apply le_trans (h ▸ G.edist_triangle (v := w))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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 ≤ 2 * G.radius
have neg : G.edist w_1 w + G.edist w w_2 ≤ G.radius + G.radius
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.radius = G.ediam ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have refine_1 : ∀ (h : G.radius = G.ediam), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
refine_1 : ∀ (h : G.radius = G.ediam), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
⊢ G.radius = G.ediam ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have refine_2 : ∀ (h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e), G.radius = G.ediam
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : G.radius = G.ediam
⊢ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have h₁ : ∀ (u : α), G.eccent u = G.radius
Tactic: use G.radius
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
⊢ G.radius = G.ediam
have refine_2 : ∀ (e : ℕ∞) (h : ∀ (u : α), G.eccent u = e), G.radius = G.ediam
Tactic: obtain ⟨e, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
⊢ G.radius = G.ediam
have ediam_eq : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = G.ediam
have refine_2 : G.radius = e
Tactic: rw [ediam_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.center = Set.univ ↔ G.radius = G.ediam
have rw : Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
Tactic: rw [radius_eq_ediam_iff, ← Set.univ_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have refine_1 : ∀ (h : Set.univ ⊆ G.center), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
refine_1 : ∀ (h : Set.univ ⊆ G.center), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
⊢ Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have refine_2 : ∀ (h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e), Set.univ ⊆ G.center
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
have h₁ : ∀ (u : α), G.eccent u = G.radius
Tactic: use G.radius
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
⊢ Set.univ ⊆ G.center
have refine_2 : ∀ (e : ℕ∞) (h : ∀ (u : α), G.eccent u = e), Set.univ ⊆ G.center
Tactic: obtain ⟨e, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : Membership.mem (γ := Set α) Set.univ u
⊢ u ∈ G.center
have refine_2 : e = G.radius
Tactic: rw [mem_center_iff, h u]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
⊢ G.center = Set.univ
have rw : ∀ (x : α), x ∈ G.center
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
u : α
⊢ u ∈ G.center
have rw : Nonempty α ∧ Subsingleton α
Tactic: rw [mem_center_iff, eccent_eq_zero_of_subsingleton u, eq_comm, radius_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
u : α
⊢ Nonempty α ∧ Subsingleton α
have left : Nonempty α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
have inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
have inr : Nontrivial α → Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
have inr : ∀ (x : α), Membership.mem (γ := Set α) (center ⊥) x
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
⊢ Membership.mem (γ := Set α) (center ⊥) u
have inr : eccent ⊥ u = radius.{u_1} (α := α) ⊥
Tactic: rw [mem_center_iff, eccent_bot, radius_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊥ u = radius.{u_1} (α := α) ⊥
⊢ Membership.mem (γ := Set α) (center ⊥) u
have inr₁ : ⊤ = radius.{u_1} (α := α) ⊥
Tactic: rw [mem_center_iff, eccent_bot, radius_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊥ u = radius.{u_1} (α := α) ⊥
inr₁ : ⊤ = radius.{u_1} (α := α) ⊥
⊢ Membership.mem (γ := Set α) (center ⊥) u
have inr₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [mem_center_iff, eccent_bot, radius_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
have inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
have inr : Nontrivial α → Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
have inr : ∀ (x : α), Membership.mem (γ := Set α) (center ⊤) x
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
⊢ Membership.mem (γ := Set α) (center ⊤) u
have inr : eccent ⊤ u = radius.{u_1} (α := α) ⊤
Tactic: rw [mem_center_iff, eccent_top, radius_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊤ u = radius.{u_1} (α := α) ⊤
⊢ Membership.mem (γ := Set α) (center ⊤) u
have inr₁ : 1 = radius.{u_1} (α := α) ⊤
Tactic: rw [mem_center_iff, eccent_top, radius_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊤ u = radius.{u_1} (α := α) ⊤
inr₁ : 1 = radius.{u_1} (α := α) ⊤
⊢ Membership.mem (γ := Set α) (center ⊤) u
have inr₂ : Eq (α := ℕ∞) 1 1
Tactic: rw [mem_center_iff, eccent_top, radius_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
⊢ Function.Injective.{u + 1, u + 1} (α := G.ComponentCompl K) (supp (K := K))
have refine : ∀ (v w : (↑Kᶜ : Type u)),
  supp (K := K) ((induce Kᶜ G).connectedComponentMk v) = supp (K := K) ((induce Kᶜ G).connectedComponentMk w) →
    (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w
Tactic: refine ConnectedComponent.ind₂ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  supp (K := K) ((induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) =
    supp (K := K) ((induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw))
⊢ (induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) =
    (induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)
have simp : ∀
  (h :
    ∀ (x : V),
      (∃ (h : x ∉ K),
          (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x sorry)
            (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) ↔
        ∃ (h : x ∉ K),
          (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x sorry)
            (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)),
  (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)
Tactic: simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ G.componentComplMk (K := K) vK = G.componentComplMk (K := K) wK
have rw : (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)
Tactic: rw [ConnectedComponent.eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)
have h : (induce Kᶜ G).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)
Tactic: apply Adj.reachable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w : (↑Kᶜ : Type u)
p : (induce Kᶜ G).Walk v w
⊢ p.IsPath → Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)
have nil : ∀ {u : (↑Kᶜ : Type u)},
  Walk.IsPath.{u} (V := (↑Kᶜ : Type u)) (G := induce Kᶜ G) (u := u) Walk.nil →
    Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) u)
Tactic: induction p with
    | nil => rintro _; rfl
    | cons a q ih => rename_i u v w; rintro h'; exact (h u.prop v.prop a).trans (ih h'.of_cons)
Cleared hypotheses: p