awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
refine_1 :
  ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
    r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have refine_2 : ∀
  (h :
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜))
  (s : Finset (Sym2 V)) (hs : s ⊆ G.edgeFinset) (hG : p (G.deleteEdges (↑s : Set (Sym2 V)))), r ≤ (↑(#s) : 𝕜)
Tactic: refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
⊢ r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have this : p (G.deleteEdges (↑(G.edgeFinset \ H.edgeFinset) : Set (Sym2 V))) → r ≤ (↑(#(G.edgeFinset \ H.edgeFinset)) : 𝕜)
Tactic: have := h (sdiff_subset (t := H.edgeFinset))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p (G.deleteEdges (↑(G.edgeFinset \ H.edgeFinset) : Set (Sym2 V))) → r ≤ (↑(#(G.edgeFinset \ H.edgeFinset)) : 𝕜)
⊢ r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have this₁ : p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
Tactic: simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have refine_1 : ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
  r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
Tactic: classical
  refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
  · have := h (sdiff_subset (t := H.edgeFinset))
    simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
    exact this hH
  · classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
refine_1 :
  ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
    r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have refine_2 : ∀
  (h :
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜))
  (s : Finset (Sym2 V)) (hs : s ⊆ G.edgeFinset) (hG : p (G.deleteEdges (↑s : Set (Sym2 V)))), r ≤ (↑(#s) : 𝕜)
Tactic: classical
  refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
  · have := h (sdiff_subset (t := H.edgeFinset))
    simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
    exact this hH
  · classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
have rw : x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
Tactic: rw [interedges, mem_filter, Finset.mem_product, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
rw : x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
have rw₁ : x ∈ s ×ˢ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
Tactic: rw [interedges, mem_filter, Finset.mem_product, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
rw : x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₁ : x ∈ s ×ˢ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
have rw₂ : (x.1 ∈ s ∧ x.2 ∈ t) ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
Tactic: rw [interedges, mem_filter, Finset.mem_product, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
rw : x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₁ : x ∈ s ×ˢ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₂ : (x.1 ∈ s ∧ x.2 ∈ t) ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
have rw₃ : x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
Tactic: rw [interedges, mem_filter, Finset.mem_product, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
⊢ interedges r ∅ t = ∅
have rw : {e ∈ SProd.sprod (α := Finset α) ∅ t | r e.1 e.2} = ∅
Tactic: rw [interedges, Finset.empty_product, filter_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
rw : {e ∈ SProd.sprod (α := Finset α) ∅ t | r e.1 e.2} = ∅
⊢ interedges r ∅ t = ∅
have rw₁ : Eq (α := Finset (α × β)) ({e ∈ ∅ | r e.1 e.2}) ∅
Tactic: rw [interedges, Finset.empty_product, filter_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
rw : {e ∈ SProd.sprod (α := Finset α) ∅ t | r e.1 e.2} = ∅
rw₁ : Eq (α := Finset (α × β)) ({e ∈ ∅ | r e.1 e.2}) ∅
⊢ interedges r ∅ t = ∅
have rw₂ : Eq (α := Finset (α × β)) ∅ ∅
Tactic: rw [interedges, Finset.empty_product, filter_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁
have simp_rw : x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2
Tactic: simp_rw [mem_interedges_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
Tactic: rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw : #(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw₁ : #({e ∈ s ×ˢ t | r e.1 e.2}) + #(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw₂ : #({e ∈ s ×ˢ t | r e.1 e.2}) + #({e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw₃ : #({e ∈ s ×ˢ t | r e.1 e.2} ∪ {e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw₄ : Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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})
⊢ #(interedges r s t) + #(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t) = #s * #t
have rw₅ : #(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)
have rw : ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s') (t : Finset β) ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t
Tactic: rw [Finset.disjoint_left] at hs ⊢
Cleared hypotheses: hs, t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ False
have hx₁ : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
Tactic: rw [mem_interedges_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ False
have hy₁ : a.1 ∈ s' ∧ a.2 ∈ t ∧ r a.1 a.2
Tactic: rw [mem_interedges_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : Disjoint t t'
⊢ Disjoint (interedges r s t) (interedges r s t')
have rw : ∀ (ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t') ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'
Tactic: rw [Finset.disjoint_left] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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'
⊢ False
have hx₁ : a.1 ∈ s ∧ a.2 ∈ t ∧ r a.1 a.2
Tactic: rw [mem_interedges_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ False
have hy₁ : a.1 ∈ s ∧ a.2 ∈ t' ∧ r a.1 a.2
Tactic: rw [mem_interedges_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
⊢ interedges r s t = s.biUnion fun (x : α) ↦ map { toFun := fun (x_1 : β) ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})
have 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' := sorry } ({y ∈ t | r x y})) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 α
⊢ interedges r (s.biUnion f) t = s.biUnion fun (a : ι) ↦ interedges r (f a) t
have h : ∀ (a : α × β),
  a ∈ interedges r (s.biUnion f) t ↔
    Membership.mem (γ := Finset (α × β)) (s.biUnion fun (a : ι) ↦ interedges r (f a) t) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 β
⊢ interedges r s (t.biUnion f) = t.biUnion fun (b : ι) ↦ interedges r s (f b)
have h : ∀ (a : α × β),
  a ∈ interedges r s (t.biUnion f) ↔
    Membership.mem (γ := Finset (α × β)) (t.biUnion fun (b : ι) ↦ interedges r s (f b)) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 (t.biUnion f) ↔
    Membership.mem (γ := Finset (α × β)) (t.biUnion fun (b : ι) ↦ interedges r s (f b)) a
have 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
Tactic: simp only [mem_interedges_iff, mem_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 β
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) ↦ interedges r (f ab.1) (g ab.2)
have simp_rw : interedges r (s.biUnion f) (t.biUnion g) = s.biUnion fun (a : ι) ↦ t.biUnion fun (b : κ) ↦ interedges r (f a) (g b)
Tactic: simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) ↦ interedges r (f ab.1) (g ab.2)
have 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))
Tactic: simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ edgeDensity r s t
have ha : LE.le (α := ℚ) 0 (↑(#(interedges r s t)) : ℚ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)) : ℚ)
⊢ 0 ≤ edgeDensity r s t
have hb : 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ edgeDensity r s t ≤ 1
have h : (↑(#(interedges r s t)) : ℚ) ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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) : ℚ)
⊢ edgeDensity r s t ≤ 1
have hb : 0 ≤ HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ edgeDensity r s t + edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s t = 1
have rw : HAdd.hAdd (α := ℚ) (↑(#(interedges r s t)) : ℚ) (↑(#(interedges (fun (x : α) (y : β) ↦ ¬r x y) s t)) : ℚ) =
  HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ)
Tactic: rw [edgeDensity, edgeDensity, ← add_div, div_eq_one_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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) : ℚ)
⊢ edgeDensity r s t + edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s t = 1
have rw₁ : HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) ≠ 0
Tactic: rw [edgeDensity, edgeDensity, ← add_div, div_eq_one_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
⊢ edgeDensity r ∅ t = 0
have rw : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) (↑(card.{u_4} (α := α) ∅) : ℚ) (↑(#t) : ℚ) = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ edgeDensity r ∅ t = 0
have rw₁ : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) (↑0 : ℚ) (↑(#t) : ℚ) = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ edgeDensity r ∅ t = 0
have rw₂ : (↑(#(interedges r ∅ t)) : ℚ) / HMul.hMul (α := ℚ) 0 (↑(#t) : ℚ) = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ edgeDensity r ∅ t = 0
have rw₃ : HDiv.hDiv (α := ℚ) (↑(#(interedges r ∅ t)) : ℚ) 0 = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ edgeDensity r ∅ t = 0
have rw₄ : Eq (α := ℚ) 0 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]