awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
rw : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t

Tactic:
rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_not_eq]

Premises used: Rel.interedges, Finset.card_product, Finset.filter_union_filter_not_eq, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r 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
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r 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
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
rw : #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #(s ×ˢ t)
rw₁ : #({e ∈ s ×ˢ t | r e.1 e.2}) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #(s ×ˢ t)
rw₂ : #({e ∈ s ×ˢ t | r e.1 e.2}) + #({e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(s ×ˢ t)
rw₃ : #({e ∈ s ×ˢ t | r e.1 e.2} ∪ {e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(s ×ˢ t)
rw₄ : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
rw₅ : #(s ×ˢ t) = #(s ×ˢ t)
rw₆ : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
rw₇ : #(s ×ˢ t) = #(s ×ˢ t)
rw₈ rw₉ : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t

Tactic:
classical
  rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_not_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Premises used: Iff.mpr, Rel.interedges, Classical.not_not, Finset.card_product, Finset.disjoint_filter, Finset.filter_union_filter_not_eq, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : Disjoint s s'
t : Finset β
rw : ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s') (t : Finset β) ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t
⊢ Disjoint (interedges r s t) (interedges r s' t)

Tactic:
rw [Finset.disjoint_left] at hs ⊢

Premises used: Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a : α × β
hx : a ∈ interedges r s t
hy : a ∈ interedges r s' t
⊢ a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2

Tactic:
rw [mem_interedges_iff] at hx hy

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a : α × β
hx : a ∈ interedges r s t
hy : a ∈ interedges r s' t
hx₁ : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
⊢ a.1 ∈ s' ∧ a.2 ∈ t ∧ r a.1 a.2

Tactic:
rw [mem_interedges_iff] at hx hy

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a : α × β
hx : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
hy : a.1 ∈ s' ∧ a.2 ∈ t ∧ r a.1 a.2
⊢ False

Tactic:
hs hx.1 hy.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a : α × β
hx : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
hy : a.1 ∈ s' ∧ a.2 ∈ t ∧ r a.1 a.2
⊢ False

Tactic:
exact hs hx.1 hy.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : Disjoint t t'
rw : ∀ (ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t') ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'
⊢ Disjoint (interedges r s t) (interedges r s t')

Tactic:
rw [Finset.disjoint_left] at ht ⊢

Premises used: Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a : α × β
hx : a ∈ interedges r s t
hy : a ∈ interedges r s t'
⊢ a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2

Tactic:
rw [mem_interedges_iff] at hx hy

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a : α × β
hx : a ∈ interedges r s t
hy : a ∈ interedges r s t'
hx₁ : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
⊢ a.1 ∈ s ∧ a.2 ∈ t' ∧ r a.1 a.2

Tactic:
rw [mem_interedges_iff] at hx hy

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a : α × β
hx : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
hy : a.1 ∈ s ∧ a.2 ∈ t' ∧ r a.1 a.2
⊢ False

Tactic:
ht hx.2.1 hy.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a : α × β
hx : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
hy : a.1 ∈ s ∧ a.2 ∈ t' ∧ r a.1 a.2
⊢ False

Tactic:
exact ht hx.2.1 hy.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
h :
  ∀ (x : α) (y : β),
    (x, y) ∈ interedges r s t ↔
      Membership.mem (γ := Finset (α × β))
        (s.biUnion fun (x : α) ↦ map { toFun := fun (x_1 : β) ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})) (x, y)
⊢ interedges r s t = s.biUnion fun (x : α) ↦ map { toFun := fun (x_1 : β) ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ interedges r s t ↔
    Membership.mem (γ := Finset (α × β))
      (s.biUnion fun (x : α) ↦ map { toFun := fun (x_1 : β) ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})) (x, y)

Tactic:
simp [mem_interedges_iff]

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
h :
  ∀ (a : α × β),
    a ∈ interedges r (s.biUnion f) t ↔
      Membership.mem (γ := Finset (α × β)) (s.biUnion fun (a : ι) ↦ interedges r (f a) t) a
⊢ interedges r (s.biUnion f) t = s.biUnion fun (a : ι) ↦ interedges r (f a) t

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a : α × β
⊢ a ∈ interedges r (s.biUnion f) t ↔
    Membership.mem (γ := Finset (α × β)) (s.biUnion fun (a : ι) ↦ interedges r (f a) t) a

Tactic:
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]

Premises used: Rel.mem_interedges_iff, exists_and_right, and_assoc, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
h :
  ∀ (a : α × β),
    a ∈ interedges r s (t.biUnion f) ↔
      Membership.mem (γ := Finset (α × β)) (t.biUnion fun (b : ι) ↦ interedges r s (f b)) a
⊢ interedges r s (t.biUnion f) = t.biUnion fun (b : ι) ↦ interedges r s (f b)

Tactic:
ext a
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
h : a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2
⊢ a ∈ interedges r s (t.biUnion f) ↔
    Membership.mem (γ := Finset (α × β)) (t.biUnion fun (b : ι) ↦ interedges r s (f b)) a

Tactic:
simp only [mem_interedges_iff, mem_biUnion]

Premises used: Rel.mem_interedges_iff, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2

Tactic:
⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩,
    fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩

Premises used: _private.0.Rel.interedges_biUnion_right.match_2, Membership.mem, Exists, Prod.fst, And, And.intro, Iff.intro, Exists.intro, _private.0.Rel.interedges_biUnion_right.match_1, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2

Tactic:
exact ⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩,
    fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
simp_rw :
  interedges r (s.biUnion f) (t.biUnion g) = s.biUnion fun (a : ι) ↦ t.biUnion fun (b : κ) ↦ interedges r (f a) (g b)
simp_rw₁ :
  Eq (α := Finset (α × β)) (s.biUnion fun (a : ι) ↦ interedges r (f a) (t.biUnion g))
    (s.biUnion fun (a : ι) ↦ t.biUnion fun (b : κ) ↦ interedges r (f a) (g b))
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) ↦ interedges r (f ab.1) (g ab.2)

Tactic:
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]

Premises used: Finset.product_biUnion, Rel.interedges_biUnion_left, Rel.interedges_biUnion_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) ≤ #s * #t

Tactic:
(card_filter_le _ _).trans (card_product _ _).le

Premises used: Rel.interedges, Finset.card_product, Eq.le, LE.le.trans, Finset.card_filter_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
ha : LE.le (α := ℚ) 0 (↑(#(interedges r s t)) : ℚ)
hb : 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
⊢ 0 ≤ edgeDensity r s t

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ LE.le (α := ℚ) 0 (↑(#(interedges r s t)) : ℚ)

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.zero_le, Rel.interedges, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ LE.le (α := ℚ) 0 (↑(#(interedges r s t)) : ℚ)

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.cast_mul._simp_1, Nat.zero_le, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
h : (↑(#(interedges r s t)) : ℚ) ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
hb : 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
⊢ edgeDensity r s t ≤ 1

Tactic:
apply div_le_one_of_le₀

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ (↑(#(interedges r s t)) : ℚ) ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
mod_cast card_interedges_le_mul r s t

Premises used: Nat.cast_mul._simp_1, Rel.card_interedges_le_mul, Rel.interedges, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ (↑(#(interedges r s t)) : ℚ) ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
exact mod_cast card_interedges_le_mul r s t

Premises used: Rel.card_interedges_le_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
rw :
  HAdd.hAdd (α := ℚ) (↑(#(interedges r s t)) : ℚ) (↑(#(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
rw₁ : HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0
⊢ edgeDensity r s t + edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s t = 1

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

Premises used: div_eq_one_iff_eq, Rel.edgeDensity, add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ HAdd.hAdd (α := ℚ) (↑(#(interedges r s t)) : ℚ) (↑(#(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
mod_cast card_interedges_add_card_interedges_compl r s t

Premises used: Nat.cast_mul._simp_1, Rel.interedges, congrArg, Nat.cast_add._simp_1, cast, congr, Finset.card, Nat.cast_inj._simp_1, Eq.symm, Eq, Not, Eq.trans, Rel.card_interedges_add_card_interedges_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ HAdd.hAdd (α := ℚ) (↑(#(interedges r s t)) : ℚ) (↑(#(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t)) : ℚ) =
    HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)

Tactic:
exact mod_cast card_interedges_add_card_interedges_compl r s t

Premises used: Rel.card_interedges_add_card_interedges_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0

Tactic:
mod_cast (mul_pos hs.card_pos ht.card_pos).ne'

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Finset.Nonempty.card_pos, Ne, Nat.cast, LT.lt.ne', mul_pos, Finset.card, Nat.cast_inj._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0

Tactic:
exact mod_cast (mul_pos hs.card_pos ht.card_pos).ne'

Premises used: Finset.Nonempty.card_pos, LT.lt.ne', mul_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
rw : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) (↑(card.{u_4} (α := α) ∅) : ℚ) (↑(#t) : ℚ) = 0
rw₁ : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) (↑0 : ℚ) (↑(#t) : ℚ) = 0
rw₂ : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) 0 (↑(#t) : ℚ) = 0
rw₃ : HDiv.hDiv (α := ℚ) (↑(#(interedges r ∅ t)) : ℚ) 0 = 0
rw₄ rw₅ : Eq (α := ℚ) 0 0
⊢ edgeDensity r ∅ t = 0

Tactic:
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]

Premises used: MulZeroClass.zero_mul, Rel.edgeDensity, Finset.card_empty, Nat.cast_zero, div_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
rw₁ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑0 : ℚ) = 0
rw₂ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) 0 = 0
rw₃ : HDiv.hDiv (α := ℚ) (↑(#(interedges r s ∅)) : ℚ) 0 = 0
rw₄ rw₅ : Eq (α := ℚ) 0 0
⊢ edgeDensity r s ∅ = 0

Tactic:
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]

Premises used: Rel.edgeDensity, MulZeroClass.mul_zero, Finset.card_empty, Nat.cast_zero, div_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
simp_rw : card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]

Premises used: id, Rel.interedges_biUnion_left, Finpartition.biUnion_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
rw : (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t
⊢ card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
rw [card_biUnion]

Premises used: Finset.card_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
⊢ (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t

Tactic:
fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

Premises used: Finpartition.disjoint, Set.PairwiseDisjoint, Rel.interedges_disjoint_left, Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
⊢ (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t

Tactic:
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

Premises used: Finpartition.disjoint, Rel.interedges_disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
simp_rw : #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₁ :
  card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r (id a) t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₂ :
  card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₃ : (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

Premises used: Finpartition.disjoint, Rel.interedges_disjoint_left, id, Finset.card_biUnion, Rel.interedges_biUnion_left, Finpartition.biUnion_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
simp_rw : card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]

Premises used: id, Rel.interedges_biUnion_right, Finpartition.biUnion_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
rw : (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ interedges r s b
⊢ card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
rw [card_biUnion]

Premises used: Finset.card_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
⊢ (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ interedges r s b

Tactic:
fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)

Premises used: Finpartition.disjoint, Set.PairwiseDisjoint, Set.Pairwise, Rel.interedges_disjoint_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
⊢ (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ interedges r s b

Tactic:
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)

Premises used: Finpartition.disjoint, Rel.interedges_disjoint_right