awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
have bc : r * (n % r) - r ≤ r * (n % r) - n % r
Tactic: rw [Nat.sub_one_mul, Nat.sub_one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inl : ∀ (cf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)),
  let n := Fintype.card V;
  #G.edgeFinset ≤
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2
Tactic: rcases r.eq_zero_or_pos with rfl | hr
Cleared hypotheses: r, cf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
inl :
  ∀ (cf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)),
    let n := Fintype.card V;
    #G.edgeFinset ≤
      (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
        (n % 0).choose 2
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : ∀ (hr : r > 0),
  let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
Tactic: rcases r.eq_zero_or_pos with rfl | hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2
have cf₁ : Fintype.card V = 0
Tactic: rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf
Cleared hypotheses: cf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2
have inl : #G.edgeFinset ≤ (Fintype.card V).choose 2
Tactic: simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : ∀ (H : SimpleGraph V) (w : DecidableRel H.Adj) (maxH : H.IsTuranMaximal r),
  let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
Tactic: obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have h : (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
    (Fintype.card V % r).choose 2 =
  #H.edgeFinset
Tactic: convert! maxH.2 cf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    #H.edgeFinset
have h : (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
    (Fintype.card V % r).choose 2 =
  Finset.card (α := Sym2 (Fin (Fintype.card V))) (edgeFinset (turanGraph (Fintype.card V) r))
Tactic: rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
      card_edgeFinset_turanGraph]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
h :
  (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    Finset.card (α := Sym2 (Fin (Fintype.card V))) (edgeFinset (turanGraph (Fintype.card V) r))
⊢ (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    #H.edgeFinset
have h₁ : (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
    (Fintype.card V % r).choose 2 =
  (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
    (Fintype.card V % r).choose 2
Tactic: rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
      card_edgeFinset_turanGraph]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
⊢ AntitoneOn (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) (Set.Ici 2)
have hf : ∀ n ≥ 2,
  HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
Tactic: apply antitoneOn_nat_Ici_of_succ_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ)
have enter : extremalNumber (n + 1) H
Tactic: enter [1, 1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| extremalNumber (n + 1) H
have rw : extremalNumber (Fintype.card (Fin (n + 1))) H
Tactic: rw [← Fintype.card_fin (n + 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ)
have enter : extremalNumber (Fintype.card (Fin (n + 1))) H
Tactic: enter [1, 1]
    rw [← Fintype.card_fin (n + 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
have hf : HDiv.hDiv (α := ℝ) (↑(extremalNumber (Fintype.card (Fin (n + 1))) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
  HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
Tactic: conv_lhs =>
    enter [1, 1]
    rw [← Fintype.card_fin (n + 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ 2 ≤ n + 1
have linarith : n + 1 < 2 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
linarith :
  n + 1 < 2 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2) = 0
⊢ 2 ≤ n + 1
have linarith₁ : n + 1 < 2 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber (Fintype.card (Fin (n + 1))) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
have hf : ∀ ⦃G : SimpleGraph (Fin (n + 1))⦄ [inst : DecidableRel G.Adj],
  H.Free G →
    (↑(#G.edgeFinset) : ℝ) ≤
      HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)
Tactic: rw [div_le_iff₀ (mod_cast Nat.choose_pos (by linarith)),
    extremalNumber_le_iff_of_nonneg H (by positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
⊢ (↑(#G.edgeFinset) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)
have hf : #G.edgeFinset * (n - 1) ≤ (n + 1) * extremalNumber n H
Tactic: rw [mul_comm, ← mul_div_assoc, le_div_iff₀' (mod_cast Nat.choose_pos hn), Nat.cast_choose_two,
    Nat.cast_choose_two, Nat.cast_add_one, add_sub_cancel_right (n : ℝ) 1,
    mul_comm _ (n - 1 : ℝ), ← mul_div (n - 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_comm (n - 1 : ℝ), ← mul_div (n + 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_le_mul_iff_right₀ (by positivity), ← Nat.cast_pred (by positivity), ← Nat.cast_mul,
    ← Nat.cast_add_one, ← Nat.cast_mul, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
| (n + 1) * extremalNumber n H
have rw : Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
Tactic: rw [← Fintype.card_fin (n + 1), ← card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset * (n - 1) ≤ (n + 1) * extremalNumber n H
have hf : #G.edgeFinset * (n - 1) ≤ Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
Tactic: conv_rhs =>
    rw [← Fintype.card_fin (n + 1), ← card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset * (n - 1) ≤ Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
have hf : ∀ b ∈ G.edgeFinset,
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ b)) :
      ℕ)
Tactic: apply card_nsmul_le_card_nsmul' (r := fun v e ↦ v ∉ e)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
hf :
  ∀ b ∈ G.edgeFinset,
    n - 1 ≤
      (↑(Finset.card (α := Fin (n + 1))
            (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ b)) :
        ℕ)
⊢ #G.edgeFinset * (n - 1) ≤ Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
have hf₁ : ∀ (a : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) univ a →
    (↑(#(bipartiteAbove (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) G.edgeFinset a)) : ℕ) ≤
      extremalNumber n H
Tactic: apply card_nsmul_le_card_nsmul' (r := fun v e ↦ v ∉ e)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf : n - 1 ≤
  (↑(Finset.card (α := Fin (n + 1))
        (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
    ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₇ : n - 1 ≤ (↑(n + 1 - #e.toFinset) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
hf₇ : n - 1 ≤ (↑(n + 1 - #e.toFinset) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₈ : n - 1 ≤ (↑(n + 1 - 2) : ℕ)
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
hf₇ : n - 1 ≤ (↑(n + 1 - #e.toFinset) : ℕ)
hf₈ : n - 1 ≤ (↑(n + 1 - 2) : ℕ)
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₉ : n - 1 ≤ n + 1 - 2
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
hf₇ : n - 1 ≤ (↑(n + 1 - #e.toFinset) : ℕ)
hf₈ : n - 1 ≤ (↑(n + 1 - 2) : ℕ)
hf₉ : n - 1 ≤ n + 1 - 2
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)
have hf₁₀ : n - 1 ≤ n - 1
Tactic: simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]