[GOAL]
m n : ℕ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℕ
h : n % 2 = 0
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℕ
h : n % 2 = 1
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℕ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℕ
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℕ
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
m✝ n : ℕ
x✝ : Even n
m : ℕ
hm : n = m + m
⊢ n % 2 = 0
[PROOFSTEP]
simp [← two_mul, hm]
[GOAL]
m n : ℕ
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2
[PROOFSTEP]
simp [← two_mul, h]
[GOAL]
m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ n % 2 = 1
[PROOFSTEP]
rw [hm, add_mod, mul_mod_right]
[GOAL]
m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ (0 + 1 % 2) % 2 = 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
rw [h, add_comm]
[GOAL]
m n : ℕ
⊢ ¬Even n ↔ n % 2 = 1
[PROOFSTEP]
rw [even_iff, mod_two_ne_zero]
[GOAL]
m n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0
[PROOFSTEP]
rw [odd_iff, mod_two_ne_one]
[GOAL]
m n : ℕ
⊢ Even n ↔ ¬Odd n
[PROOFSTEP]
rw [not_odd_iff, even_iff]
[GOAL]
m n : ℕ
⊢ Odd n ↔ ¬Even n
[PROOFSTEP]
rw [not_even_iff, odd_iff]
[GOAL]
m n : ℕ
h : Odd n
⊢ ¬2 ∣ n
[PROOFSTEP]
rwa [← even_iff_two_dvd, ← odd_iff_not_even]
[GOAL]
m n : ℕ
⊢ IsCompl {n | Even n} {n | Odd n}
[PROOFSTEP]
simp only [← Set.compl_setOf, isCompl_compl, odd_iff_not_even]
[GOAL]
m n✝ n : ℕ
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
simp [Xor', odd_iff_not_even, Decidable.em (Even n)]
[GOAL]
m n✝ n : ℕ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1
[PROOFSTEP]
simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n
[GOAL]
m n✝ n : ℕ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
[PROOFSTEP]
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)
[GOAL]
case inl.intro
m n k : ℕ
⊢ ∃ k_1, Xor' (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case inr.intro
m n k : ℕ
⊢ ∃ k_1, Xor' (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case h
m n k : ℕ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
[PROOFSTEP]
simpa only [← two_mul, eq_self_iff_true, xor_true] using (succ_ne_self (2 * k)).symm
[GOAL]
case h
m n k : ℕ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
[PROOFSTEP]
simpa only [xor_true, xor_comm] using (succ_ne_self _)
[GOAL]
m✝ n✝ m n : ℕ
hn : Odd n
hm : Even m
⊢ m % 2 + (m + n) % 2 = 1
[PROOFSTEP]
rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]
[GOAL]
m✝ n✝ m n : ℕ
hn : Odd n
hm : Odd m
⊢ m % 2 + (m + n) % 2 = 1
[PROOFSTEP]
rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]
[GOAL]
m✝ n m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1
[PROOFSTEP]
rw [add_comm, mod_two_add_succ_mod_two]
[GOAL]
m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' mod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.add_mod]
[GOAL]
case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.add_mod]
[GOAL]
case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.add_mod]
[GOAL]
case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.add_mod]
[GOAL]
m n : ℕ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n : ℕ
⊢ Even (n + 1) ↔ ¬Even n
[PROOFSTEP]
simp [even_add]
[GOAL]
m n✝ n : ℕ
⊢ ¬Even (bit1 n)
[PROOFSTEP]
simp [bit1, parity_simps]
[GOAL]
m n✝ n : ℕ
⊢ ¬2 ∣ 2 * n + 1
[PROOFSTEP]
simp [add_mod]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
conv_rhs => rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
by_cases h : Even n
[GOAL]
case pos
m n : ℕ
h✝ : n ≤ m
h : Even n
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
m n : ℕ
h✝ : n ≤ m
h : ¬Even n
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
h : n ≤ m
⊢ Even (m - n)
[PROOFSTEP]
simp only [even_sub' h, *]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
h : m ≤ n
⊢ Even (m - n)
[PROOFSTEP]
simp only [tsub_eq_zero_iff_le.mpr h, even_zero]
[GOAL]
m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' mod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.mul_mod]
[GOAL]
case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.mul_mod]
[GOAL]
case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.mul_mod]
[GOAL]
case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Nat.mul_mod]
[GOAL]
m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n
[PROOFSTEP]
simp [not_or, even_mul]
[GOAL]
m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
m n : ℕ
⊢ Even (m ^ zero) ↔ Even m ∧ zero ≠ 0
[PROOFSTEP]
simp (config := { contextual := true }) [*, pow_succ', even_mul]
[GOAL]
case succ
m n✝ n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even (m ^ succ n) ↔ Even m ∧ succ n ≠ 0
[PROOFSTEP]
simp (config := { contextual := true }) [*, pow_succ', even_mul]
[GOAL]
m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
[PROOFSTEP]
rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, Nat.div_mod_eq_mod_mul_div, mul_comm]
[GOAL]
m n : ℕ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_add, not_iff, odd_iff_not_even]
[GOAL]
m n : ℕ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [add_comm, odd_add]
[GOAL]
m n : ℕ
h : Odd (m + n)
hnot : m = n
⊢ False
[PROOFSTEP]
simp [hnot] at h
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub h, not_iff, odd_iff_not_even]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub h, not_iff, not_iff_comm, odd_iff_not_even]
[GOAL]
m n✝ n : ℕ
⊢ Even (n * (n + 1))
[PROOFSTEP]
rw [even_mul, even_add_one]
[GOAL]
m n✝ n : ℕ
⊢ Even n ∨ ¬Even n
[PROOFSTEP]
exact em _
[GOAL]
m n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n
[PROOFSTEP]
rw [← odd_iff.mp h, div_add_mod]
[GOAL]
m n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n
[PROOFSTEP]
rw [← odd_iff.mp h, div_add_mod']
[GOAL]
m n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n
[PROOFSTEP]
rw [← odd_iff.mp h, mod_add_div']
[GOAL]
m n : ℕ
⊢ bit0 n / 2 = n
[PROOFSTEP]
rw [← Nat.bit0_eq_bit0, bit0_eq_two_mul, two_mul_div_two_of_even (even_bit0 n)]
[GOAL]
m n : ℕ
⊢ bit1 n / 2 = n
[PROOFSTEP]
rw [← Nat.bit1_eq_bit1, bit1, bit0_eq_two_mul, Nat.two_mul_div_two_add_one_of_odd (odd_bit1 n)]
[GOAL]
m n : ℕ
⊢ bit0 n / bit0 m = n / m
[PROOFSTEP]
rw [bit0_eq_two_mul m, ← Nat.div_div_eq_div_mul, bit0_div_two]
[GOAL]
m n : ℕ
⊢ bit1 n / bit0 m = n / m
[PROOFSTEP]
rw [bit0_eq_two_mul, ← Nat.div_div_eq_div_mul, bit1_div_two]
[GOAL]
m n : ℕ
⊢ bit0 n % bit0 m = bit0 (n % m)
[PROOFSTEP]
rw [bit0_eq_two_mul n, bit0_eq_two_mul m, bit0_eq_two_mul (n % m), Nat.mul_mod_mul_left]
[GOAL]
m n : ℕ
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
have h₁ :=
  congr_arg bit1
    (Nat.div_add_mod n m)
      -- `∀ m n : ℕ, bit0 m * n = bit0 (m * n)` seems to be missing...
[GOAL]
m n : ℕ
h₁ : bit1 (m * (n / m) + n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
rw [bit1_add, bit0_eq_two_mul, ← mul_assoc, ← bit0_eq_two_mul] at h₁
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
have h₂ := Nat.div_add_mod (bit1 n) (bit0 m)
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (bit1 n / bit0 m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
rw [bit1_div_bit0] at h₂
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (n / m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
exact add_left_cancel (h₂.trans h₁.symm)
[GOAL]
m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)
[PROOFSTEP]
simp [*, two_ne_zero, parity_simps]
  /- Porting note: the `simp` lemmas about `bit*` no longer apply, but `simp` in Lean 4 currently
  simplifies decidable propositions. This may change in the future. -/
[GOAL]
m n : ℕ
⊢ ¬Even 25394535
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[bit0 n] = id
[PROOFSTEP]
rw [bit0, ← two_mul, iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[bit1 n] = f
[PROOFSTEP]
rw [bit1, ← succ_eq_add_one, iterate_succ, hf.iterate_bit0, comp.left_id]
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id
[PROOFSTEP]
rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id
[PROOFSTEP]
rcases hn with ⟨m, rfl⟩
[GOAL]
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
[PROOFSTEP]
rw [← two_mul, hf.iterate_two_mul]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f
[PROOFSTEP]
rcases hn with ⟨m, rfl⟩
[GOAL]
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
[PROOFSTEP]
rw [iterate_add, hf.iterate_two_mul, comp.left_id, iterate_one]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id
[PROOFSTEP]
rwa [hf.iterate_even hn, eq_comm] at H
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id
[PROOFSTEP]
rwa [hf.iterate_odd hn] at H
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ m ≠ 2
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False
[PROOFSTEP]
exact absurd (hn.of_dvd_nat hm) (by decide)
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd 2
[PROOFSTEP]
decide


[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(choose b a) = ↑b ! / (↑a ! * ↑(b - a)!)
[PROOFSTEP]
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_ne_zero _)
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(choose b a) = ↑b ! / (↑a ! * ↑(b - a)!)
[PROOFSTEP]
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(choose b a) * (↑a ! * ↑(b - a)!) = ↑b !
[PROOFSTEP]
rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(choose (a + b) a) = ↑(a + b)! / (↑a ! * ↑b !)
[PROOFSTEP]
rw [cast_choose K (_root_.le_add_right le_rfl), add_tsub_cancel_left]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(choose a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer K b) / ↑b !
[PROOFSTEP]
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul, mul_comm, ←
  descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a : ℕ
⊢ ↑(choose a 2) = ↑a * (↑a - 1) / 2
[PROOFSTEP]
rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm, cast_mul, cast_two,
  eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]


[GOAL]
m n k : ℕ
⊢ choose (m + n) k = ∑ ij in antidiagonal k, choose m ij.fst * choose n ij.snd
[PROOFSTEP]
calc
  (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, Nat.cast_id]
  _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
  _ = ∑ ij : ℕ × ℕ in antidiagonal k, m.choose ij.1 * n.choose ij.2 :=
    by
    rw [coeff_mul, Finset.sum_congr rfl]
    simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]
[GOAL]
m n k : ℕ
⊢ choose (m + n) k = coeff ((X + 1) ^ (m + n)) k
[PROOFSTEP]
rw [coeff_X_add_one_pow, Nat.cast_id]
[GOAL]
m n k : ℕ
⊢ coeff ((X + 1) ^ (m + n)) k = coeff ((X + 1) ^ m * (X + 1) ^ n) k
[PROOFSTEP]
rw [pow_add]
[GOAL]
m n k : ℕ
⊢ coeff ((X + 1) ^ m * (X + 1) ^ n) k = ∑ ij in antidiagonal k, choose m ij.fst * choose n ij.snd
[PROOFSTEP]
rw [coeff_mul, Finset.sum_congr rfl]
[GOAL]
m n k : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k → coeff ((X + 1) ^ m) x.fst * coeff ((X + 1) ^ n) x.snd = choose m x.fst * choose n x.snd
[PROOFSTEP]
simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]


[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : IsPrimePow n
⊢ Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
[PROOFSTEP]
obtain ⟨p, k, hp, hk, rfl⟩ := hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
[PROOFSTEP]
rw [← Nat.prime_iff] at hp
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
[PROOFSTEP]
rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
⊢ IsPrimePow n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn')
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : Nat.minFac 0 ^ ↑(Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0
[PROOFSTEP]
simp_all
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
[PROOFSTEP]
refine' ⟨_, _, (Nat.minFac_prime hn).prime, _, h⟩
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < ↑(Nat.factorization n) (Nat.minFac n)
[PROOFSTEP]
rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.factor_iff_mem_factorization,
  Nat.mem_factors_iff_dvd hn' (Nat.minFac_prime hn)]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ Nat.minFac n ∣ n
[PROOFSTEP]
apply Nat.minFac_dvd
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
refine' exists₂_congr fun p k => _
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rintro ⟨hp, hk, hn⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rw [← hn, Nat.Prime.factorization_pow hp]
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ 0 < k ∧ Nat.factorization n = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨hk, hn⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
have hn0 : n ≠ 0 := by
  rintro rfl
  simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False
[PROOFSTEP]
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k
[PROOFSTEP]
exact ⟨Nat.prime_of_mem_factorization (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ p ∈ (Nat.factorization n).support
[PROOFSTEP]
simp [hn, hk.ne']
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ Finset.card (Nat.factorization n).support = 1
[PROOFSTEP]
simp_rw [isPrimePow_iff_factorization_eq_single, Finsupp.card_support_eq_one', exists_prop, pos_iff_ne_zero]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ ↑(Nat.factorization 0) p = 1
[PROOFSTEP]
cases not_isPrimePow_zero h
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩
[GOAL]
case inr.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases em' p.Prime with (pp | pp)
[GOAL]
case inr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' absurd _ hk0.ne'
[GOAL]
case inr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0
[PROOFSTEP]
simp [← Nat.factorization_eq_zero_of_non_prime n pp, h1]
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' ⟨p, pp, _⟩
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' Nat.eq_of_factorization_eq (Nat.ord_compl_pos p hn0).ne' (by simp) fun q => _
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Nat.factorization (n / p ^ ↑(Nat.factorization n) p)) q = ↑(Nat.factorization 1) q
[PROOFSTEP]
rw [Nat.factorization_ord_compl n p, h1]
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Finsupp.erase p (Finsupp.single p k)) q = ↑(Nat.factorization 1) q
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' ⟨fun h => IsPrimePow.exists_ord_compl_eq_one h, fun h => _⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
[PROOFSTEP]
rcases h with ⟨p, pp, h⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ord_proj_dvd n p) h] at hn ⊢
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
refine' ⟨p, n.factorization p, pp, _, by simp⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ p ^ ↑(Nat.factorization n) p = p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
simp
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ 0 < ↑(Nat.factorization n) p
[PROOFSTEP]
contrapose! hn
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
hn : ↑(Nat.factorization n) p ≤ 0
⊢ p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
simp [le_zero_iff.1 hn]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1, Nat.Prime p_1 ∧ p_1 ∣ p ^ k
[PROOFSTEP]
refine' ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, _⟩
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∀ (y : ℕ), (fun p_1 => Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p
[PROOFSTEP]
rintro q ⟨hq, hq'⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p
[PROOFSTEP]
exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, ⟨hp, hn⟩, hq⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn₀)
[GOAL]
case mpr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
[PROOFSTEP]
cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, _⟩
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ p ^ ↑(Nat.factorization n) p = n
[PROOFSTEP]
simp only [and_imp] at hq
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ p ^ ↑(Nat.factorization n) p = n
[PROOFSTEP]
apply
  Nat.dvd_antisymm
    (Nat.ord_proj_dvd _ _)
      -- We need to show n ∣ p ^ n.factorization p
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
apply Nat.dvd_of_factors_subperm hn₀
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ Nat.factors n <+~ Nat.factors (p ^ ↑(Nat.factorization n) p)
[PROOFSTEP]
rw [hp.factors_pow, List.subperm_ext_iff]
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ (x : ℕ),
    x ∈ Nat.factors n → List.count x (Nat.factors n) ≤ List.count x (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
intro q hq'
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ Nat.factors n
⊢ List.count q (Nat.factors n) ≤ List.count q (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
rw [Nat.mem_factors hn₀] at hq'
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q (Nat.factors n) ≤ List.count q (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
cases hq _ hq'.1 hq'.2
[GOAL]
case mpr.intro.intro.intro.inr.refl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p (Nat.factors n) ≤ List.count p (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n
[PROOFSTEP]
simp only [isPrimePow_iff_unique_prime_dvd]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
apply exists_unique_congr
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
[PROOFSTEP]
simp only [and_congr_right_iff]
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)
[PROOFSTEP]
intro p hp
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n
[PROOFSTEP]
exact ⟨hp.dvd_of_dvd_pow, fun t => t.trans (dvd_pow_self _ hk)⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
[PROOFSTEP]
simp only [Nat.coprime_zero_left] at hab
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : b = 1
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : coprime a 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
[PROOFSTEP]
simp only [Nat.coprime_zero_right] at hab
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a = 1
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
refine'
  ⟨_, fun h =>
    Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a))) fun i =>
      i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b
[PROOFSTEP]
obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
[PROOFSTEP]
simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
  hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply, Finsupp.coe_add]
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
have : a.factorization p = 0 ∨ b.factorization p = 0 :=
  by
  rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ← Finset.mem_inter]
  intro t
  simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
[PROOFSTEP]
rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ← Finset.mem_inter]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ¬p ∈ (factorization a).support ∩ (factorization b).support
[PROOFSTEP]
intro t
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
t : p ∈ (factorization a).support ∩ (factorization b).support
⊢ False
[PROOFSTEP]
simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
this : ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
cases' this with h h
[GOAL]
case inr.inr.intro.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : ↑(factorization a) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
simp [h, imp_or]
[GOAL]
case inr.inr.intro.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
simp [h, imp_or]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : coprime 0 b
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
[PROOFSTEP]
simp only [Nat.coprime_zero_left] at hab
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : coprime a 0
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
[PROOFSTEP]
simp only [Nat.coprime_zero_right] at hab
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
ext n
[GOAL]
case inr.inr.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (divisors (a * b)) ↔ n ∈ Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true_iff, Ne.def, and_congr_left_iff,
  not_false_iff, Nat.mem_divisors, or_self_iff]
[GOAL]
case inr.inr.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
[PROOFSTEP]
apply hab.isPrimePow_dvd_mul


[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (x : α ⊕ β), x ∈ disjSum univ univ
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ disjSum univ univ
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ disjSum univ univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a : α
h : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)
[PROOFSTEP]
classical exact (Equiv.sumCompl (· = a)).bijective
[GOAL]
α : Type u_1
β : Type u_2
a : α
h : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)
[PROOFSTEP]
exact (Equiv.sumCompl (· = a)).bijective
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ = erase (image b univ) k
[PROOFSTEP]
apply subset_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ ⊆ erase (image b univ) k
[PROOFSTEP]
rw [image_subset_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ (x : { a // b a ≠ k }), x ∈ univ → b ↑x ∈ erase (image b univ) k
[PROOFSTEP]
intro i _
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ erase (image b univ) k
[PROOFSTEP]
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ erase (image b univ) k ⊆ image (fun i => b ↑i) univ
[PROOFSTEP]
intro i hi
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ i ∈ image (fun i => b ↑i) univ
[PROOFSTEP]
rw [mem_image]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
[PROOFSTEP]
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
[PROOFSTEP]
subst ha
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ erase (image b univ) k
⊢ ∃ a_1, a_1 ∈ univ ∧ b ↑a_1 = b a
[PROOFSTEP]
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊂ image b univ
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊆ image b univ
[PROOFSTEP]
intro x hx
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
⊢ x ∈ image b univ
[PROOFSTEP]
rcases mem_image.1 hx with ⟨y, _, hy⟩
[GOAL]
case left.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
y : { a // p (b a) }
left✝ : y ∈ univ
hy : b ↑y = x
⊢ x ∈ image b univ
[PROOFSTEP]
exact hy ▸ mem_image_of_mem b (mem_univ (y : α))
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ ¬image b univ ⊆ image (fun i => b ↑i) univ
[PROOFSTEP]
intro h
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rw [mem_image] at hk
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : ∃ a, a ∈ univ ∧ b a = k
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rcases hk with ⟨k', _, hk'⟩
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hk' : b k' = k
⊢ False
[PROOFSTEP]
subst hk'
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
⊢ False
[PROOFSTEP]
have := h (mem_image_of_mem b (mem_univ k'))
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : b k' ∈ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rw [mem_image] at this
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : ∃ a, a ∈ univ ∧ b ↑a = b k'
⊢ False
[PROOFSTEP]
rcases this with ⟨j, _, hj'⟩
[GOAL]
case right.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝¹ : k' ∈ univ
hp : ¬p (b k')
j : { a // p (b a) }
left✝ : j ∈ univ
hj' : b ↑j = b k'
⊢ False
[PROOFSTEP]
exact hp (hj' ▸ j.2)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
classical
induction' s using Finset.induction with a s has H generalizing f
· obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
  use e
  simp
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
obtain ⟨g', hg'⟩ := H hfst' hfs'
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
simp_rw [mem_insert]
rintro i (rfl | hi)
· simp
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
·
  exact
    ne_of_apply_ne Subtype.val
      (ne_of_eq_of_ne (hg' _ hi) <| hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
· exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
induction' s using Finset.induction with a s has H generalizing f
[GOAL]
case empty
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ ∃ g, ∀ (i : α), i ∈ ∅ → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Nonempty (α ≃ { x // x ∈ t })
[PROOFSTEP]
rwa [← Fintype.card_eq, Fintype.card_coe]
[GOAL]
case empty.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ { x // x ∈ t }
⊢ ∃ g, ∀ (i : α), i ∈ ∅ → ↑(↑g i) = f i
[PROOFSTEP]
use e
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ { x // x ∈ t }
⊢ ∀ (i : α), i ∈ ∅ → ↑(↑e i) = f i
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨g', hg'⟩ := H hfst' hfs'
[GOAL]
case insert.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
[GOAL]
case insert.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∀ (i : α), i ∈ insert a s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
simp_rw [mem_insert]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∀ (i : α), i = a ∨ i ∈ s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
rintro i (rfl | hi)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
s : Finset α
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
i : α
has : ¬i ∈ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f ↑(insert i s)
hfat : f i ∈ t
⊢ ↑(↑(g'.trans (Equiv.swap { val := f i, property := hfat } (↑g' i))) i) = f i
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
[GOAL]
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑g' i ≠ { val := f a, property := hfat }
[PROOFSTEP]
exact
  ne_of_apply_ne Subtype.val
    (ne_of_eq_of_ne (hg' _ hi) <| hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
[GOAL]
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑g' i ≠ ↑g' a
[PROOFSTEP]
exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
classical
let s' : Finset α := s.toFinset
have hfst' : s'.image f ⊆ t := by simpa [← Finset.coe_subset] using hfst
have hfs' : Set.InjOn f s' := by simpa using hfs
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
refine' ⟨g, fun i hi => _⟩
apply hg
simpa using hi
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
let s' : Finset α := s.toFinset
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
have hfst' : s'.image f ⊆ t := by simpa [← Finset.coe_subset] using hfst
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
⊢ Finset.image f s' ⊆ t
[PROOFSTEP]
simpa [← Finset.coe_subset] using hfst
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
have hfs' : Set.InjOn f s' := by simpa using hfs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
⊢ InjOn f ↑s'
[PROOFSTEP]
simpa using hfs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
refine' ⟨g, fun i hi => _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
i : α
hi : i ∈ s
⊢ ↑(↑g i) = f i
[PROOFSTEP]
apply hg
[GOAL]
case intro.a
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
i : α
hi : i ∈ s
⊢ i ∈ s'
[PROOFSTEP]
simpa using hi
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }
[PROOFSTEP]
classical
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
rw [Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }
[PROOFSTEP]
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
[PROOFSTEP]
rw [Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }
[PROOFSTEP]
classical
convert Fintype.card_congr (subtypeOrEquiv p q h)
simp
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }
[PROOFSTEP]
convert Fintype.card_congr (subtypeOrEquiv p q h)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
[PROOFSTEP]
refine' ⟨fun H => _, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
[GOAL]
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β
[PROOFSTEP]
contrapose! H
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
haveI := fintypeOfNotInfinite H.1
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
haveI := fintypeOfNotInfinite H.2
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
exact Infinite.false


[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
l : List ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ Quotient inferInstance
[PROOFSTEP]
refine'
  Quotient.liftOn₂ (f i (List.mem_cons_self _ _)) (Quotient.finChoiceAux l fun j h => f j (List.mem_cons_of_mem _ h)) _
    _
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ α i → ((i : ι) → i ∈ l → α i) → Quotient inferInstance
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ ∀ (a₁ : α i) (b₁ : (i : ι) → i ∈ l → α i) (a₂ : α i) (b₂ : (i : ι) → i ∈ l → α i),
    a₁ ≈ a₂ → b₁ ≈ b₂ → ?refine'_1 a₁ b₁ = ?refine'_1 a₂ b₂
[PROOFSTEP]
exact fun a l => ⟦fun j h => if e : j = i then by rw [e]; exact a else l _ ((List.mem_cons.1 h).resolve_left e)⟧
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l✝ : List ι
f : (i_1 : ι) → i_1 ∈ i :: l✝ → Quotient (S i_1)
a : α i
l : (i : ι) → i ∈ l✝ → α i
j : ι
h : j ∈ i :: l✝
e : j = i
⊢ α j
[PROOFSTEP]
rw [e]
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l✝ : List ι
f : (i_1 : ι) → i_1 ∈ i :: l✝ → Quotient (S i_1)
a : α i
l : (i : ι) → i ∈ l✝ → α i
j : ι
h : j ∈ i :: l✝
e : j = i
⊢ α i
[PROOFSTEP]
exact a
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ ∀ (a₁ : α i) (b₁ : (i : ι) → i ∈ l → α i) (a₂ : α i) (b₂ : (i : ι) → i ∈ l → α i),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ →
        (Quotient.mk inferInstance fun j h => if e : j = i then Eq.mpr (_ : α j = α i) a₁ else b₁ j (_ : j ∈ l)) =
          Quotient.mk inferInstance fun j h => if e : j = i then Eq.mpr (_ : α j = α i) a₂ else b₂ j (_ : j ∈ l)
[PROOFSTEP]
refine' fun a₁ l₁ a₂ l₂ h₁ h₂ => Quotient.sound fun j h => _
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
by_cases e : j = i
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : j = i
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
simp [e]
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ (if e : j = i then Eq.mpr (_ : α j = α i) a₁ else l₁ j (_ : j ∈ l)) ≈
    if e : j = i then Eq.mpr (_ : α j = α i) a₂ else l₂ j (_ : j ∈ l)
[PROOFSTEP]
simp [e]
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : α i = α j) a₁ ≈ cast (_ : α i = α j) a₂
[PROOFSTEP]
subst j
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
h : i ∈ i :: l
⊢ cast (_ : α i = α i) a₁ ≈ cast (_ : α i = α i) a₂
[PROOFSTEP]
exact h₁
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a₁ : α i
l₁ : (i : ι) → i ∈ l → α i
a₂ : α i
l₂ : (i : ι) → i ∈ l → α i
h₁ : a₁ ≈ a₂
h₂ : l₁ ≈ l₂
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ l₁ j (_ : j ∈ l) ≈ l₂ j (_ : j ∈ l)
[PROOFSTEP]
exact h₂ _ _
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (finChoiceAux (i :: l) fun i_1 h => Quotient.mk (S i_1) (f i_1 h)) = Quotient.mk inferInstance f
[PROOFSTEP]
simp [Quotient.finChoiceAux, Quotient.finChoiceAux_eq l, -Quotient.eq]
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (Quotient.mk inferInstance fun j h =>
      if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l))
      else f j (_ : j ∈ i :: l)) =
    Quotient.mk inferInstance f
[PROOFSTEP]
refine' Quotient.sound fun j h => _
[GOAL]
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
by_cases e : j = i
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
simp [e]
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ (if h : j = i then cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) else f j (_ : j ∈ i :: l)) ≈
    f j h
[PROOFSTEP]
simp [e]
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
try exact Setoid.refl _
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ f j (_ : j ∈ i :: l) ≈ f j h
[PROOFSTEP]
try exact Setoid.refl _
[GOAL]
case neg
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : ¬j = i
⊢ f j (_ : j ∈ i :: l) ≈ f j h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
j : ι
h : j ∈ i :: l
e : j = i
⊢ cast (_ : (fun i => α i) i = (fun i => α i) j) (f i (_ : i ∈ i :: l)) ≈ f j h
[PROOFSTEP]
subst j
[GOAL]
case pos
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
i : ι
l : List ι
f : (i_1 : ι) → i_1 ∈ i :: l → α i_1
h : i ∈ i :: l
⊢ cast (_ : (fun i => α i) i = (fun i => α i) i) (f i (_ : i ∈ i :: l)) ≈ f i h
[PROOFSTEP]
exact Setoid.refl _
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
l : Multiset ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
have := fun a => Quotient.finChoiceAux_eq a fun i _ => Quotient.out (f i)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this :
  ∀ (a : List ι),
    (finChoiceAux a fun i h => Quotient.mk (S i) (out (f i))) = Quotient.mk inferInstance fun i x => out (f i)
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
simp [Quotient.out_eq] at this
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
⊢ (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸ (fun l => finChoiceAux l fun i x => f i) a =
    (fun l => finChoiceAux l fun i x => f i) b
[PROOFSTEP]
simp [this]
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
⊢ ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i)) =
    Quotient.mk inferInstance fun i x => out (f i)
[PROOFSTEP]
let g := fun a : Multiset ι => (⟦fun (i : ι) (_ : i ∈ a) => Quotient.out (f i)⟧ : Quotient (by infer_instance))
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a✝ b : List ι
h : a✝ ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
a : Multiset ι
⊢ Setoid ((i : ι) → i ∈ a → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i)) =
    Quotient.mk inferInstance fun i x => out (f i)
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case h
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq
    ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i))
    (Quotient.mk inferInstance fun i x => out (f i))
[PROOFSTEP]
trans (g a)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq
    ((_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
      Quotient.mk inferInstance fun i x => out (f i))
    (g ↑a)
[PROOFSTEP]
exact eq_rec_heq (φ := fun l : Multiset ι => @Quotient (∀ i ∈ l, α i) (by infer_instance)) (Quotient.sound h) (g a)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
l : Multiset ι
⊢ Setoid ((i : ι) → i ∈ l → α i)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq (g ↑a) (Quotient.mk inferInstance fun i x => out (f i))
[PROOFSTEP]
change HEq (g a) (g b)
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ HEq (g ↑a) (g ↑b)
[PROOFSTEP]
congr 1
[GOAL]
case e_1
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : List ι
h : a ≈ b
this : ∀ (a : List ι), (finChoiceAux a fun i h => f i) = Quotient.mk inferInstance fun i x => out (f i)
g : (a : Multiset ι) → Quotient inferInstance := fun a => Quotient.mk inferInstance fun i x => out (f i)
⊢ ↑a = ↑b
[PROOFSTEP]
exact Quotient.sound h
[GOAL]
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Type u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a b : (i : ι) → i ∈ Finset.univ.val → α i
h : a ≈ b
i : ι
⊢ a i (_ : i ∈ Finset.univ) ≈ b i (_ : i ∈ Finset.univ)
[PROOFSTEP]
apply h
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ (finChoice fun i => Quotient.mk (inst✝ i) (f i)) = Quotient.mk inferInstance f
[PROOFSTEP]
dsimp only [Quotient.finChoice]
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.liftOn
      (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
        (_ :
          ∀ (a b : List ι) (h : a ≈ b),
            (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
                (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
      (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
      (_ :
        ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
          a ≈ b →
            (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
              Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ)) =
    Quotient.mk inferInstance f
[PROOFSTEP]
conv_lhs =>
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
| Quotient.liftOn
    (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
    (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
    (_ :
      ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
        a ≈ b →
          (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
            Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ))
[PROOFSTEP]
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
| Quotient.liftOn
    (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
    (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
    (_ :
      ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
        a ≈ b →
          (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
            Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ))
[PROOFSTEP]
  enter [1]
  tactic =>
    change _ = ⟦fun i _ => f i⟧
    exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
| Quotient.liftOn
    (Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b))
    (fun f => Quotient.mk inferInstance fun i => f i (_ : i ∈ Finset.univ))
    (_ :
      ∀ (a b : (i : ι) → i ∈ Finset.univ.val → α i),
        a ≈ b →
          (Quotient.mk inferInstance fun i => a i (_ : i ∈ Finset.univ)) =
            Quotient.mk inferInstance fun i => b i (_ : i ∈ Finset.univ))
[PROOFSTEP]
enter [1]
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
| Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
    (_ :
      ∀ (a b : List ι) (h : a ≈ b),
        (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
          (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b)
[PROOFSTEP]
tactic =>
  change _ = ⟦fun i _ => f i⟧
  exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b) =
    ?m.23336
[PROOFSTEP]
change _ = ⟦fun i _ => f i⟧
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
α : ι → Type u_2
inst✝ : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i))
      (_ :
        ∀ (a b : List ι) (h : a ≈ b),
          (_ : Quotient.mk (List.isSetoid ι) a = Quotient.mk (List.isSetoid ι) b) ▸
              (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) a =
            (fun l => finChoiceAux l fun i x => Quotient.mk (inst✝ i) (f i)) b) =
    Quotient.mk inferInstance fun i x => f i
[PROOFSTEP]
exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
[PROOFSTEP]
rw [Subsingleton.elim emb Embedding.fintype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
[PROOFSTEP]
refine'
  Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) (fun α₁ α₂ h₂ e ih ↦ ?_) (?_)
    (fun γ h ih ↦ ?_) α
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₂
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) PEmpty
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) (Option γ)
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖PEmpty ↪ β‖ = descFactorial ‖β‖ ‖PEmpty‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
letI := Fintype.ofEquiv _ e.symm
[GOAL]
case refine'_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
this : Fintype α₁ := ofEquiv α₂ e.symm
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
[GOAL]
case refine'_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty ↪ β‖ = descFactorial ‖β‖ ‖PEmpty‖
[PROOFSTEP]
rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
[GOAL]
case refine'_2
β : Type u_2
inst✝ : Fintype β
⊢ ∃ x, ∀ (y : PEmpty ↪ β), y = x
[PROOFSTEP]
exact ⟨Embedding.ofIsEmpty, fun x ↦ FunLike.ext _ _ isEmptyElim⟩
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
classical
dsimp only at ih
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β), card_sigma, ← ih]
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_comm]
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
dsimp only at ih
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = descFactorial ‖β‖ ‖γ‖
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β), card_sigma, ← ih]
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = descFactorial ‖β‖ ‖γ‖
⊢ ∑ a : γ ↪ β, ‖↑(Set.range ↑a)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
[PROOFSTEP]
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_comm]


[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in s, (f i)! ∣ (∑ i in s, f i)!
[PROOFSTEP]
classical
induction' s using Finset.induction with a' s' has ih
· simp only [Finset.sum_empty, Finset.prod_empty, factorial]
· simp only [Finset.prod_insert has, Finset.sum_insert has]
  refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
  apply Nat.factorial_mul_factorial_dvd_factorial_add
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in s, (f i)! ∣ (∑ i in s, f i)!
[PROOFSTEP]
induction' s using Finset.induction with a' s' has ih
[GOAL]
case empty
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in ∅, (f i)! ∣ (∑ i in ∅, f i)!
[PROOFSTEP]
simp only [Finset.sum_empty, Finset.prod_empty, factorial]
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ ∏ i in insert a' s', (f i)! ∣ (∑ i in insert a' s', f i)!
[PROOFSTEP]
simp only [Finset.prod_insert has, Finset.sum_insert has]
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ (f a')! * ∏ i in s', (f i)! ∣ (f a' + ∑ i in s', f i)!
[PROOFSTEP]
refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ (f a')! * (∑ i in s', f i)! ∣ (f a' + ∑ i in s', f i)!
[PROOFSTEP]
apply Nat.factorial_mul_factorial_dvd_factorial_add


[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(ascFactorial a b) = Polynomial.eval (↑a + 1) (pochhammer S b)
[PROOFSTEP]
rw [← pochhammer_nat_eq_ascFactorial, pochhammer_eval_cast, Nat.cast_add, Nat.cast_one]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer S b)
[PROOFSTEP]
rw [← pochhammer_eval_cast, pochhammer_nat_eq_descFactorial]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
[PROOFSTEP]
induction' b with b
[GOAL]
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a zero) = ↑(descFactorial (a - (zero - 1) + zero - 1) zero)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - (succ b - 1) + succ b - 1) (succ b))
[PROOFSTEP]
simp_rw [add_succ, succ_sub_one]
[GOAL]
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : a ≤ b
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : a ≤ b
⊢ a - b + b ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr h, zero_add]
[GOAL]
case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : b ≤ a
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
rw [tsub_add_cancel_of_le h]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑a ! = Polynomial.eval 1 (pochhammer S a)
[PROOFSTEP]
rw [← zero_ascFactorial, cast_ascFactorial, cast_zero, zero_add]
[GOAL]
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ ↑(descFactorial a 2) = ↑a * (↑a - 1)
[PROOFSTEP]
rw [cast_descFactorial]
[GOAL]
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (pochhammer S 2) = ↑a * (↑a - 1)
[PROOFSTEP]
cases a
[GOAL]
case zero
S : Type u_1
inst✝ : Ring S
b : ℕ
⊢ Polynomial.eval (↑(zero - (2 - 1))) (pochhammer S 2) = ↑zero * (↑zero - 1)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u_1
inst✝ : Ring S
b n✝ : ℕ
⊢ Polynomial.eval (↑(succ n✝ - (2 - 1))) (pochhammer S 2) = ↑(succ n✝) * (↑(succ n✝) - 1)
[PROOFSTEP]
rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel, pochhammer_succ_right, pochhammer_one, Polynomial.X_mul,
  Polynomial.eval_mul_X, Polynomial.eval_add, Polynomial.eval_X, cast_one, Polynomial.eval_one]


[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : α → Type u_5
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
x✝ : Sigma β
a : α
b : β a
⊢ { fst := a, snd := b } ∈ Finset.sigma univ fun x => univ
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(choose n r) ≤ ↑(n ^ r) / ↑r !
[PROOFSTEP]
rw [le_div_iff']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑r ! * ↑(choose n r) ≤ ↑(n ^ r)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ r ! * choose n r ≤ n ^ r
[PROOFSTEP]
rw [← Nat.descFactorial_eq_factorial_mul_choose]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ descFactorial n r ≤ n ^ r
[PROOFSTEP]
exact n.descFactorial_le_pow r
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !
[PROOFSTEP]
exact_mod_cast r.factorial_pos
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑((n + 1 - r) ^ r) / ↑r ! ≤ ↑(choose n r)
[PROOFSTEP]
rw [div_le_iff']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑((n + 1 - r) ^ r) ≤ ↑r ! * ↑(choose n r)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * choose n r
[PROOFSTEP]
rw [← Nat.descFactorial_eq_factorial_mul_choose]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ descFactorial n r
[PROOFSTEP]
exact n.pow_sub_le_descFactorial r
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !
[PROOFSTEP]
exact_mod_cast r.factorial_pos