awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
⊢ (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S = (↑H : Set G)
have this₁ : (⇑H.subtype : (a : ↥H) → G) '' ((↑H'' : Set ↥H) * S) = (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S
Tactic: have : H.subtype '' (H'' * S) = H''.map H.subtype * H.subtype '' S := image_mul H.subtype
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this :
  (⇑H.subtype : (a : ↥H) → G) '' ((↑H'' : Set ↥H) * S) =
    (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S
⊢ (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S = (↑H : Set G)
have refine_1 : image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) univ = (↑H : Set G)
Tactic: rw [← this, cmem.mul_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H
have this₁ : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
Tactic: have : Nat.card H'' * Nat.card S = Nat.card H := cmem.card_mul_card
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H
have refine_2 : Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
  Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)
have refine_2 : Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H''
Tactic: refine congr_arg₂ (· * ·) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
refine_2 : Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H''
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)
have refine_2₁ : Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)
Tactic: refine congr_arg₂ (· * ·) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    LeftCosetEquivalence (↑K : Set G) g₁ g₂
have rw : Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
  g₁⁻¹ * g₂ ∈ K
Tactic: rw [LeftCosetEquivalence, leftCoset_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    g₁⁻¹ * g₂ ∈ K
have mp : Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 →
  g₁⁻¹ * g₂ ∈ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
mp :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 →
    g₁⁻¹ * g₂ ∈ K
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    g₁⁻¹ * g₂ ∈ K
have mpr : g₁⁻¹ * g₂ ∈ K →
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
⊢ g₁⁻¹ * g₂ ∈ K
have mp : (↑(HMul.hMul (α := ↥K)
        ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2⁻¹
        ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2) :
    G) ∈
  K
Tactic: rw [← hSK.equiv_fst_mul_equiv_snd g₂, ← hSK.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
have mpr : (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1 : G)⁻¹ * g₁ ∈
  (↑K : Set G)
Tactic: apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
mpr :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
have mpr₁ : (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ * g₁ ∈
  (↑K : Set G)
Tactic: apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)
have mpr : (g₁ *
        (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2 :
            G)⁻¹)⁻¹ *
    g₁ ∈
  (↑K : Set G)
Tactic: rw [equiv_fst_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)
have mpr : (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ * g₁ *
    (g₁⁻¹ * g₂) ∈
  K
Tactic: rw [SetLike.mem_coe, ← mul_mem_cancel_right h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
        g₁ *
      (g₁⁻¹ * g₂) ∈
    K
have mpr : (g₂ *
          (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2 :
              G)⁻¹)⁻¹ *
      g₁ *
    (g₁⁻¹ * g₂) ∈
  K
Tactic: rw [equiv_fst_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    RightCosetEquivalence (↑H : Set G) g₁ g₂
have rw : Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
  g₂ * g₁⁻¹ ∈ H
Tactic: rw [RightCosetEquivalence, rightCoset_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    g₂ * g₁⁻¹ ∈ H
have mp : Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 →
  g₂ * g₁⁻¹ ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
mp :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 →
    g₂ * g₁⁻¹ ∈ H
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    g₂ * g₁⁻¹ ∈ H
have mpr : g₂ * g₁⁻¹ ∈ H →
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
⊢ g₂ * g₁⁻¹ ∈ H
have mp : (↑(HMul.hMul (α := ↥H)
        ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1
        ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1⁻¹) :
    G) ∈
  H
Tactic: rw [← hHT.equiv_fst_mul_equiv_snd g₂, ← hHT.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
have mpr : g₁ * (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2 : G)⁻¹ ∈
  (↑H : Set G)
Tactic: apply (isComplement_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
mpr :
  g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2 :
          G)⁻¹ ∈
    (↑H : Set G)
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
have mpr₁ : g₁ * (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 : G)⁻¹ ∈
  (↑H : Set G)
Tactic: apply (isComplement_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2 :
          G)⁻¹ ∈
    (↑H : Set G)
have mpr : g₁ *
    ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1 : G)⁻¹ *
        g₁)⁻¹ ∈
  (↑H : Set G)
Tactic: rw [equiv_snd_eq_inv_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
          G)⁻¹ ∈
    (↑H : Set G)
have mpr : g₂ * g₁⁻¹ *
    (g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
          G)⁻¹) ∈
  H
Tactic: rw [SetLike.mem_coe, ← mul_mem_cancel_left h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * g₁⁻¹ *
      (g₁ *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
            G)⁻¹) ∈
    H
have mpr : g₂ *
    (g₁⁻¹ *
      (g₁ *
        ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1 :
                G)⁻¹ *
            g₂)⁻¹)) ∈
  H
Tactic: rw [equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g : G
⊢ LeftCosetEquivalence (↑K : Set G) g
    (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1 : G)
have rw : LeftCosetEquivalence (↑K : Set G) g
  (g * (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).2 : G)⁻¹)
Tactic: rw [equiv_fst_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g : G
⊢ RightCosetEquivalence (↑H : Set G) g
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)
have rw : (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g *
    g⁻¹ ∈
  H
Tactic: rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]
-- 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
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g
have rw : ({ toFun := fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G), invFun := surjInv sorry, left_inv := sorry,
            right_inv := sorry : (↑S : Type u_1) × (↑T : Type u_1) ≃ G }.symm.symm :
      (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
  g
Tactic: rw [equiv, Equiv.ofBijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
have this : (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
  g
Tactic: have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by
    rw [equiv, Equiv.ofBijective]; simp
-- 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
g : G
h1 : 1 ∈ T
hg : g ∈ S
this :
  (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g
| ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1
have rw : (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1).1
Tactic: rw [← this, Equiv.apply_symm_apply]
-- 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
g : G
h1 : 1 ∈ T
hg : g ∈ S
this :
  (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
have conv_lhs : ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
  Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
Tactic: conv_lhs => rw [← this, Equiv.apply_symm_apply]
-- 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
g : G
h1 : 1 ∈ T
hg : g ∈ S
this :
  (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g
conv_lhs :
  ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
have conv_lhs₁ : (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1).1 =
  Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
Tactic: conv_lhs => rw [← this, Equiv.apply_symm_apply]
-- 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
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g
have rw : ({ toFun := fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G), invFun := surjInv sorry, left_inv := sorry,
            right_inv := sorry : (↑S : Type u_1) × (↑T : Type u_1) ≃ G }.symm.symm :
      (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
  g
Tactic: rw [equiv, Equiv.ofBijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg
have this : (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
  g
Tactic: have : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g := by
    rw [equiv, Equiv.ofBijective]; simp
-- 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
g : G
h1 : 1 ∈ S
hg : g ∈ T
this :
  (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g
| ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2
have rw : (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg).2
Tactic: rw [← this, Equiv.apply_symm_apply]
-- 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
g : G
h1 : 1 ∈ S
hg : g ∈ T
this :
  (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg
have conv_lhs : ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
  Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg
Tactic: conv_lhs => rw [← this, Equiv.apply_symm_apply]