-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_reciprocal (n : ℕ) :
    commProb (Product (reciprocalFactors n)) = 1 / n

Proof state:
case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Tactic:
have := hn.pos.ne'

Result:
case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this✝ : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
this : n % 4 ≠ 0
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Proof state:
case neg
n : ℕ
h0 : ¬n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
by_cases h1 : n = 1

Result:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
have key : n % 4 = 1 ∨ n % 4 = 3 := Nat.odd_mod_four_iff.mp (Nat.odd_iff.mp h2)

Result:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Proof state:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (n % 4) ^ 2 + 3 = n % 4 * 4
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

Tactic:
have h1 := (Nat.div_add_mod n 4).symm

Result:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1✝ : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (n % 4) ^ 2 + 3 = n % 4 * 4
h1 : n = 4 * (n / 4) + n % 4
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

Tactic:
have h0 : (n % 4) ^ 2 + 3 = n % 4 * 4 := by rcases key with h | h <;> rw [h] <;> norm_num

Result:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (n % 4) ^ 2 + 3 = n % 4 * 4
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

Proof state:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2),
    commProb_odd (by decide)]

Result:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ (↑3 + 3) / (4 * ↑3) * (1 / ↑(n / 2)) = 1 / ↑n

Proof state:
n : ℕ
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
by_cases h0 : n = 0

Result:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

case neg
n : ℕ
h0 : ¬n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Proof state:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) = 0

Tactic:
apply commProb_eq_zero_of_infinite

Result:
no goals

Proof state:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ (n % 4) ^ 2 + 3 = n % 4 * 4

Tactic:
rcases key with h | h <;> rw [h] <;> norm_num

Result:
no goals

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rw [reciprocalFactors_odd h1 h2, commProb_cons, commProb_reciprocal (n / 4 + 1)]

Result:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
rw [commProb_odd (hn.mul h2), div_mul_div_comm, mul_one, div_eq_div_iff, one_mul] <;> norm_cast

Result:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Proof state:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
⊢ Odd (n % 4)

Tactic:
rcases key with h | h <;> rw [h] <;> decide

Result:
no goals

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
have hn : Odd (n % 4) := by rcases key with h | h <;> rw [h] <;> decide

Result:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Proof state:
case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rcases Nat.even_or_odd n with h2 | h2

Result:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Proof state:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ (3 + 3) * 2 = 4 * 3

Tactic:
norm_num

Result:
no goals

Proof state:
case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this✝ : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
this : n % 4 ≠ 0
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Tactic:
positivity

Result:
no goals

Proof state:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ (↑3 + 3) / (4 * ↑3) * (1 / ↑(n / 2)) = 1 / ↑n

Tactic:
field_simp [h0, h2.two_dvd]

Result:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ (3 + 3) * 2 = 4 * 3

Proof state:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]

Result:
no goals

Proof state:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
have := div_two_lt h0

Result:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Proof state:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1✝ : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (n % 4) ^ 2 + 3 = n % 4 * 4
h1 : n = 4 * (n / 4) + n % 4
⊢ (n % 4 * n + 3) * n = 4 * (n % 4 * n) * (n / 4 + 1)

Tactic:
zify at h0 h1 ⊢

Result:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1✝ : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (↑n % 4) ^ 2 + 3 = ↑n % 4 * 4
h1 : ↑n = 4 * (↑n / 4) + ↑n % 4
⊢ (↑n % 4 * ↑n + 3) * ↑n = 4 * (↑n % 4 * ↑n) * (↑n / 4 + 1)

Proof state:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
have := div_four_lt h0 h1

Result:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Proof state:
case neg.inr
n : ℕ
h0✝ : ¬n = 0
h1✝ : ¬n = 1
h2 : Odd n
this : n / 4 + 1 < n
key : n % 4 = 1 ∨ n % 4 = 3
hn : Odd (n % 4)
h0 : (↑n % 4) ^ 2 + 3 = ↑n % 4 * 4
h1 : ↑n = 4 * (↑n / 4) + ↑n % 4
⊢ (↑n % 4 * ↑n + 3) * ↑n = 4 * (↑n % 4 * ↑n) * (↑n / 4 + 1)

Tactic:
linear_combination (h0 + h1 * (n % 4)) * n

Result:
no goals

Proof state:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rw [h0, reciprocalFactors_zero, commProb_cons, commProb_nil, mul_one, Nat.cast_zero, div_zero]

Result:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) = 0