awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ IsMulCommutative M
have haveI : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
Tactic: classical
  haveI := Fintype.ofFinite M
  rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
  · exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
haveI haveI₁ haveI₂ : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
⊢ commProb M = 1 ↔ IsMulCommutative M
have haveI₃ : ∀ (this : Fintype M),
  (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 = 1 ↔
    IsMulCommutative M
Tactic: classical
  haveI := Fintype.ofFinite M
  rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
  · exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
haveI haveI₁ haveI₂ : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
haveI₃ :
  ∀ (this : Fintype M),
    (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 =
        1 ↔
      IsMulCommutative M
⊢ commProb M = 1 ↔ IsMulCommutative M
have haveI₄ : ∀ (this : Fintype M),
  (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M
Tactic: classical
  haveI := Fintype.ofFinite M
  rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
  · exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
haveI haveI₁ haveI₂ : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
haveI₃ :
  ∀ (this : Fintype M),
    (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 =
        1 ↔
      IsMulCommutative M
haveI₄ :
  ∀ (this : Fintype M),
    (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M
⊢ commProb M = 1 ↔ IsMulCommutative M
have haveI₅ : ∀ (this : Fintype M), HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0
Tactic: classical
  haveI := Fintype.ofFinite M
  rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
  · exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
⊢ commProb G = HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have rw : HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
    HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
  HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
Tactic: rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have pos : ∀ (h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0),
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
Tactic: by_cases h : (Nat.card G : ℚ) = 0
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
pos :
  ∀ (h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0),
    HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
        HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
      HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have neg : ∀ (h : ¬Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0),
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
Tactic: by_cases h : (Nat.card G : ℚ) = 0
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have pos : HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / HMul.hMul (α := ℚ) 0 0 =
  HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
Tactic: rw [h, zero_mul, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0
pos :
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / HMul.hMul (α := ℚ) 0 0 =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have pos₁ : HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / 0 =
  HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
Tactic: rw [h, zero_mul, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0
pos :
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / HMul.hMul (α := ℚ) 0 0 =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
pos₁ :
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / 0 =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have pos₂ : 0 = HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
Tactic: rw [h, zero_mul, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
h : Eq (α := ℚ) (↑(Nat.card G) : ℚ) 0
pos :
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / HMul.hMul (α := ℚ) 0 0 =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
pos₁ :
  HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0 / 0 =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
pos₂ : 0 = HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ) /
      HMul.hMul (α := ℚ) (↑(Nat.card G) : ℚ) (↑(Nat.card G) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(Nat.card.{u_2} (ConjClasses G)) : ℚ) (↑(Nat.card G) : ℚ)
have pos₃ : Eq (α := ℚ) 0 0
Tactic: rw [h, zero_mul, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ commProb.{u_2} ↥H ≤ commProb G * HPow.hPow (α := ℚ) (β := ℕ) (↑H.index : ℚ) 2
have rw : Nat.card.{u_2} { p : ↥H × ↥H // Commute p.1 p.2 } ≤ Nat.card.{u_2} { p : G × G // Commute p.1 p.2 }
Tactic: rw [commProb_def, commProb_def, div_le_iff₀, mul_assoc, ← mul_pow, ← Nat.cast_mul,
    mul_comm H.index, H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
rw : Nat.card.{u_2} { p : ↥H × ↥H // Commute p.1 p.2 } ≤ Nat.card.{u_2} { p : G × G // Commute p.1 p.2 }
⊢ commProb.{u_2} ↥H ≤ commProb G * HPow.hPow (α := ℚ) (β := ℕ) (↑H.index : ℚ) 2
have h : HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card G) : ℚ) 2 ≠ 0
Tactic: rw [commProb_def, commProb_def, div_le_iff₀, mul_assoc, ← mul_pow, ← Nat.cast_mul,
    mul_comm H.index, H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
rw : Nat.card.{u_2} { p : ↥H × ↥H // Commute p.1 p.2 } ≤ Nat.card.{u_2} { p : G × G // Commute p.1 p.2 }
h : HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card G) : ℚ) 2 ≠ 0
⊢ commProb.{u_2} ↥H ≤ commProb G * HPow.hPow (α := ℚ) (β := ℕ) (↑H.index : ℚ) 2
have rw₁ : 0 < HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card.{u_2} ↥H) : ℚ) 2
Tactic: rw [commProb_def, commProb_def, div_le_iff₀, mul_assoc, ← mul_pow, ← Nat.cast_mul,
    mul_comm H.index, H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ Nat.card.{u_2} { p : ↥H × ↥H // Commute p.1 p.2 } ≤ Nat.card.{u_2} { p : G × G // Commute p.1 p.2 }
have refine : Function.Injective (β := { p : G × G // Commute p.1 p.2 }) fun (p : { p : ↥H × ↥H // Commute p.1 p.2 }) ↦
  Subtype.mk (p := fun (p : G × G) ↦ Commute p.1 p.2) ((↑(↑p : ↥H × ↥H).1 : G), (↑(↑p : ↥H × ↥H).2 : G)) sorry
Tactic: refine Nat.card_le_card_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ commProb.{u_2} (G ⧸ H) ≤ commProb G * (↑(Nat.card.{u_2} ↥H) : ℚ)
have rw : Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)
Tactic: rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
    H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
rw : Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)
⊢ commProb.{u_2} (G ⧸ H) ≤ commProb G * (↑(Nat.card.{u_2} ↥H) : ℚ)
have h : Ne (α := ℚ) (↑(Nat.card G) : ℚ) 0
Tactic: rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
    H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
rw : Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)
h : Ne (α := ℚ) (↑(Nat.card G) : ℚ) 0
⊢ commProb.{u_2} (G ⧸ H) ≤ commProb G * (↑(Nat.card.{u_2} ↥H) : ℚ)
have rw₁ : LT.lt (α := ℚ) 0 (↑(Nat.card.{u_2} (G ⧸ H)) : ℚ)
Tactic: rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
    H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)
have hf : Function.Surjective (β := ConjClasses (G ⧸ H)) (ConjClasses.map (QuotientGroup.mk' H))
Tactic: apply Nat.card_le_card_of_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
hf : Function.Surjective (β := ConjClasses (G ⧸ H)) (ConjClasses.map (QuotientGroup.mk' H))
⊢ Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)
have f : ConjClasses G → ConjClasses (G ⧸ H)
Tactic: apply Nat.card_le_card_of_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
⊢ commProb (DihedralGroup n) = HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
have rw : HDiv.hDiv (α := ℚ) (↑((n + 3) / 2) : ℚ) (↑(2 * n) : ℚ) = HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
Tactic: rw [commProb_def', DihedralGroup.card_conjClasses_odd hn, nat_card]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
⊢ 2 ∣ n + 3
have rw : (n + 3) % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
rw : (n + 3) % 2 = 0
⊢ 2 ∣ n + 3
have rw₁ : (n % 2 + HMod.hMod (α := ℕ) 3 2) % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
rw : (n + 3) % 2 = 0
rw₁ : (n % 2 + HMod.hMod (α := ℕ) 3 2) % 2 = 0
⊢ 2 ∣ n + 3
have rw₂ : (1 + HMod.hMod (α := ℕ) 3 2) % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
⊢ HDiv.hDiv (α := ℚ) (↑((n + 3) / 2) : ℚ) (↑(2 * n) : ℚ) = HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
have qify : HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 / HMul.hMul (α := ℚ) 2 (↑n : ℚ) =
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
Tactic: qify [show 2 ∣ n + 3 by rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 / HMul.hMul (α := ℚ) 2 (↑n : ℚ) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
have rw : HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / (HMul.hMul (α := ℚ) 2 2 * (↑n : ℚ)) =
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
Tactic: rw [div_div, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
hn : Odd n
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / (HMul.hMul (α := ℚ) 2 2 * (↑n : ℚ)) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
have e_a : HMul.hMul (α := ℚ) 2 2 = 4
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
⊢ reciprocalFactors 0 = [0]
have unfold : Eq (α := List ℕ)
  (if x : Eq (α := ℕ) 0 0 then [0]
  else
    if x : Eq (α := ℕ) 0 1 then []
    else
      if Even (α := ℕ) 0 then 3 :: reciprocalFactors (0 / 2)
      else HMod.hMod (α := ℕ) 0 4 * 0 :: reciprocalFactors (0 / 4 + 1))
  [0]
Tactic: unfold reciprocalFactors
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
⊢ reciprocalFactors 1 = []
have unfold : Eq (α := List ℕ)
  (if x : Eq (α := ℕ) 1 0 then [0]
  else
    if x : Eq (α := ℕ) 1 1 then []
    else
      if Even (α := ℕ) 1 then 3 :: reciprocalFactors (1 / 2)
      else HMod.hMod (α := ℕ) 1 4 * 1 :: reciprocalFactors (1 / 4 + 1))
  []
Tactic: unfold reciprocalFactors
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (hypothesis)
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
have h1 : n ≠ 1
Tactic: have h1 : n ≠ 1 := by
    rintro rfl
    norm_num at h2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
have rw : (if x : n = 0 then [0]
  else
    if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  3 :: reciprocalFactors (n / 2)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
have rw₁ : (if x : n = 1 then []
  else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  3 :: reciprocalFactors (n / 2)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
rw₁ :
  (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
have rw₂ : (if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  3 :: reciprocalFactors (n / 2)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
rw₁ :
  (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
rw₂ :
  (if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
have rw₃ : 3 :: reciprocalFactors (n / 2) = 3 :: reciprocalFactors (n / 2)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (hypothesis)
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
have h0 : n ≠ 0
Tactic: have h0 : n ≠ 0 := by
    rintro rfl
    norm_num [← Nat.not_even_iff_odd] at h2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
have rw : (if x : n = 0 then [0]
  else
    if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  n % 4 * n :: reciprocalFactors (n / 4 + 1)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
have rw₁ : (if x : n = 1 then []
  else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  n % 4 * n :: reciprocalFactors (n / 4 + 1)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
rw₁ :
  (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
have rw₂ : (if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
  n % 4 * n :: reciprocalFactors (n / 4 + 1)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
rw :
  (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
rw₁ :
  (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
rw₂ :
  (if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
have rw₃ : n % 4 * n :: reciprocalFactors (n / 4 + 1) = n % 4 * n :: reciprocalFactors (n / 4 + 1)
Tactic: rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos : ∀ (h0 : n = 0), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: by_cases h0 : n = 0
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
pos : ∀ (h0 : n = 0), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : ∀ (h0 : ¬n = 0), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: by_cases h0 : n = 0
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos : commProb (DihedralGroup 0) = 0
Tactic: rw [h0, reciprocalFactors_zero, commProb_cons, commProb_nil, mul_one, Nat.cast_zero, div_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos : ∀ (h1 : n = 1), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
pos : ∀ (h1 : n = 1), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : ∀ (h1 : ¬n = 1), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos : commProb (Product (reciprocalFactors 1)) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
Tactic: rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]