awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₂ t₂) : 𝕜)

Tactic:
mod_cast edgeDensity_nonneg r _ _

Premises used: congrArg, cast, Rel.edgeDensity, Rat.cast, Rat.natCast_le_cast._simp_1, LE.le, congrFun', Nat.cast_zero, Eq.symm, Rel.edgeDensity_nonneg, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₂ t₂) : 𝕜)

Tactic:
exact mod_cast edgeDensity_nonneg r _ _

Premises used: Rel.edgeDensity_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜) 1
inr₁ : LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₁ t₁) : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₁ t₁) : 𝕜)| 1

Tactic:
rw [abs_of_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜) 1

Tactic:
mod_cast edgeDensity_le_one r _ _

Premises used: congrArg, cast, Rel.edgeDensity, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Rel.edgeDensity_le_one, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜) 1

Tactic:
exact mod_cast edgeDensity_le_one r _ _

Premises used: Rel.edgeDensity_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₁ t₁) : 𝕜)

Tactic:
mod_cast edgeDensity_nonneg r _ _

Premises used: congrArg, cast, Rel.edgeDensity, Rat.cast, Rat.natCast_le_cast._simp_1, LE.le, congrFun', Nat.cast_zero, Eq.symm, Rel.edgeDensity_nonneg, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₁ t₁) : 𝕜)

Tactic:
exact mod_cast edgeDensity_nonneg r _ _

Premises used: Rel.edgeDensity_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
rw : x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2
⊢ x.swap ∈ interedges r s t ↔ x ∈ interedges r t s

Tactic:
rw [mem_interedges_iff, mem_interedges_iff, hr.iff]

Premises used: Rel.mem_interedges_iff, Symmetric.iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Tactic:
and_left_comm

Premises used: Set.Mem, setOf, and_left_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Tactic:
exact and_left_comm

Premises used: and_left_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
s t : Finset α
a b : α
hr : Symmetric r
⊢ (a, b) ∈ interedges r s t ↔ (b, a) ∈ interedges r t s

Tactic:
@swap_mem_interedges_iff _ _ _ _ _ hr (b, a)

Premises used: Set.Mem, setOf, Prod.swap, Rel.swap_mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
⊢ #(interedges r s t) = #(interedges r t s)

Tactic:
Finset.card_bij (fun (x : α × α) _ ↦ x.swap) (fun _ ↦ (swap_mem_interedges_iff hr).2)
    (fun _ _ _ _ h ↦ Prod.swap_injective h) fun x h ↦
    ⟨x.swap, (swap_mem_interedges_iff hr).2 h, x.swap_swap⟩

Premises used: Iff.mpr, Prod.swap_swap, Finset.card_bij, Exists.intro, Prod.swap_injective, Prod.swap, Rel.swap_mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
rw : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = edgeDensity r t s
rw₁ : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
rw₂ : (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
rw₃ rw₄ :
  (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) =
    (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ)
⊢ edgeDensity r s t = edgeDensity r t s

Tactic:
rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]

Premises used: Rel.edgeDensity, mul_comm, Rel.card_interedges_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ G.interedges s t = {e ∈ s ×ˢ t | G.Adj e.1 e.2}

Tactic:
rfl

Premises used: Rel.interedges, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ G.edgeDensity s t = (↑(#(G.interedges s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
rfl

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ (↑(#(G.interedges s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = G.edgeDensity s t

Tactic:
rfl

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
x : α × α
⊢ x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2

Tactic:
Rel.mem_interedges_iff

Premises used: Set.Mem, setOf, Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
a b : α
⊢ (a, b) ∈ G.interedges s t ↔ a ∈ s ∧ b ∈ t ∧ G.Adj a b

Tactic:
Rel.mk_mem_interedges_iff

Premises used: Set.Mem, setOf, Rel.mk_mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
t : Finset α
⊢ G.interedges ∅ t = ∅

Tactic:
Rel.interedges_empty_left _

Premises used: Rel.interedges_empty_left, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s₁ s₂ t₁ t₂ : Finset α
⊢ s₂ ⊆ s₁ → t₂ ⊆ t₁ → G.interedges s₂ t₂ ⊆ G.interedges s₁ t₁

Tactic:
Rel.interedges_mono

Premises used: Set.Mem, setOf, Rel.interedges_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s₁ s₂ : Finset α
hs : Disjoint s₁ s₂
t : Finset α
⊢ Disjoint (G.interedges s₁ t) (G.interedges s₂ t)

Tactic:
Rel.interedges_disjoint_left _ hs _

Premises used: Rel.interedges_disjoint_left, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
t₁ t₂ s : Finset α
ht : Disjoint t₁ t₂
⊢ Disjoint (G.interedges s t₁) (G.interedges s t₂)

Tactic:
Rel.interedges_disjoint_right _ _ ht

Premises used: Rel.interedges_disjoint_right, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
inst_1 : DecidableEq α
s : Finset ι
t : Finset α
f : ι → Finset α
⊢ G.interedges (s.biUnion f) t = s.biUnion fun (a : ι) ↦ G.interedges (f a) t

Tactic:
Rel.interedges_biUnion_left _ _ _ _

Premises used: Rel.interedges_biUnion_left, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
inst_1 : DecidableEq α
s : Finset α
t : Finset ι
f : ι → Finset α
⊢ G.interedges s (t.biUnion f) = t.biUnion fun (b : ι) ↦ G.interedges s (f b)

Tactic:
Rel.interedges_biUnion_right _ _ _ _

Premises used: Rel.interedges_biUnion_right, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
κ : Type u_3
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
inst_1 : DecidableEq α
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset α
⊢ G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) ↦ G.interedges (f ab.1) (g ab.2)

Tactic:
Rel.interedges_biUnion _ _ _ _ _

Premises used: Rel.interedges_biUnion, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
rw : #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2}) = #(s ×ˢ t)
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Tactic:
rw [← card_product, interedges_def, interedges_def]

Premises used: Finset.card_product, SimpleGraph.interedges_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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}

Tactic:
filter_congr fun x hx ↦ ?_

Premises used: Finset.filter_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
refine : ∀ (x : α × α) (hx : x ∈ s ×ˢ t), Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
⊢ {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}

Tactic:
refine filter_congr fun x hx ↦ ?_

Premises used: Finset.filter_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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
⊢ x.1 ∈ s ∧ x.2 ∈ t

Tactic:
rw [mem_product] at hx

Premises used: Finset.mem_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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
rw₁ rw₂ : ¬G.Adj x.1 x.2 ↔ ¬G.Adj 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)]

Premises used: SimpleGraph.compl_adj, and_iff_right, Disjoint.forall_ne_finset, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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}

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)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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}
rw : Disjoint ({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)

Tactic:
rw [this, ← card_union_of_disjoint, filter_union_filter_not_eq]

Premises used: Finset.filter_union_filter_not_eq, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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}
⊢ Disjoint ({e ∈ s ×ˢ t | G.Adj e.1 e.2}) ({e ∈ s ×ˢ t | ¬G.Adj e.1 e.2})

Tactic:
disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Premises used: Iff.mpr, Classical.not_not, Finset.disjoint_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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}
⊢ Disjoint ({e ∈ s ×ˢ t | G.Adj e.1 e.2}) ({e ∈ s ×ˢ t | ¬G.Adj e.1 e.2})

Tactic:
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Premises used: Iff.mpr, Classical.not_not, Finset.disjoint_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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) : ℚ)
rw₁ : HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Tactic:
rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]

Premises used: SimpleGraph.edgeDensity_def, div_eq_one_iff_eq, add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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
⊢ HAdd.hAdd (α := ℚ) (↑(#(G.interedges s t)) : ℚ) (↑(#(Gᶜ.interedges s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
mod_cast card_interedges_add_card_interedges_compl _ h

Premises used: Nat.cast_mul._simp_1, SimpleGraph.card_interedges_add_card_interedges_compl, congrArg, Compl.compl, Nat.cast_add._simp_1, cast, congr, Finset.card, Nat.cast_inj._simp_1, Eq.symm, Eq, Eq.trans, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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
⊢ HAdd.hAdd (α := ℚ) (↑(#(G.interedges s t)) : ℚ) (↑(#(Gᶜ.interedges s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
exact mod_cast card_interedges_add_card_interedges_compl _ h

Premises used: SimpleGraph.card_interedges_add_card_interedges_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
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
⊢ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ #(G.interedges s t) ≤ #s * #t

Tactic:
Rel.card_interedges_le_mul _ _ _

Premises used: Rel.card_interedges_le_mul, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ 0 ≤ G.edgeDensity s t

Tactic:
Rel.edgeDensity_nonneg _ _ _

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ G.edgeDensity s t ≤ 1

Tactic:
Rel.edgeDensity_le_one _ _ _

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
t : Finset α
⊢ G.edgeDensity ∅ t = 0

Tactic:
Rel.edgeDensity_empty_left _ _

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity_empty_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s : Finset α
⊢ G.edgeDensity s ∅ = 0

Tactic:
Rel.edgeDensity_empty_right _ _

Premises used: Rel.edgeDensity_empty_right, SimpleGraph.edgeDensity
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
x : α × α
⊢ x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s

Tactic:
Rel.swap_mem_interedges_iff G.symm

Premises used: Set.Mem, setOf, SimpleGraph.symm, Rel.swap_mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
a b : α
⊢ (a, b) ∈ G.interedges s t ↔ (b, a) ∈ G.interedges t s

Tactic:
Rel.mk_mem_interedges_comm G.symm

Premises used: Rel.mk_mem_interedges_comm, Set.Mem, setOf, SimpleGraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
⊢ G.edgeDensity s t = G.edgeDensity t s

Tactic:
Rel.edgeDensity_comm G.symm s t

Premises used: SimpleGraph.edgeDensity, Rel.edgeDensity_comm, SimpleGraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.eccent = fun (u : α) ↦ ⨆ (v : α), G.edist u v

Tactic:
rfl

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

Tactic:
le_iSup (G.edist u) v

Premises used: le_iSup, SimpleGraph.edist, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Finite α
u : α
⊢ ∃ (v : α), G.edist u v = G.eccent u

Tactic:
have : Nonempty α := Nonempty.intro u
  exists_eq_ciSup_of_finite

Premises used: Nonempty.intro, exists_eq_ciSup_of_finite, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
u : α
rw : ∀ (h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w) (u : α), G.eccent u = ⊤
⊢ G.eccent u = ⊤

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 α
h : ¬∃ (v : α), ∀ (w : α), G.Reachable v w
u : α
⊢ ∀ (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 α
u : α
h : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
obtain : ∀ (v : α) (h : ¬G.Reachable u v), G.eccent u = ⊤
⊢ G.eccent u = ⊤

Tactic:
obtain ⟨v, h⟩ := h u
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h_1 : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
rw : G.edist u v ≤ G.eccent u
⊢ G.eccent u = ⊤

Tactic:
rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]

Premises used: eq_top_iff, SimpleGraph.edist_eq_top_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h_1 : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.edist u v ≤ G.eccent u

Tactic:
le_iSup (G.edist u) v

Premises used: le_iSup, SimpleGraph.edist, SimpleGraph.eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h_1 : ∀ (v : α), ∃ (w : α), ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.edist u v ≤ G.eccent u

Tactic:
exact le_iSup (G.edist u) v

Premises used: le_iSup, SimpleGraph.edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
u : α
⊢ G.eccent u = 0

Tactic:
simpa [eccent, edist_eq_zero_iff] using subsingleton_iff.mp ‹_› u

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

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

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

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

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

Premises used: 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 : α), u = i
⊢ v = u

Tactic:
(huv v).symm

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

Tactic:
exact (huv v).symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u = 0 ↔ Subsingleton α

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

Premises used: Iff.intro, SimpleGraph.eccent_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
refine : ∀ (h : G.eccent u = 0), Subsingleton α
⊢ G.eccent u = 0 ↔ Subsingleton α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ eccent_eq_zero_of_subsingleton u⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u = 0
contrapose! : ∀ (h : Nontrivial α), G.eccent u ≠ 0
⊢ Subsingleton α

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
h : Nontrivial α
⊢ 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 α
u : α
h : Nontrivial α
⊢ 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 : α
rw : G.eccent u ≠ 0 ↔ Nontrivial α
rw₁ : G.eccent u ≠ 0 ↔ ¬Subsingleton α
rw₂ : G.eccent u ≠ 0 ↔ ¬G.eccent u = 0
rw₃ : α
rw₄ : SimpleGraph α
rw₅ : G.eccent u ≠ 0 ↔ ¬G.eccent u = 0
rw₆ : α
rw₇ : SimpleGraph α
⊢ 0 < G.eccent u ↔ Nontrivial α

Tactic:
rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]

Premises used: SimpleGraph.eccent_eq_zero_iff, not_subsingleton_iff_nontrivial, pos_iff_ne_zero