awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
pos : commProb (Product (reciprocalFactors 1)) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos₁ : commProb (Product []) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
Tactic: rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
pos : commProb (Product (reciprocalFactors 1)) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
pos₁ : commProb (Product []) = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos₂ : 1 = HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ)
Tactic: rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
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 : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos₃ : 1 = 1 / 1
Tactic: rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
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
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have pos₄ : Eq (α := ℚ) 1 1
Tactic: rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
-- 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 neg : ∀ (h2 : Even n), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: rcases Nat.even_or_odd n with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
neg : ∀ (h2 : Even n), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg₁ : ∀ (h2 : Odd n), commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: rcases Nat.even_or_odd n with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : HAdd.hAdd (α := ℚ) (↑3 : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑3 : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n / 2) : ℚ) =
  HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2),
        commProb_odd (by decide)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ HAdd.hAdd (α := ℚ) (↑3 : ℚ) 3 / HMul.hMul (α := ℚ) 4 (↑3 : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n / 2) : ℚ) =
    HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : HAdd.hAdd (α := ℚ) 1 1 * 2 = 4
Tactic: simp [field, h2.two_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (Product (reciprocalFactors n)) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
Tactic: rw [reciprocalFactors_odd h1 h2, commProb_cons, commProb_reciprocal (n / 4 + 1)]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (hypothesis)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have hn : Odd (n % 4)
Tactic: have hn : Odd (n % 4) := by grind
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg : HAdd.hAdd (α := ℚ) (↑(n % 4 * n) : ℚ) 3 * 1 * (↑n : ℚ) =
  1 * (HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ))
Tactic: rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
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) : ℚ))
⊢ commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg₁ : HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ) ≠ 0
Tactic: rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
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
⊢ commProb (DihedralGroup (n % 4 * n)) * HDiv.hDiv (α := ℚ) 1 (↑(n / 4 + 1) : ℚ) = HDiv.hDiv (α := ℚ) 1 (↑n : ℚ)
have neg₂ : Ne (α := ℚ) (↑n : ℚ) 0
Tactic: rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ HAdd.hAdd (α := ℚ) (↑(n % 4 * n) : ℚ) 3 * 1 * (↑n : ℚ) =
    1 * (HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ))
have neg : (n % 4 * n + 3) * 1 * n = 1 * (4 * (n % 4 * n) * (n / 4 + 1))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ HMul.hMul (α := ℚ) 4 (↑(n % 4 * n) : ℚ) * (↑(n / 4 + 1) : ℚ) ≠ 0
have neg : ¬4 * (n % 4 * n) * (n / 4 + 1) = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.CommutingProbability (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ ¬4 * (n % 4 * n) * (n / 4 + 1) = 0
have neg : n % 4 ≠ 0 → ¬4 * (n % 4 * n) * (n / 4 + 1) = 0
Tactic: positivity [hn.pos.ne']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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))
⊢ K.IsComplement' H
have rwa : IsComplement (↑K : Set G) (↑H : Set G)
Tactic: rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ K.IsComplement' H
have rwa₁ : Bijective (β := G) fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)
Tactic: rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ K.IsComplement' H
have rwa₂ : Bijective (α := ↥H × ↥K) (β := G) ((fun (x : ↥K × ↥H) ↦ (↑x.1 : G) * (↑x.2 : G)) ∘ (⇑ϕ : (a : ↥H × ↥K) → ↥K × ↥H))
Tactic: rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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))
⊢ K.IsComplement' H
have rwa₃ : Bijective (α := ↥H × ↥K) (β := G) (comp (β := G) (⇑ψ : (a : G) → G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G))
Tactic: rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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))
⊢ K.IsComplement' H
have rwa₄ : Bijective (β := G) fun (x : ↥H × ↥K) ↦ (↑x.1 : G) * (↑x.2 : G)
Tactic: rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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 := ⋯ }
⊢ K.IsComplement' H
have 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))
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ IsComplement {g} S ↔ S = univ
have h : ∀ (h : IsComplement {g} S) (x : G), Membership.mem (γ := Set G) ⊤ x → x ∈ S
Tactic: refine
    ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => (congr_arg _ h).mpr isComplement_singleton_univ⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ x ∈ S
have 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 sorry,
          Subtype.mk (p := fun (x : G) ↦ x ∈ S) y property) =
      z * x),
  x ∈ S
Tactic: obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ x ∈ S
have rwa : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {z} x) z sorry,
          Subtype.mk (p := fun (x : G) ↦ x ∈ S) y property).2 :
    G) ∈
  S
Tactic: rwa [← mul_left_cancel hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ IsComplement S {g} ↔ S = univ
have h : ∀ (h : IsComplement S {g}) (x : G), Membership.mem (γ := Set G) ⊤ x → x ∈ S
Tactic: refine
    ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => h ▸ isComplement_univ_singleton⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ x ∈ S
have 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
Tactic: obtain ⟨y, hy⟩ := h.2 (x * g)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
| x * g
have rw : x * (↑y.2 : G)
Tactic: rw [← show y.2.1 = g from y.2.2]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
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
⊢ x ∈ S
have hy₁ : (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]
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ x ∈ S
have rw : (↑y.1 : G) ∈ S
Tactic: rw [← mul_right_cancel hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ IsComplement univ S ↔ ∃ (g : G), S = {g}
have refine_1 : ∀ (h : IsComplement univ S), S.Nonempty
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
refine_1 : ∀ (h : IsComplement univ S), S.Nonempty
⊢ IsComplement univ S ↔ ∃ (g : G), S = {g}
have refine_2 : ∀ (h : IsComplement univ S) (a : G) (ha : a ∈ S) (b : G) (hb : b ∈ S), a = b
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ IsComplement univ S ↔ ∃ (g : G), S = {g}
have refine_3 : (∃ (g : G), S = {g}) → IsComplement univ S
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement univ S
⊢ S.Nonempty
have 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
Tactic: obtain ⟨a, _⟩ := h.2 1
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
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
⊢ a = b
have this : Eq (α := (↑⊤ : Type u_1) × (↑S : Type u_1))
  ((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) a⁻¹ sorry, 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⁻¹ sorry, 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)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ IsComplement S univ ↔ ∃ (g : G), S = {g}
have refine_1 : ∀ (h : IsComplement S univ), S.Nonempty
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
refine_1 : ∀ (h : IsComplement S univ), S.Nonempty
⊢ IsComplement S univ ↔ ∃ (g : G), S = {g}
have refine_2 : ∀ (h : IsComplement S univ) (a : G) (ha : a ∈ S) (b : G) (hb : b ∈ S), a = b
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
refine_1 : ∀ (h : IsComplement S univ), S.Nonempty
refine_2 : ∀ (h : IsComplement S univ) (a : G) (ha : a ∈ S) (b : G) (hb : b ∈ S), a = b
⊢ IsComplement S univ ↔ ∃ (g : G), S = {g}
have refine_3 : (∃ (g : G), S = {g}) → IsComplement S univ
Tactic: refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement S univ
⊢ S.Nonempty
have refine_1 : ∀ (a : (↑S : Type u_1) × (↑univ : Type u_1)),
  Eq.{u_1 + 1} (α := G) ((fun (x : (↑S : Type u_1) × (↑univ : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a) 1 → S.Nonempty
Tactic: obtain ⟨a, _⟩ := h.2 1
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b
have this : Eq (α := (↑S : Type u_1) × (↑⊤ : Type u_1))
  ((Subtype.mk (p := fun (x : G) ↦ x ∈ S) a ha, Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) a⁻¹ sorry) :
    (↑S : Type u_1) × (↑⊤ : Type u_1))
  ((Subtype.mk (p := fun (x : G) ↦ x ∈ S) b hb, Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) ⊤ x) b⁻¹ sorry) :
    (↑S : Type u_1) × (↑⊤ : Type u_1))
Tactic: have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
      h.1 ((mul_inv_cancel a).trans (mul_inv_cancel b).symm)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
⊢ S.Nonempty
have contrapose! : ∀ (hst : S = ∅), ¬IsComplement S T
Tactic: contrapose! hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
⊢ T.Nonempty
have contrapose! : ∀ (hst : T = ∅), ¬IsComplement S T
Tactic: contrapose! hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T
have h : ∀ (g : G),
  (∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: convert! isComplement_iff_existsUnique with g
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
⊢ (∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have h : (∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T) → ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
h : (∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T) → ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
⊢ (∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have h₁ : (∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g) → ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S
have h : ∀ (g : G),
  (∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: convert! isComplement_iff_existsUnique with g
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
⊢ (∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have h : (∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S) → ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
h : (∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S) → ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
⊢ (∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S) ↔ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have h₁ : (∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g) → ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S (↑H : Set G) ↔ ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
have simp_rw : (∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)) ↔
  ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
Tactic: simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq,
    QuotientGroup.forall_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
simp_rw :
  (∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)) ↔
    ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
⊢ IsComplement S (↑H : Set G) ↔ ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
have simp_rw₁ : (∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ H) ↔ ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
Tactic: simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq,
    QuotientGroup.forall_mk]