awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
⊢ {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
have refine : ∀ (x : α × α) (hx : x ∈ s ×ˢ t), Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
Tactic: refine filter_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
have hx₁ : x.1 ∈ s ∧ x.2 ∈ t
Tactic: rw [mem_product] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.1 ∈ s ∧ x.2 ∈ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
have rw : x.1 ≠ x.2 ∧ ¬G.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
Tactic: rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.1 ∈ s ∧ x.2 ∈ t
rw : x.1 ≠ x.2 ∧ ¬G.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
have rw₁ : ¬G.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
Tactic: rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2}) = #(s ×ˢ t)
have this : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
Tactic: have : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2} := by
    refine filter_congr fun x hx ↦ ?_
    rw [mem_product] at hx
    rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
this : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2}) = #(s ×ˢ t)
have rw : Disjoint ({e ∈ s ×ˢ t | G.Adj e.1 e.2}) ({e ∈ s ×ˢ t | ¬G.Adj e.1 e.2})
Tactic: rw [this, ← card_union_of_disjoint, filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1
have rw : HAdd.hAdd (α := ℚ) (↑(#(G.interedges s t)) : ℚ) (↑(#(Gᶜ.interedges s t)) : ℚ) =
  HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
Tactic: rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
rw :
  HAdd.hAdd (α := ℚ) (↑(#(G.interedges s t)) : ℚ) (↑(#(Gᶜ.interedges s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1
have rw₁ : HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0
Tactic: rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
u : α
⊢ G.eccent u = ⊤
have rw : ∀ (h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w) (u : α), G.eccent u = ⊤
Tactic: rw [connected_iff_exists_forall_reachable] at h
Cleared hypotheses: h, u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w
u : α
⊢ G.eccent u = ⊤
have h₁ : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
⊢ G.eccent u = ⊤
have obtain : ∀ (v : α) (h : ¬G.Reachable u v), G.eccent u = ⊤
Tactic: obtain ⟨v, h⟩ := h u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h_1 : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.eccent u = ⊤
have rw : G.edist u v ≤ G.eccent u
Tactic: rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
⊢ G.eccent u ≠ 0
have obtain : ∀ (v : α) (huv : v ≠ u), G.eccent u ≠ 0
Tactic: obtain ⟨v, huv⟩ := exists_ne ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : v ≠ u
⊢ G.eccent u ≠ 0
have contrapose : ∀ (huv : G.eccent u = 0), v = u
Tactic: contrapose huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : G.eccent u = 0
⊢ v = u
have huv₁ : ∀ (i : α), u = i
Tactic: simp only [eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u = 0 ↔ Subsingleton α
have refine : ∀ (h : G.eccent u = 0), Subsingleton α
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ eccent_eq_zero_of_subsingleton u⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u = 0
⊢ Subsingleton α
have contrapose! : ∀ (h : Nontrivial α), G.eccent u ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ 0 < G.eccent u ↔ Nontrivial α
have rw : G.eccent u ≠ 0 ↔ Nontrivial α
Tactic: rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
rw : G.eccent u ≠ 0 ↔ Nontrivial α
⊢ 0 < G.eccent u ↔ Nontrivial α
have rw₁ : G.eccent u ≠ 0 ↔ ¬Subsingleton α
Tactic: rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
rw : G.eccent u ≠ 0 ↔ Nontrivial α
rw₁ : G.eccent u ≠ 0 ↔ ¬Subsingleton α
⊢ 0 < G.eccent u ↔ Nontrivial α
have rw₂ : G.eccent u ≠ 0 ↔ ¬G.eccent u = 0
Tactic: rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
u : α
⊢ eccent ⊤ u = 1
have apply : eccent ⊤ u ≤ 1
Tactic: apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
u : α
⊢ eccent ⊤ u ≤ 1
have rw : ∀ (i : α), edist ⊤ u i ≤ 1
Tactic: rw [eccent, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
u v : α
⊢ edist ⊤ u v ≤ 1
have inl : u = v → edist ⊤ u v ≤ 1
Tactic: cases eq_or_ne u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
inst : Nontrivial α
u v : α
inl : u = v → edist ⊤ u v ≤ 1
⊢ edist ⊤ u v ≤ 1
have inr : u ≠ v → edist ⊤ u v ≤ 1
Tactic: cases eq_or_ne u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G = ⊤ ↔ ∀ (u : α), G.eccent u = 1
have refine : ∀ (h : ∀ (u : α), G.eccent u = 1), G = ⊤
Tactic: refine ⟨fun h ↦ h ▸ eccent_top, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
⊢ G = ⊤
have Adj : ∀ (u v : α), G.Adj u v ↔ Adj ⊤ u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
⊢ G.Adj u v ↔ Adj ⊤ u v
have Adj : ∀ (huv : Adj ⊤ u v), G.Adj u v
Tactic: refine ⟨Adj.ne, fun huv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : Adj ⊤ u v
⊢ G.Adj u v
have Adj : G.edist u v = 1
Tactic: rw [← edist_eq_one_iff_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : Adj ⊤ u v
⊢ G.edist u v = 1
have Adj : 1 ≤ G.edist u v
Tactic: apply le_antisymm ((h u).symm ▸ edist_le_eccent)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : Adj ⊤ u v
⊢ 1 ≤ G.edist u v
have Adj : u ≠ v
Tactic: rw [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
have mp : G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
mp : G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
have mpr : (∀ (v : α), u ≠ v → G.Adj u v) → G.eccent u ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
⊢ G.Adj u v
have hd : G.edist u v ≤ 1
Tactic: have hd : G.edist u v ≤ 1 := edist_le_eccent.trans h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
hd : G.edist u v ≤ 1
⊢ G.Adj u v
have hd' : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
⊢ G.eccent u ≤ 1
have mpr : ∀ (v : α), G.edist u v ≤ 1
Tactic: rw [eccent_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.edist u v ≤ 1
have mpr : G.Adj u v ∨ u = v
Tactic: rw [edist_le_one_iff_adj_or_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u : α
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
have h : 1 ≤ G.eccent u
Tactic: have h : 1 ≤ G.eccent u := ENat.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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
have rw : G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
Tactic: rw [← h.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ (p : α × α), G.edist p.1 p.2
have rw : Eq (α := ℕ∞) (⨆ (u : α), G.eccent u) (⨆ (p : α × α), G.edist p.1 p.2)
Tactic: rw [ediam, eccent_def, iSup_prod]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
rw : Eq (α := ℕ∞) (⨆ (u : α), G.eccent u) (⨆ (p : α × α), G.edist p.1 p.2)
⊢ G.ediam = ⨆ (p : α × α), G.edist p.1 p.2
have rw₁ : Eq (α := ℕ∞) (⨆ (u : α), (fun (u : α) ↦ (⨆ (v : α), G.edist u v : ℕ∞)) u) (⨆ (p : α × α), G.edist p.1 p.2)
Tactic: rw [ediam, eccent_def, iSup_prod]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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)
⊢ G.ediam = ⨆ (p : α × α), G.edist p.1 p.2
have rw₂ : Eq (α := ℕ∞) (⨆ (u : α), (fun (u : α) ↦ (⨆ (v : α), G.edist u v : ℕ∞)) u)
  (⨆ (i : α), ⨆ (j : α), G.edist (i, j).1 (i, j).2)
Tactic: rw [ediam, eccent_def, iSup_prod]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ 0
⊢ Nontrivial α
have contrapose! : ∀ (h : Subsingleton α), G.ediam = 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.ediam ≠ 0
have obtain : ∀ (u v : α) (huv : u ≠ v), G.ediam ≠ 0
Tactic: obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : u ≠ v
⊢ G.ediam ≠ 0
have contrapose : ∀ (huv : G.ediam = 0), u = v
Tactic: contrapose huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
u v : α
huv : G.ediam = 0
⊢ u = v
have huv₁ : ∀ (i i_1 : α), i = i_1
Tactic: simp only [ediam, eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ Subsingleton α
have contrapose! : ∀ (h : Nontrivial α), G.ediam ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.Connected
⊢ G.ediam = ⊤
have h₁ : ¬∃ (v : α), ∀ (w : α), G.Reachable v w
Tactic: rw [connected_iff_exists_forall_reachable] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w
⊢ G.ediam = ⊤
have h₁ : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
⊢ G.ediam = ⊤
have obtain : ∀ (w : α) (hw : ¬G.Reachable Classical.ofNonempty w), G.ediam = ⊤
Tactic: obtain ⟨_, hw⟩ := h Classical.ofNonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
w : α
hw : ¬G.Reachable Classical.ofNonempty w
⊢ G.ediam = ⊤
have rw : G.edist Classical.ofNonempty w ≤ G.ediam
Tactic: rw [eq_top_iff, ← edist_eq_top_of_not_reachable hw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
⊢ G.ediam = ⊤
have inl : IsEmpty α → G.ediam = ⊤
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
inl : IsEmpty α → G.ediam = ⊤
⊢ G.ediam = ⊤
have inr : Nonempty α → G.ediam = ⊤
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : IsEmpty α
⊢ G.ediam = ⊤
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
⊢ G.ediam = ⊤
have inr : ¬G.Connected
Tactic: apply ediam_eq_top_of_not_connected
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
⊢ ¬G.Connected
have inr : ¬(G.Preconnected ∧ Nonempty α)
Tactic: rw [connected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h_1 : Nonempty α
⊢ ¬(G.Preconnected ∧ Nonempty α)
have inr : G.Preconnected → Nonempty α → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤
have refine : ∀ (h : G.ediam = 1), G = ⊤
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
⊢ G = ⊤
have rw : ∀ (u : α), G.eccent u = 1
Tactic: rw [eq_top_iff_forall_eccent_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
⊢ G.eccent u = 1
have apply : 1 ≤ G.eccent u
Tactic: apply le_antisymm (h ▸ eccent_le_ediam)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nontrivial α
h : G.ediam = 1
u : α
⊢ 1 ≤ G.eccent u
have rw : G.eccent u ≠ 0
Tactic: rw [Order.one_le_iff_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.ediam ≤ 2 * G.eccent u
have refine : ∀ (v w : α), G.edist v w ≤ 2 * G.eccent u
Tactic: refine ediam_le_of_edist_le fun v w ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v u + G.edist u w = G.edist u v + G.edist u w
have rw : G.edist u v + G.edist u w = G.edist u v + G.edist u w
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v w ≤ 2 * G.eccent u
have v₁ : G.edist v u + G.edist u w = G.edist u v + G.edist u w
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.diam = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
have rw : G.ediam.toNat = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
Tactic: rw [diam, ediam_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
rw : G.ediam.toNat = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
⊢ G.diam = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
have rw₁ : ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2) = ENat.toNat (⨆ (p : α × α), G.edist p.1 p.2)
Tactic: rw [diam, ediam_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ Nontrivial α
have contrapose! : ∀ (h : Subsingleton α), G.diam = 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.Connected
⊢ G.diam = 0
have inl : IsEmpty α → G.diam = 0
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
inl : IsEmpty α → G.diam = 0
⊢ G.diam = 0
have inr : Nonempty α → G.diam = 0
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : IsEmpty α
⊢ G.diam = 0
have inl : ENat.toNat 0 = 0
Tactic: rw [diam, ediam, ciSup_of_empty, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : Nonempty α
⊢ G.diam = 0
have inr : G.ediam.toNat = 0
Tactic: rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : Nonempty α
inr : G.ediam.toNat = 0
⊢ G.diam = 0
have inr₁ : ENat.toNat ⊤ = 0
Tactic: rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h_1 : Nonempty α
inr : G.ediam.toNat = 0
inr₁ : ENat.toNat ⊤ = 0
⊢ G.diam = 0
have inr₂ : Eq (α := ℕ) 0 0
Tactic: rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ G.diam = 0
have rw : G.ediam.toNat = 0
Tactic: rw [diam, h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
rw : G.ediam.toNat = 0
⊢ G.diam = 0
have rw₁ : ENat.toNat ⊤ = 0
Tactic: rw [diam, h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
rw : G.ediam.toNat = 0
rw₁ : ENat.toNat ⊤ = 0
⊢ G.diam = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [diam, h, ENat.toNat_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam
have pos : ∀ (h : G.diam = 0), ∃ (u : α) (v : α), G.dist u v = G.diam
Tactic: by_cases h : G.diam = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
pos : ∀ (h : G.diam = 0), ∃ (u : α) (v : α), G.dist u v = G.diam
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam
have neg : ∀ (h : ¬G.diam = 0), ∃ (u : α) (v : α), G.dist u v = G.diam
Tactic: by_cases h : G.diam = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam
have neg : ∀ (u v : α) (huv : G.edist u v = G.ediam), ∃ (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ ∃ (u : α) (v : α), G.dist u v = G.diam
have h₁ : G.dist u v = G.diam
Tactic: use u, v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.diam
have h₁ : G.dist u v = G.ediam.toNat
Tactic: rw [diam, dist, congrArg ENat.toNat huv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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
⊢ G.dist u v = G.diam
have h₂ : (G.edist u v).toNat = G.ediam.toNat
Tactic: rw [diam, dist, congrArg ENat.toNat huv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
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
⊢ G.dist u v = G.diam
have h₃ : G.ediam.toNat = G.ediam.toNat
Tactic: rw [diam, dist, congrArg ENat.toNat huv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
⊢ diam.{u_1} (α := α) ⊥ = 0
have rw : ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
Tactic: rw [diam, ENat.toNat_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Diam (goal)
Goal:
α : Type u_1
⊢ ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
have inl : Subsingleton α → ediam.{u_1} (α := α) ⊥ = 0 ∨ ediam.{u_1} (α := α) ⊥ = ⊤
Tactic: cases subsingleton_or_nontrivial α