awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
⊢ Nat.card { p : (M × M') × M × M' // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card (Prod.{u_1, u_2} { p : M × M // p.1 * p.2 = p.2 * p.1 } { p : M' × M' // p.1 * p.2 = p.2 * p.1 })

Tactic:
Nat.card_congr ⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩,
    fun x => ⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩

Premises used: Equiv.mk, Prod.mk, Prod.fst, Subtype.mk, Nat.card_congr, And.right, And.left, And.intro, Subtype.val, Prod.snd, rfl, Subtype.property
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
M' : Type u_2
inst_1 : Mul M'
⊢ Nat.card { p : (M × M') × M × M' // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card (Prod.{u_1, u_2} { p : M × M // p.1 * p.2 = p.2 * p.1 } { p : M' × M' // p.1 * p.2 = p.2 * p.1 })

Tactic:
exact Nat.card_congr ⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩,
    fun x => ⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩

Premises used: Equiv.mk, Nat.card_congr
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
simp_rw :
  (↑(Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2 =
    (↑(Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2
⊢ commProb ((a : α) → i a) = ∏ a : α, commProb.{u_3} (i a)

Tactic:
simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod,
    ← Nat.card_pi, Commute, SemiconjBy, funext_iff]

Premises used: SemiconjBy, funext_iff, Commute, Nat.cast_prod, Nat.card_pi, Finset.prod_pow, Finset.prod_div_distrib, commProb_def
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
e_a :
  Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } =
    Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })
⊢ (↑(Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2 =
    (↑(Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })) : ℚ) /
      HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card ((a : α) → i a)) : ℚ) 2

Tactic:
congr 2
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
⊢ Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } =
    Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })

Tactic:
Nat.card_congr ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1,
    fun a => (x a).1.2⟩, fun a => (x a).2⟩, fun x => rfl, fun x => rfl⟩

Premises used: Equiv.mk, Prod.mk, Prod.fst, Subtype.mk, Nat.card_congr, Subtype.val, Prod.snd, rfl, Subtype.property
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
α : Type u_2
i : α → Type u_3
inst : Fintype α
inst_1 : (a : α) → Mul (i a)
⊢ Nat.card { p : ((a : α) → i a) × ((a : α) → i a) // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } =
    Nat.card ((a : α) → { p : i a × i a // p.1 * p.2 = p.2 * p.1 })

Tactic:
exact Nat.card_congr ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1,
    fun a => (x a).1.2⟩, fun a => (x a).2⟩, fun x => rfl, fun x => rfl⟩

Premises used: Equiv.mk, Nat.card_congr
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Mul β
rw : ∏ a : α, commProb β = commProb β ^ card α
rw₁ : commProb β ^ Finset.card.{u_2} (α := α) Finset.univ = commProb β ^ card α
rw₂ rw₃ : commProb β ^ card α = commProb β ^ card α
⊢ commProb (α → β) = commProb β ^ card α

Tactic:
rw [commProb_pi, Finset.prod_const, Finset.card_univ]

Premises used: Finset.card_univ, Finset.prod_const, commProb_pi
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Infinite M
⊢ commProb M = 0

Tactic:
div_eq_zero_iff.2 (Or.inl (Nat.cast_eq_zero.2 Nat.card_eq_zero_of_infinite))

Premises used: Iff.mpr, Nat.card_eq_zero_of_infinite, commProb, Nat.cast_eq_zero, Or.inl, div_eq_zero_iff
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
⊢ 0 < commProb M

Tactic:
h.elim fun x ↦
    div_pos (Nat.cast_pos.mpr (Finite.card_pos_iff.mpr ⟨⟨(x, x), rfl⟩⟩))
      (pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2)

Premises used: Iff.mpr, pow_pos, Nat.cast_pos, Nonempty.elim, Prod.mk, Nonempty.intro, Subtype.mk, Finite.card_pos_iff, div_pos, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
⊢ commProb M ≤ 1

Tactic:
div_le_one_of_le₀ ?_ (sq_nonneg (Nat.card M : ℚ))

Premises used: div_le_one_of_le₀, Nat.card, Nat.cast, commProb, sq_nonneg
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
refine : (↑(Nat.card.{u_1} { p : M × M // Commute p.1 p.2 }) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2
⊢ commProb M ≤ 1

Tactic:
refine div_le_one_of_le₀ ?_ (sq_nonneg (Nat.card M : ℚ))

Premises used: div_le_one_of_le₀, Nat.card, Nat.cast, sq_nonneg
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
norm_cast : Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ HPow.hPow (β := ℕ) (Nat.card M) 2
⊢ (↑(Nat.card.{u_1} { p : M × M // Commute p.1 p.2 }) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card M) : ℚ) 2

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
rw : Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ Nat.card.{u_1} (M × M)
⊢ Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ HPow.hPow (β := ℕ) (Nat.card M) 2

Tactic:
rw [sq, ← Nat.card_prod]

Premises used: sq, Nat.card_prod
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
⊢ Nat.card.{u_1} { p : M × M // Commute p.1 p.2 } ≤ Nat.card.{u_1} (M × M)

Tactic:
apply Finite.card_subtype_le

Premises used: Finite.card_subtype_le
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
haveI : ∀ (this : Fintype M), commProb M = 1 ↔ IsMulCommutative M
⊢ commProb M = 1 ↔ IsMulCommutative M

Tactic:
haveI := Fintype.ofFinite M
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
rw :
  (↑(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

Tactic:
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]

Premises used: commProb, Set.coe_setOf, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
rw : (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M
rw₁ : HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0
⊢ (↑(card.{u_1} (↑{x : M × M | Commute x.1 x.2} : Type u_1)) : ℚ) / HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 = 1 ↔
    IsMulCommutative M

Tactic:
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]

Premises used: set_fintype_card_eq_univ_iff, div_eq_one_iff_eq, Set.eq_univ_iff_forall, sq, Nat.cast_inj, Fintype.card_prod, Nat.cast_pow
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M

Tactic:
⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩

Premises used: Prod.mk, Prod.fst, mul_comm', Iff.intro, IsMulCommutative.mk, Std.Commutative.mk, Prod.snd
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), Membership.mem (γ := Set (M × M)) {x : M × M | Commute x.1 x.2} x) ↔ IsMulCommutative M

Tactic:
exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0

Tactic:
pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)

Premises used: Iff.mpr, pow_ne_zero, Fintype.card_ne_zero, OfNat.ofNat, Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
M : Type u_1
inst : Mul M
inst_1 : Finite M
h : Nonempty M
this : Fintype M
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)

Premises used: pow_ne_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CommutingProbability
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
haveI₅ haveI₆ : ∀ (this : Fintype M), HPow.hPow (α := ℚ) (β := ℕ) (↑(card M) : ℚ) 2 ≠ 0
⊢ 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)

Premises used: set_fintype_card_eq_univ_iff, div_eq_one_iff_eq, Set.eq_univ_iff_forall, pow_ne_zero, sq, Nat.cast_inj, Fintype.card_prod, commProb, Set.coe_setOf, Nat.cast_pow, OfNat.ofNat, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
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) : ℚ)
⊢ commProb 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]

Premises used: card_comm_eq_card_conjClasses_mul_card, sq, commProb, Nat.cast_mul
-- Module: Mathlib.GroupTheory.CommutingProbability
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) : ℚ)
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) : ℚ)
⊢ 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

Premises used: Nat.card, Nat.cast
-- Module: Mathlib.GroupTheory.CommutingProbability
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
pos₃ pos₄ : Eq (α := ℚ) 0 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:
rw [h, zero_mul, div_zero, div_zero]

Premises used: MulZeroClass.zero_mul, div_zero
-- Module: Mathlib.GroupTheory.CommutingProbability
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) : ℚ)

Tactic:
mul_div_mul_right _ _ h

Premises used: mul_div_mul_right
-- Module: Mathlib.GroupTheory.CommutingProbability
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) : ℚ)

Tactic:
exact mul_div_mul_right _ _ h

Premises used: mul_div_mul_right
-- Module: Mathlib.GroupTheory.CommutingProbability
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
rw₁ : 0 < HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card.{u_2} ↥H) : ℚ) 2
⊢ commProb.{u_2} ↥H ≤ commProb G * HPow.hPow (α := ℚ) (β := ℕ) (↑H.index : ℚ) 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]

Premises used: div_le_iff₀, div_mul_cancel₀, mul_assoc, Nat.cast_mul, Subgroup.index, mul_comm, Nat.cast_le, Subgroup.card_mul_index, mul_pow, commProb_def
-- Module: Mathlib.GroupTheory.CommutingProbability
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 }

Tactic:
Nat.card_le_card_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_

Premises used: Nat.card_le_card_of_injective, Prod.mk, Prod.fst, Subtype.ext_iff, Subtype.mk, Iff.mp, Subtype.val, Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
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)) ⋯
⊢ 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:
refine Nat.card_le_card_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_

Premises used: Nat.card_le_card_of_injective
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
p q : { p : ↥H × ↥H // Commute p.1 p.2 }
h :
  Eq.{u_2 + 1} (α := { 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)) ⋯ :
          { p : G × G // Commute p.1 p.2 }))
      p)
    ((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)) ⋯ :
          { p : G × G // Commute p.1 p.2 }))
      q)
⊢ p = q

Tactic:
simpa only [Subtype.ext_iff, Prod.ext_iff] using h

Premises used: Prod.ext_iff, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ 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)) ⋯

Tactic:
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card G) : ℚ) 2 ≠ 0

Tactic:
pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')

Premises used: Iff.mpr, pow_ne_zero, Finite.card_pos, LT.lt.ne', OfNat.ofNat, Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card G) : ℚ) 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')

Premises used: pow_ne_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ 0 < HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card.{u_2} ↥H) : ℚ) 2

Tactic:
pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2

Premises used: pow_pos, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
⊢ 0 < HPow.hPow (α := ℚ) (β := ℕ) (↑(Nat.card.{u_2} ↥H) : ℚ) 2

Tactic:
exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2

Premises used: pow_pos, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CommutingProbability
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
rw₁ : LT.lt (α := ℚ) 0 (↑(Nat.card.{u_2} (G ⧸ H)) : ℚ)
⊢ commProb.{u_2} (G ⧸ H) ≤ commProb G * (↑(Nat.card.{u_2} ↥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]

Premises used: div_le_iff₀, div_mul_cancel₀, mul_assoc, Nat.cast_mul, Subgroup.index, Nat.cast_le, commProb_def', Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.CommutingProbability
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))
f : ConjClasses G → ConjClasses (G ⧸ H)
⊢ Nat.card.{u_2} (ConjClasses (G ⧸ H)) ≤ Nat.card.{u_2} (ConjClasses G)

Tactic:
apply Nat.card_le_card_of_surjective

Premises used: Nat.card_le_card_of_surjective
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ Function.Surjective (β := ConjClasses (G ⧸ H)) (ConjClasses.map (QuotientGroup.mk' H))

Tactic:
ConjClasses.map_surjective Quotient.mk''_surjective

Premises used: Quotient.mk''_surjective, ConjClasses.map_surjective
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ Function.Surjective (β := ConjClasses (G ⧸ H)) (ConjClasses.map (QuotientGroup.mk' H))

Tactic:
exact ConjClasses.map_surjective Quotient.mk''_surjective

Premises used: ConjClasses.map_surjective
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ Ne (α := ℚ) (↑(Nat.card G) : ℚ) 0

Tactic:
Nat.cast_ne_zero.mpr Finite.card_pos.ne'

Premises used: Iff.mpr, Finite.card_pos, LT.lt.ne', Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ Ne (α := ℚ) (↑(Nat.card G) : ℚ) 0

Tactic:
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'

Premises used: Iff.mpr, Finite.card_pos, LT.lt.ne', Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ LT.lt (α := ℚ) 0 (↑(Nat.card.{u_2} (G ⧸ H)) : ℚ)

Tactic:
Nat.cast_pos.mpr Finite.card_pos

Premises used: Iff.mpr, Nat.cast_pos, Finite.card_pos
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
H : Subgroup G
inst_2 : H.Normal
⊢ LT.lt (α := ℚ) 0 (↑(Nat.card.{u_2} (G ⧸ H)) : ℚ)

Tactic:
exact Nat.cast_pos.mpr Finite.card_pos

Premises used: Iff.mpr, Nat.cast_pos, Finite.card_pos
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
⊢ (↑(Nat.card.{u_2} ↥(commutator G)) : ℚ)⁻¹ ≤ commProb G

Tactic:
(inv_le_iff_one_le_mul₀ (Nat.cast_pos.mpr Finite.card_pos)).mpr
    (le_trans (ge_of_eq (commProb_eq_one_iff.mpr (Abelianization.commGroup G).to_isCommutative))
      (commutator G).commProb_quotient_le)

Premises used: Iff.mpr, ge_of_eq, CommMagma.to_isCommutative, commutator, commProb_eq_one_iff, inv_le_iff_one_le_mul₀, Subgroup.commProb_quotient_le, le_trans
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
rw :
  HDiv.hDiv (α := ℚ) (↑((n + 3) / 2) : ℚ) (↑(2 * n) : ℚ) = HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
⊢ commProb (DihedralGroup n) = HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)

Tactic:
rw [commProb_def', DihedralGroup.card_conjClasses_odd hn, nat_card]

Premises used: DihedralGroup.nat_card, DihedralGroup.card_conjClasses_odd, commProb_def'
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
rw : (n + 3) % 2 = 0
rw₁ : (n % 2 + HMod.hMod (α := ℕ) 3 2) % 2 = 0
rw₂ rw₃ : (1 + HMod.hMod (α := ℕ) 3 2) % 2 = 0
⊢ 2 ∣ n + 3

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]

Premises used: Nat.dvd_iff_mod_eq_zero, Iff.mp, Nat.add_mod, Nat.odd_iff
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
qify :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 / HMul.hMul (α := ℚ) 2 (↑n : ℚ) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑((n + 3) / 2) : ℚ) (↑(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]]
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
rw :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / (HMul.hMul (α := ℚ) 2 2 * (↑n : ℚ)) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 / HMul.hMul (α := ℚ) 2 (↑n : ℚ) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)

Tactic:
rw [div_div, ← mul_assoc]

Premises used: mul_assoc, div_div
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
e_a : HMul.hMul (α := ℚ) 2 2 = 4
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / (HMul.hMul (α := ℚ) 2 2 * (↑n : ℚ)) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑n : ℚ)

Tactic:
congr
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
hn : Odd n
⊢ HMul.hMul (α := ℚ) 2 2 = 4

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
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]
⊢ reciprocalFactors 0 = [0]

Tactic:
unfold reciprocalFactors

Premises used: DihedralGroup.reciprocalFactors
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
⊢ 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:
rfl