Golf Request

Stream: new members

[Marcus Rossel]

Golf Request

I'm trying to solve the theorem below, while keeping the structure of the calc-block. My problem is that I don't know what good tactics are to solve equalities over $\mathbb{R}$ when specific equations like $\Gamma(n + 1) = n!$ are also required. Similar for casting from $\mathbb{N}$ to $\mathbb{R}$.
I've left the side conditions of theorems as sorrys for now, as I'm rather interested in reducing the number of manual rws.

import Mathlib

open Nat

notation:100 r "﹗" => Real.Gamma (r + 1)

variable {n r : Nat} (h₁ : r < n + 1) (h₂ : r ≠ 0)

example : n ! / ((r - 1)! * (n - r + 1)!) + n ! / (r ! * (n - r)!) = (n + 1)! / (r ! * (n + 1 - r)!) :=
  cast_inj.mp <| calc
    _ = n﹗ / ((r - 1)﹗ * (n - r + 1)﹗) + n﹗ / (r﹗ * (n - r)﹗) := by
      rw [cast_add, cast_div sorry sorry, cast_div sorry sorry, cast_mul, cast_mul]
      repeat' rw [← Real.Gamma_nat_eq_factorial]
      rw [cast_sub sorry, cast_add, cast_sub sorry, cast_one]
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * (1 / (n - r + 1) + 1 / r) := by
      rw (occs := [3]) [Real.Gamma_add_one sorry]
      rw (occs := [2]) [mul_comm]
      rw [← mul_assoc]
      rw [div_mul_eq_div_mul_one_div]
      rw (occs := [4]) [← sub_add_cancel ↑r (1 : Real)]
      rw (occs := [5]) [Real.Gamma_add_one sorry]
      ring
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * ((r + (n - r + 1)) / (r * (n - r + 1))) := by
      rw [div_add_div _ _ sorry sorry]
      ring
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * ((n + 1) / (r * (n - r + 1))) := by
      ring
    _ = (n + 1)﹗ / (r﹗ * (n + 1 - r)﹗) := by
      rw [_root_.div_mul_div_comm, mul_comm, ← Real.Gamma_add_one sorry, mul_assoc]
      rw (occs := [2]) [mul_comm]
      rw [mul_assoc, ← mul_assoc]
      rw (occs := [2]) [mul_comm]
      rw [sub_add, sub_self, sub_zero, ← Real.Gamma_add_one sorry, ← Real.Gamma_add_one sorry]
      ring_nf
    _ = _ := by
      rw [cast_div sorry sorry, cast_mul]
      repeat' rw [← Real.Gamma_nat_eq_factorial]
      rw [cast_add, cast_sub sorry, cast_add, cast_one]

[Aaron Liu]

What if you plug in r := 0?

[Aaron Liu]

Remember 0 - 1 = 0

[Marcus Rossel]

Ah sorry, I missed some assumptions. I've added them now.

[Aaron Liu]

Can I ditch your long complicated proof for my simpler one?

import Mathlib

open Nat

variable {n r : Nat} (h₁ : r < n + 1) (h₂ : r ≠ 0)

example : n ! / ((r - 1)! * (n - r + 1)!) + n ! / (r ! * (n - r)!) = (n + 1)! / (r ! * (n + 1 - r)!) := by
  rw [← Nat.choose_eq_factorial_div_factorial (by omega), ← Nat.choose_eq_factorial_div_factorial (by omega),
    show n - r + 1 = n - (r - 1) by omega, ← Nat.choose_eq_factorial_div_factorial (by omega),
    Nat.choose_eq_choose_pred_add (Nat.add_one_pos n) (Nat.pos_iff_ne_zero.mpr h₂), Nat.add_sub_cancel]

[Marcus Rossel]

Unfortunately I want to exactly keep the structure of the calc-block :upside_down:

[Aaron Liu]

Unfortunately I'm not motivated enough to fill in the rest

import Mathlib

open Nat

notation:100 r "﹗" => Real.Gamma (r + 1)

variable {n r : Nat} (h₁ : r < n + 1) (h₂ : r ≠ 0)

example : n ! / ((r - 1)! * (n - r + 1)!) + n ! / (r ! * (n - r)!) = (n + 1)! / (r ! * (n + 1 - r)!) :=
  cast_inj.mp <| calc
    _ = n﹗ / ((r - 1)﹗ * (n - r + 1)﹗) + n﹗ / (r﹗ * (n - r)﹗) := by
      rw [cast_add, cast_div sorry (by positivity), cast_div sorry sorry, cast_mul, cast_mul]
      repeat' rw [← Real.Gamma_nat_eq_factorial]
      rw [cast_sub (by omega), cast_add, cast_sub (by omega), cast_one]
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * (1 / (n - r + 1) + 1 / r) := by
      rw (occs := [3]) [Real.Gamma_add_one (by rify at h₁; linarith)]
      rw (occs := [2]) [mul_comm]
      rw [← mul_assoc]
      rw [div_mul_eq_div_mul_one_div]
      rw (occs := [4]) [← sub_add_cancel ↑r (1 : Real)]
      rw (occs := [5]) [Real.Gamma_add_one (by ring_nf; exact_mod_cast h₂)]
      ring
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * ((r + (n - r + 1)) / (r * (n - r + 1))) := by
      rw [div_add_div _ _ (by rify at h₁; linarith) (by exact_mod_cast h₂)]
      ring
    _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * ((n + 1) / (r * (n - r + 1))) := by
      ring
    _ = (n + 1)﹗ / (r﹗ * (n + 1 - r)﹗) := by
      rw [_root_.div_mul_div_comm, mul_comm, ← Real.Gamma_add_one (by norm_cast), mul_assoc]
      rw (occs := [2]) [mul_comm]
      rw [mul_assoc, ← mul_assoc]
      rw (occs := [2]) [mul_comm]
      rw [sub_add, sub_self, sub_zero, ← Real.Gamma_add_one (by exact_mod_cast h₂), ← Real.Gamma_add_one (by rify at h₁; linarith)]
      ring_nf
    _ = _ := by
      rw [cast_div sorry sorry, cast_mul]
      repeat' rw [← Real.Gamma_nat_eq_factorial]
      rw [cast_add, cast_sub (by omega), cast_add, cast_one]

[Marcus Rossel]

Thanks! I'm fine keeping the sorrys as sorrys though - filling those in is not really important to me. I'm rather interested in eliminating more of the manual rw steps.

[Aaron Liu]

Is Real.Gamma_add_one and Real.Gamma_nat_eq_factorial named wrong? Those should be Real.gamma_add_one and Rea.gamma_nat_eq_factorial.

[Marcus Rossel]

I guess the function is called docs#Real.Gamma, so it's consistent.

[Aaron Liu]

Real.Gamma feels wrong too, although I kind of understand this one