awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g → g ∈ S
mpr : g ∈ S → (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g ↔ g ∈ S

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) ∈ S
⊢ g ∈ S

Tactic:
rw [← h]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) ∈ S

Tactic:
Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) ∈ S

Tactic:
exact Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : g ∈ S
mpr mpr₁ : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) g h) : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g

Tactic:
rw [hST.equiv_fst_eq_self_of_mem_of_one_mem h1 h]

Premises used: Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g → g ∈ T
mpr : g ∈ T → (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g ↔ g ∈ T

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ∈ T
⊢ g ∈ T

Tactic:
rw [← h]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ∈ T

Tactic:
Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ∈ T

Tactic:
exact Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
mpr mpr₁ : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) g h) : G) = g
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g

Tactic:
rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h]

Premises used: Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
rw : g * (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ = 1 ↔ g ∈ T
rw₁ : g = (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ↔ g ∈ T
rw₂ : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g ↔ g ∈ T
rw₃ rw₄ : g ∈ T ↔ g ∈ T
⊢ Eq.{u_1 + 1} (α := G) (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) 1 ↔
    g ∈ T

Tactic:
rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]

Premises used: Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, mul_inv_eq_one, eq_comm, Subgroup.IsComplement.equiv_fst_eq_mul_inv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
rw : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g = 1 ↔ g ∈ S
rw₁ : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g ↔ g ∈ S
rw₂ rw₃ : g ∈ S ↔ g ∈ S
⊢ Eq.{u_1 + 1} (α := G) (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) 1 ↔
    g ∈ S

Tactic:
rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]

Premises used: Subgroup.IsComplement.equiv_snd_eq_inv_mul, Subgroup.IsComplement.equiv_fst_eq_self_iff_mem, inv_mul_eq_one
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
h : IsComplement S (↑H : Set G)
rw : Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex
⊢ Finite.{u_1 + 1} (↑S : Type u_1) ↔ H.FiniteIndex

Tactic:
rw [← h.leftQuotientEquiv.finite_iff]

Premises used: Equiv.finite_iff, Subgroup.IsComplement.leftQuotientEquiv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
h : IsComplement S (↑H : Set G)
⊢ Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex

Tactic:
⟨fun _ ↦ finiteIndex_of_finite_quotient, fun _ ↦ finite_quotient_of_finiteIndex⟩

Premises used: Subgroup.finite_quotient_of_finiteIndex, Iff.intro, Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
h : IsComplement S (↑H : Set G)
⊢ Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex

Tactic:
exact ⟨fun _ ↦ finiteIndex_of_finite_quotient, fun _ ↦ finite_quotient_of_finiteIndex⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
inst_1 : H.FiniteIndex
hS : IsComplement S (↑H : Set G)
⊢ S.Finite

Tactic:
hS.finite_left_iff.2 ‹_›

Premises used: Iff.mpr, Set.Finite, Subgroup.IsComplement.finite_left_iff
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
hS : IsComplement S (↑H : Set G)
q : G ⧸ H
⊢ Quotient.mk'' (↑((hS.leftQuotientEquiv (S := S) : (a : G ⧸ H) → (↑S : Type u_1)) q) : G) = q

Tactic:
hS.leftQuotientEquiv.symm_apply_apply q

Premises used: Equiv.symm_apply_apply, Set.restrict, Subgroup.IsComplement.leftQuotientEquiv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), (↑(f q) : G ⧸ H) = q
q : G ⧸ H
⊢ (↑((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q) : G) = f q

Tactic:
(Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Premises used: Subtype.coe_mk, Subtype.ext_iff, Iff.mp, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), (↑(f q) : G ⧸ H) = q
q : G ⧸ H
refine :
  Eq (α := { x : G // x ∈ range f })
    ((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q : (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })
⊢ (↑((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q) : G) = f q

Tactic:
refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Premises used: Subtype.coe_mk, Subtype.ext_iff, Iff.mp, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), (↑(f q) : G ⧸ H) = q
q : G ⧸ H
⊢ Eq (α := { x : G // x ∈ range f })
    ((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q : (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })

Tactic:
(leftQuotientEquiv (isComplement_range_left hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm

Premises used: Iff.mpr, Subgroup.isComplement_range_left, Subgroup.IsComplement.leftQuotientEquiv, Eq.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), (↑(f q) : G ⧸ H) = q
q : G ⧸ H
⊢ Eq (α := { x : G // x ∈ range f })
    ((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q : (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })

Tactic:
exact (leftQuotientEquiv (isComplement_range_left hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm

Premises used: Iff.mpr, Subgroup.isComplement_range_left, Subgroup.IsComplement.leftQuotientEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
hS : IsComplement S (↑H : Set G)
g : G
⊢ (↑(hS.toLeftFun (S := S) g) : G)⁻¹ * g ∈ H

Tactic:
QuotientGroup.leftRel_apply.mp <| Quotient.exact' <| quotientGroupMk_leftQuotientEquiv _ _

Premises used: Iff.mp, Quotient.exact', Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
hS : IsComplement S (↑H : Set G)
g : G
rw : g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)⁻¹⁻¹ = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
rw₁ rw₂ : g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G) = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
⊢ ((↑(hS.toLeftFun (S := S) g) : G)⁻¹ * g)⁻¹ = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)

Tactic:
rw [mul_inv_rev, inv_inv]

Premises used: inv_inv, mul_inv_rev
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H : Set G) T
rw : Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex
⊢ Finite.{u_1 + 1} (↑T : Type u_1) ↔ H.FiniteIndex

Tactic:
rw [← h.rightQuotientEquiv.finite_iff,
    (QuotientGroup.quotientRightRelEquivQuotientLeftRel H).finite_iff]

Premises used: Equiv.finite_iff, QuotientGroup.quotientRightRelEquivQuotientLeftRel, Subgroup.IsComplement.rightQuotientEquiv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H : Set G) T
⊢ Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex

Tactic:
⟨fun _ ↦ finiteIndex_of_finite_quotient, fun _ ↦ finite_quotient_of_finiteIndex⟩

Premises used: Subgroup.finite_quotient_of_finiteIndex, Iff.intro, Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H : Set G) T
⊢ Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex

Tactic:
exact ⟨fun _ ↦ finiteIndex_of_finite_quotient, fun _ ↦ finite_quotient_of_finiteIndex⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
inst_1 : H.FiniteIndex
hT : IsComplement (↑H : Set G) T
⊢ T.Finite

Tactic:
hT.finite_right_iff.2 ‹_›

Premises used: Iff.mpr, Set.Finite, Subgroup.IsComplement.finite_right_iff
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H : Set G) T
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk''
      (↑((hT.rightQuotientEquiv (T := T) : (a : Quotient (QuotientGroup.rightRel H)) → (↑T : Type u_1)) q) : G) =
    q

Tactic:
(rightQuotientEquiv hT).symm_apply_apply q

Premises used: Equiv.symm_apply_apply, Set.restrict, Subgroup.IsComplement.rightQuotientEquiv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ (↑((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q) :
      G) =
    f q

Tactic:
(Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Premises used: Subtype.coe_mk, Subtype.ext_iff, Iff.mp, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
refine :
  Eq (α := { x : G // x ∈ range f })
    ((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q :
      (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })
⊢ (↑((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q) :
      G) =
    f q

Tactic:
refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Premises used: Subtype.coe_mk, Subtype.ext_iff, Iff.mp, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ Eq (α := { x : G // x ∈ range f })
    ((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q :
      (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })

Tactic:
(rightQuotientEquiv (isComplement_range_right hf)).apply_eq_iff_eq_symm_apply.2 (hf q).symm

Premises used: Iff.mpr, Subgroup.isComplement_range_right, Subgroup.IsComplement.rightQuotientEquiv, Eq.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ Eq (α := { x : G // x ∈ range f })
    ((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q :
      (↑(range f) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q) ⋯ : { x : G // x ∈ range f })

Tactic:
exact (rightQuotientEquiv (isComplement_range_right hf)).apply_eq_iff_eq_symm_apply.2 (hf q).symm

Premises used: Iff.mpr, Subgroup.isComplement_range_right, Subgroup.IsComplement.rightQuotientEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H : Set G) T
g : G
⊢ g * (↑(hT.toRightFun (T := T) g) : G)⁻¹ ∈ H

Tactic:
QuotientGroup.rightRel_apply.mp <| Quotient.exact' <| mk''_rightQuotientEquiv _ _

Premises used: QuotientGroup.rightRel_apply, Iff.mp, Quotient.exact', Subgroup.IsComplement.mk''_rightQuotientEquiv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H : Set G) T
g : G
rw : (↑(hT.toRightFun (T := T) g) : G)⁻¹⁻¹ * g⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
rw₁ rw₂ : (↑(hT.toRightFun (T := T) g) : G) * g⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
⊢ (g * (↑(hT.toRightFun (T := T) g) : G)⁻¹)⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹

Tactic:
rw [mul_inv_rev, inv_inv]

Premises used: inv_inv, mul_inv_rev
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
inst_1 : H.FiniteIndex
h : IsComplement S (↑H : Set G)
rw : Eq (α := ℕ∞) (↑S.ncard : ℕ∞) (↑H.index : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑H.index : ℕ∞) (↑H.index : ℕ∞)
⊢ S.encard = (↑H.index : ℕ∞)

Tactic:
rw [← h.finite_left.cast_ncard_eq, h.ncard_left]

Premises used: Subgroup.IsComplement.finite_left, Subgroup.IsComplement.ncard_left, Set.Finite.cast_ncard_eq
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
inst_1 : H.FiniteIndex
h : IsComplement (↑H : Set G) T
rw : Eq (α := ℕ∞) (↑T.ncard : ℕ∞) (↑H.index : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑H.index : ℕ∞) (↑H.index : ℕ∞)
⊢ T.encard = (↑H.index : ℕ∞)

Tactic:
rw [← h.finite_right.cast_ncard_eq, h.ncard_right]

Premises used: Subgroup.IsComplement.finite_right, Subgroup.IsComplement.ncard_right, Set.Finite.cast_ncard_eq
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
⊢ IsComplement (f • (↑T : Set G)) (↑H : Set G)

Tactic:
isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_

Premises used: Iff.mpr, Subgroup.isComplement_iff_existsUnique_inv_mul_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
refine : ∀ (g : G), ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
⊢ IsComplement (f • (↑T : Set G)) (↑H : Set G)

Tactic:
refine isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_

Premises used: Iff.mpr, Subgroup.isComplement_iff_existsUnique_inv_mul_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
obtain :
  ∀ (t : (↑(↑T : Set G) : Type u_1)) (ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G))
    (ht2 :
      ∀ (y : (↑(↑T : Set G) : Type u_1)),
        (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t),
    ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)

Tactic:
obtain ⟨t, ht1, ht2⟩ := isComplement_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)

Premises used: Inv.inv, Subgroup.isComplement_iff_existsUnique_inv_mul_mem, Iff.mp, HSMul.hSMul, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)

Tactic:
⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩

Premises used: Subtype.mk, ExistsUnique, And.intro, Exists.intro, HSMul.hSMul, Subtype.val, Subtype.property, Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
refine_1 :
  (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯)
refine_2 :
  ∀ (y : (↑(f • (↑T : Set G)) : Type u_1)),
    (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G)) y →
      y = Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)

Tactic:
refine ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
⊢ (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯)

Tactic:
smul_inv_smul f g ▸ QuotientAction.inv_mul_mem f ht1

Premises used: MulAction.QuotientAction.inv_mul_mem, Eq.rec, smul_inv_smul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
⊢ (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯)

Tactic:
exact smul_inv_smul f g ▸ QuotientAction.inv_mul_mem f ht1
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯) : G)⁻¹ * g ∈ (↑H : Set G)
⊢ (f⁻¹ • (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯) : G))⁻¹ * f⁻¹ • g ∈ H

Tactic:
replace h := QuotientAction.inv_mul_mem f⁻¹ h
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : (f⁻¹ • (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯) : G))⁻¹ * f⁻¹ • g ∈ H
refine_2 : ∀ (h : t'⁻¹ * f⁻¹ • g ∈ H), t' = (↑t : G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯

Tactic:
simp only [Subtype.ext_iff, smul_left_cancel_iff, inv_smul_smul] at h ⊢

Premises used: inv_smul_smul, Subtype.ext_iff, smul_left_cancel_iff
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : t'⁻¹ * f⁻¹ • g ∈ H
⊢ t' = (↑t : G)

Tactic:
Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)

Premises used: Subtype.ext_iff, Subtype.mk, Iff.mp