awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
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))
    []
⊢ reciprocalFactors 1 = []

Tactic:
unfold reciprocalFactors

Premises used: DihedralGroup.reciprocalFactors
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
⊢ 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:
rfl
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
h0 : Ne (α := ℕ) 1 0
h2 : Even (α := ℕ) 1
⊢ False

Tactic:
norm_num at h2
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ n ≠ 1

Tactic:
have h1 : n ≠ 1 := by
    rintro rfl
    norm_num at h2
-- Module: Mathlib.GroupTheory.CommutingProbability
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)
rw₃ rw₄ : 3 :: reciprocalFactors (n / 2) = 3 :: reciprocalFactors (n / 2)
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]

Premises used: if_pos, dif_neg, DihedralGroup.reciprocalFactors
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
h1 : Ne (α := ℕ) 0 1
h2 : Odd (α := ℕ) 0
⊢ False

Tactic:
norm_num [← Nat.not_even_iff_odd] at h2

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ n ≠ 0

Tactic:
have h0 : n ≠ 0 := by
    rintro rfl
    norm_num [← Nat.not_even_iff_odd] at h2
-- Module: Mathlib.GroupTheory.CommutingProbability
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)
rw₃ rw₄ : n % 4 * n :: reciprocalFactors (n / 4 + 1) = n % 4 * n :: reciprocalFactors (n / 4 + 1)
⊢ reciprocalFactors n = 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)]

Premises used: Iff.mpr, Nat.not_even_iff_odd, dif_neg, DihedralGroup.reciprocalFactors, if_neg
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
⊢ commProb (Product []) = 1

Tactic:
simp [Product, commProb_pi]

Premises used: commProb_pi, DihedralGroup.Product
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
l : List ℕ
⊢ commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)

Tactic:
simp only [commProb_pi, Fin.prod_univ_succ, Fin.getElem_fin, Fin.val_succ, Fin.val_zero,
    List.getElem_cons_zero, List.length_cons, List.getElem_cons_succ]

Premises used: List.length_cons, Fin.val_succ, List.getElem_cons_zero, Fin.prod_univ_succ, commProb_pi, Fin.getElem_fin, Fin.val_zero, List.getElem_cons_succ
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
pos : ∀ (h0 : n = 0), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
neg : ∀ (h0 : ¬n = 0), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

Tactic:
by_cases h0 : n = 0
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : n = 0
pos : commProb (DihedralGroup 0) = 0
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

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

Premises used: DihedralGroup.commProb_nil, DihedralGroup.reciprocalFactors_zero, Nat.cast_zero, mul_one, div_zero, DihedralGroup.commProb_cons
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) = 0

Tactic:
apply commProb_eq_zero_of_infinite

Premises used: commProb_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
pos : ∀ (h1 : n = 1), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
neg : ∀ (h1 : ¬n = 1), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

Tactic:
by_cases h1 : n = 1
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
pos : commProb (Product (reciprocalFactors 1)) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
pos₁ : commProb (Product []) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
pos₂ : 1 = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
pos₃ : 1 = 1 / 1
pos₄ pos₅ : Eq (α := ℚ) 1 1
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

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

Premises used: DihedralGroup.commProb_nil, DihedralGroup.reciprocalFactors_one, div_one, Nat.cast_one
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
neg : ∀ (h2 : Even n), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
neg₁ : ∀ (h2 : Odd n), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

Tactic:
rcases Nat.even_or_odd n with h2 | h2

Premises used: Nat.even_or_odd
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ Odd (α := ℕ) 3

Tactic:
decide
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
neg :
  HAdd.hAdd (α := ℚ) (↑3 : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑3 : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n / 2) : ℚ) =
    HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

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

Premises used: HDiv.hDiv, DihedralGroup.reciprocalFactors_even, DihedralGroup.commProb_odd, OfNat.ofNat, DihedralGroup.commProb_cons
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
neg : HAdd.hAdd (α := ℚ) 1 1 * 2 = 4
⊢ HAdd.hAdd (α := ℚ) (↑3 : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑3 : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n / 2) : ℚ) =
    HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

Tactic:
simp [field, h2.two_dvd]

Premises used: Even.two_dvd
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ HAdd.hAdd (α := ℚ) 1 1 * 2 = 4

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
neg : commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

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

Premises used: HDiv.hDiv, HAdd.hAdd, DihedralGroup.reciprocalFactors_odd, OfNat.ofNat, DihedralGroup.commProb_cons
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ Odd (n % 4)

Tactic:
grind
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ Odd (n % 4)

Tactic:
have hn : Odd (n % 4) := by grind
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
neg :
  HAdd.hAdd (α := ℚ) (↑(n % 4 * n) : ℚ) 3 * 1 * (↑n : ℚ) =
    1 * (HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ))
neg₁ : HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ) ≠ 0
neg₂ : Ne (α := ℚ) (↑n : ℚ) 0
⊢ commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)

Tactic:
rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff]

Premises used: div_mul_div_comm, div_eq_div_iff, DihedralGroup.commProb_odd, Odd.mul
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
neg : (n % 4 * n + 3) * 1 * n = 1 * (4 * (n % 4 * n) * (n / 4 + 1))
⊢ HAdd.hAdd (α := ℚ) (↑(n % 4 * n) : ℚ) 3 * 1 * (↑n : ℚ) =
    1 * (HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ))

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
neg : ¬4 * (n % 4 * n) * (n / 4 + 1) = 0
⊢ HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
neg neg₁ neg₂ neg₃ : ¬n = 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ (n % 4 * n + 3) * 1 * n = 1 * (4 * (n % 4 * n) * (n / 4 + 1))

Tactic:
grind [Nat.div_add_mod n 4, Odd]

Premises used: Nat.div_add_mod, Odd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CommutingProbability
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
neg neg₁ neg₂ neg₃ : n % 4 ≠ 0 → ¬4 * (n % 4 * n) * (n / 4 + 1) = 0
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0

Tactic:
positivity [hn.pos.ne']

Premises used: Odd.pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Type u_2
inst_1 : SetLike S G
s t : S
⊢ IsComplement (↑s : Set G) (↑t : Set G) ↔ Bijective (β := G) fun (x : ↥s × ↥t) ↦ (↑x.1 : G) * (↑x.2 : G)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Subgroup.IsComplement
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.IsComplement' K ↔ IsComplement (↑H : Set G) (↑K : Set G)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
Function.bijective_iff_existsUnique _

Premises used: Subgroup.IsComplement, Function.bijective_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
h : IsComplement S T
g : G
⊢ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
isComplement_iff_existsUnique.mp h g

Premises used: Subgroup.isComplement_iff_existsUnique, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun (x : ↥H × ↥K) ↦ (x.2⁻¹, x.1⁻¹), invFun := fun (x : ↥K × ↥H) ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯,
    right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun (g : G) ↦ g⁻¹, invFun := fun (g : G) ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf :
  Eq (α := ↥H × ↥K → G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
    ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))
rwa : IsComplement (↑K : Set G) (↑H : Set G)
rwa₁ : Bijective (β := G) fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)
rwa₂ :
  Bijective (α := ↥H × ↥K) (β := G) ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))
rwa₃ : Bijective (α := ↥H × ↥K) (β := G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
rwa₄ rwa₅ rwa₆ rwa₇ : Bijective (β := G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G)
⊢ K.IsComplement' H

Tactic:
rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]

Premises used: Equiv.bijective_comp, Subgroup.isComplement_iff_bijective, Equiv.comp_bijective, Subgroup.isComplement'_def
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun (x : ↥H × ↥K) ↦ (x.2⁻¹, x.1⁻¹), invFun := fun (x : ↥K × ↥H) ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯,
    right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun (g : G) ↦ g⁻¹, invFun := fun (g : G) ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
suffices :
  Eq (α := ↥H × ↥K → G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
    ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))
⊢ K.IsComplement' H

Tactic:
suffices hf : (ψ ∘ fun x : H × K => x.1.1 * x.2.1) = (fun x : K × H => x.1.1 * x.2.1) ∘ ϕ by
    rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun (x : ↥H × ↥K) ↦ (x.2⁻¹, x.1⁻¹), invFun := fun (x : ↥K × ↥H) ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯,
    right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun (g : G) ↦ g⁻¹, invFun := fun (g : G) ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
⊢ Eq (α := ↥H × ↥K → G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
    ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))

Tactic:
funext fun x => mul_inv_rev _ _

Premises used: Prod.fst, funext, mul_inv_rev, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun (x : ↥H × ↥K) ↦ (x.2⁻¹, x.1⁻¹), invFun := fun (x : ↥K × ↥H) ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯,
    right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun (g : G) ↦ g⁻¹, invFun := fun (g : G) ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
⊢ Eq (α := ↥H × ↥K → G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
    ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))

Tactic:
exact funext fun x => mul_inv_rev _ _

Premises used: funext, mul_inv_rev
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.IsComplement' K ↔ K.IsComplement' H

Tactic:
⟨IsComplement'.symm, IsComplement'.symm⟩

Premises used: Iff.intro, Subgroup.IsComplement'.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
g : G
⊢ IsComplement (G := G) univ {g}

Tactic:
⟨fun ⟨_, _, rfl⟩ ⟨_, _, rfl⟩ h => Prod.ext (Subtype.ext (mul_right_cancel h)) rfl, fun x =>
    ⟨⟨⟨x * g⁻¹, ⟨⟩⟩, g, rfl⟩, inv_mul_cancel_right x g⟩⟩

Premises used: HMul.hMul, Prod.mk, Subtype.mk, Inv.inv, Prod.ext, And.intro, Exists.intro, _private.0.Subgroup.isComplement_univ_singleton.match_1, Function.Bijective, mul_right_cancel, _private.0.Subgroup.isComplement_univ_singleton.match_2, Subgroup.IsComplement, inv_mul_cancel_right, Eq, rfl, True.intro, Subtype.ext
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
g : G
⊢ IsComplement (G := G) {g} univ

Tactic:
⟨fun ⟨⟨_, rfl⟩, _⟩ ⟨⟨_, rfl⟩, _⟩ h => Prod.ext rfl (Subtype.ext (mul_left_cancel h)), fun x =>
    ⟨⟨⟨g, rfl⟩, g⁻¹ * x, ⟨⟩⟩, mul_inv_cancel_left g x⟩⟩

Premises used: HMul.hMul, mul_left_cancel, Prod.mk, Subtype.mk, Inv.inv, Prod.ext, _private.0.Subgroup.isComplement_singleton_univ.match_1, And.intro, _private.0.Subgroup.isComplement_singleton_univ.match_2, Exists.intro, Function.Bijective, Subgroup.IsComplement, mul_inv_cancel_left, Eq, rfl, True.intro, Subtype.ext
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ IsComplement {g} S ↔ S = univ

Tactic:
⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => (congr_arg _ h).mpr isComplement_singleton_univ⟩

Premises used: Subgroup.isComplement_singleton_univ, Eq.mpr, congr_arg, Iff.intro, top_le_iff, Iff.mp, Subgroup.IsComplement, Singleton.singleton
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : IsComplement {g} S) (x : G), Membership.mem (γ := Set G) ⊤ x → x ∈ S
⊢ IsComplement {g} S ↔ S = univ

Tactic:
refine
    ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => (congr_arg _ h).mpr isComplement_singleton_univ⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement {g} S
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
obtain :
  ∀ (z : G) (h : IsComplement {z} S) (y : G) (property : y ∈ S)
    (hy :
      (fun (x : (↑{z} : Type u_1) × (↑S : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G))
          (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {z} x) z ⋯,
            Subtype.mk (p := fun (x : G) ↦ x ∈ S) y property) =
        z * x),
    x ∈ S
⊢ x ∈ S

Tactic:
obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)

Premises used: HMul.hMul, And.right, rfl
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
z : G
h : IsComplement {z} S
y : G
property : y ∈ S
hy :
  (fun (x : (↑{z} : Type u_1) × (↑S : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {z} x) z ⋯,
        Subtype.mk (p := fun (x : G) ↦ x ∈ S) y property) =
    z * x
rwa rwa₁ rwa₂ rwa₃ :
  (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {z} x) z ⋯,
            Subtype.mk (p := fun (x : G) ↦ x ∈ S) y property).2 :
      G) ∈
    S
⊢ x ∈ S

Tactic:
rwa [← mul_left_cancel hy]

Premises used: mul_left_cancel
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ IsComplement S {g} ↔ S = univ

Tactic:
⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => h ▸ isComplement_univ_singleton⟩

Premises used: Eq.rec, Iff.intro, top_le_iff, Iff.mp, Subgroup.isComplement_univ_singleton, Eq.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : IsComplement S {g}) (x : G), Membership.mem (γ := Set G) ⊤ x → x ∈ S
⊢ IsComplement S {g} ↔ S = univ

Tactic:
refine
    ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => h ▸ isComplement_univ_singleton⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
obtain :
  ∀ (y : (↑S : Type u_1) × (↑{g} : Type u_1))
    (hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * g), x ∈ S
⊢ x ∈ S

Tactic:
obtain ⟨y, hy⟩ := h.2 (x * g)

Premises used: HMul.hMul, And.right
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
y : (↑S : Type u_1) × (↑{g} : Type u_1)
hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * g
rw : x * (↑y.2 : G)
| x * g

Tactic:
rw [← show y.2.1 = g from y.2.2]

Premises used: Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
y : (↑S : Type u_1) × (↑{g} : Type u_1)
hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * g
⊢ (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * (↑y.2 : G)

Tactic:
conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]

Premises used: Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
y : (↑S : Type u_1) × (↑{g} : Type u_1)
hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * (↑y.2 : G)
rw : (↑y.1 : G) ∈ S
⊢ x ∈ S

Tactic:
rw [← mul_right_cancel hy]

Premises used: mul_right_cancel
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
y : (↑S : Type u_1) × (↑{g} : Type u_1)
hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * (↑y.2 : G)
⊢ (↑y.1 : G) ∈ S

Tactic:
y.1.2

Premises used: Prod.fst, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
h_1 : Membership.mem (γ := Set G) ⊤ x
y : (↑S : Type u_1) × (↑{g} : Type u_1)
hy : (fun (x : (↑S : Type u_1) × (↑{g} : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) y = x * (↑y.2 : G)
⊢ (↑y.1 : G) ∈ S

Tactic:
exact y.1.2

Premises used: Prod.fst, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ IsComplement univ S ↔ ∃ (g : G), S = {g}

Tactic:
⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩

Premises used: Iff.mpr, Set.exists_eq_singleton_iff_nonempty_subsingleton, And.intro, Iff.intro
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
refine_1 : ∀ (h : IsComplement univ S), S.Nonempty
refine_2 : ∀ (h : IsComplement univ S) (a : G) (ha : a ∈ S) (b : G) (hb : b ∈ S), a = b
refine_3 : (∃ (g : G), S = {g}) → IsComplement univ S
⊢ IsComplement univ S ↔ ∃ (g : G), S = {g}

Tactic:
refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
refine_1 :
  ∀ (a : (↑univ : Type u_1) × (↑S : Type u_1)),
    Eq.{u_1 + 1} (α := G) ((fun (x : (↑univ : Type u_1) × (↑S : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a) 1 → S.Nonempty
⊢ S.Nonempty

Tactic:
obtain ⟨a, _⟩ := h.2 1

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
a : (↑univ : Type u_1) × (↑S : Type u_1)
h_1 : Eq.{u_1 + 1} (α := G) ((fun (x : (↑univ : Type u_1) × (↑S : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a) 1
⊢ S.Nonempty

Tactic:
⟨a.2.1, a.2.2⟩

Premises used: Set.Nonempty, Exists.intro, Subtype.val, Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
a : (↑univ : Type u_1) × (↑S : Type u_1)
h_1 : Eq.{u_1 + 1} (α := G) ((fun (x : (↑univ : Type u_1) × (↑S : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a) 1
⊢ S.Nonempty

Tactic:
exact ⟨a.2.1, a.2.2⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ Eq (α := (↑⊤ : Type u_1) × (↑S : Type u_1))
    ((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) a⁻¹ ⋯,
        Subtype.mk (p := fun (x : G) ↦ x ∈ S) a ha) :
      (↑⊤ : Type u_1) × (↑S : Type u_1))
    ((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) b⁻¹ ⋯,
        Subtype.mk (p := fun (x : G) ↦ x ∈ S) b hb) :
      (↑⊤ : Type u_1) × (↑S : Type u_1))

Tactic:
have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
      h.1 ((inv_mul_cancel a).trans (inv_mul_cancel b).symm)
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this :
  Eq (α := (↑⊤ : Type u_1) × (↑S : Type u_1))
    ((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) a⁻¹ ⋯,
        Subtype.mk (p := fun (x : G) ↦ x ∈ S) a ha) :
      (↑⊤ : Type u_1) × (↑S : Type u_1))
    ((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) b⁻¹ ⋯,
        Subtype.mk (p := fun (x : G) ↦ x ∈ S) b hb) :
      (↑⊤ : Type u_1) × (↑S : Type u_1))
⊢ a = b

Tactic:
Subtype.ext_iff.mp (Prod.ext_iff.mp this).2

Premises used: Prod.ext_iff, Subtype.ext_iff, And.right, Iff.mp