awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2

Premises used: Prod.ext_iff, Subtype.ext_iff, And.right, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
g : G
⊢ IsComplement (G := G) univ {g}

Tactic:
isComplement_univ_singleton

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

Tactic:
exact isComplement_univ_singleton

Premises used: Subgroup.isComplement_univ_singleton
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
⊢ IsComplement S univ ↔ ∃ (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 S univ), S.Nonempty
refine_2 : ∀ (h : IsComplement S univ) (a : G) (ha : a ∈ S) (b : G) (hb : b ∈ S), a = b
refine_3 : (∃ (g : G), S = {g}) → IsComplement S univ
⊢ IsComplement S univ ↔ ∃ (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 S univ
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
⊢ 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 S univ
a : (↑S : Type u_1) × (↑univ : Type u_1)
h_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:
⟨a.1.1, a.1.2⟩

Premises used: Prod.fst, Set.Nonempty, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement S univ
a : (↑S : Type u_1) × (↑univ : Type u_1)
h_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:
exact ⟨a.1.1, a.1.2⟩
-- Module: Mathlib.GroupTheory.Complement
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
⊢ 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⁻¹ ⋯) :
      (↑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⁻¹ ⋯) :
      (↑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)
-- Module: Mathlib.GroupTheory.Complement
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
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⁻¹ ⋯) :
      (↑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⁻¹ ⋯) :
      (↑S : Type u_1) × (↑⊤ : Type u_1))
⊢ a = b

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

Premises used: Prod.ext_iff, Subtype.ext_iff, And.left, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
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
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⁻¹ ⋯) :
      (↑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⁻¹ ⋯) :
      (↑S : Type u_1) × (↑⊤ : Type u_1))
⊢ a = b

Tactic:
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1

Premises used: Prod.ext_iff, Subtype.ext_iff, And.left, Iff.mp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
g : G
⊢ IsComplement (G := G) {g} univ

Tactic:
isComplement_singleton_univ

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

Tactic:
exact isComplement_singleton_univ

Premises used: Subgroup.isComplement_singleton_univ
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
h : IsComplement S T
x : G
⊢ x ∈ S * T

Tactic:
simpa [mem_mul] using (h.existsUnique x).exists

Premises used: ExistsUnique.exists, Subgroup.IsComplement.existsUnique, Set.mem_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
T : Set G
h : IsComplement ∅ T
⊢ False

Tactic:
simpa [eq_comm (a := ∅)] using h.mul_eq

Premises used: eq_comm, Subgroup.IsComplement.mul_eq
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S : Set G
h : IsComplement S ∅
⊢ False

Tactic:
simpa [eq_comm (a := ∅)] using h.mul_eq

Premises used: eq_comm, Subgroup.IsComplement.mul_eq
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
contrapose! : ∀ (hst : S = ∅), ¬IsComplement S T
⊢ S.Nonempty

Tactic:
contrapose! hst
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T

Tactic:
simp [hst]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
contrapose! : ∀ (hst : T = ∅), ¬IsComplement S T
⊢ T.Nonempty

Tactic:
contrapose! hst
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T

Tactic:
simp [hst]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
c : G
hc : c ∈ T
d : G
hd : d ∈ T
⊢ (Subtype.mk (p := fun (x : G) ↦ x ∈ S) a ha, Subtype.mk (p := fun (x : G) ↦ x ∈ T) c hc) ≠
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) b hb, Subtype.mk (p := fun (x : G) ↦ x ∈ T) d hd)

Tactic:
simp [hab]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
c : G
hc : c ∈ T
d : G
hd : d ∈ T
⊢ Ne.{u_1 + 1} (α := G) ((fun (x : G) ↦ a • x) c) ((fun (x : G) ↦ b • x) d)

Tactic:
exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂ := (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])

Premises used: Function.Injective.ne, And.left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
h : IsComplement S T
⊢ Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} (↑T : Type u_1) = Nat.card G

Tactic:
(Nat.card_prod _ _).symm.trans <| Nat.card_congr <| Equiv.ofBijective _ h

Premises used: Nat.card_congr, Equiv.ofBijective, Nat.card_prod, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
⊢ IsComplement'.{u_1} (G := G) ⊤ ⊥

Tactic:
isComplement_univ_singleton

Premises used: Set.univ, setOf, Set.singleton, Subgroup.isComplement_univ_singleton
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
⊢ IsComplement'.{u_1} (G := G) ⊥ ⊤

Tactic:
isComplement_singleton_univ

Premises used: Subgroup.isComplement_singleton_univ, Set.univ, setOf, Set.singleton
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsComplement' ⊥ H ↔ H = ⊤

Tactic:
isComplement_singleton_left.trans coe_eq_univ

Premises used: setOf, Subgroup.isComplement_singleton_left, Set.singleton, Subgroup.coe_eq_univ, Iff.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.IsComplement' ⊥ ↔ H = ⊤

Tactic:
isComplement_singleton_right.trans coe_eq_univ

Premises used: Subgroup.isComplement_singleton_right, setOf, Set.singleton, Subgroup.coe_eq_univ, Iff.trans
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsComplement' ⊤ H ↔ H = ⊥

Tactic:
isComplement_univ_left.trans coe_eq_singleton

Premises used: Set.univ, setOf, Iff.trans, Subgroup.coe_eq_singleton, Subgroup.isComplement_univ_left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.IsComplement' ⊤ ↔ H = ⊥

Tactic:
isComplement_univ_right.trans coe_eq_singleton

Premises used: Set.univ, setOf, Iff.trans, Subgroup.isComplement_univ_right, Subgroup.coe_eq_singleton
-- 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:
isComplement_iff_existsUnique

Premises used: Subgroup.isComplement_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
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
⊢ IsComplement S T ↔ ∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T

Tactic:
convert! isComplement_iff_existsUnique with g

Premises used: Subgroup.isComplement_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
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
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
⊢ (∃! 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
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1)
hx : (↑x : G)⁻¹ * g ∈ T
hx' : ∀ (y : (↑S : Type u_1)), (fun (s : (↑S : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ T) y → y = x
⊢ (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g)
    (x, Subtype.mk (p := fun (x : G) ↦ x ∈ T) ((↑x : G)⁻¹ * g) hx)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1)
hx : (↑x : G)⁻¹ * g ∈ T
hx' : ∀ (y : (↑S : Type u_1)), (fun (s : (↑S : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ T) y → y = x
⊢ ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y →
      y = (x, Subtype.mk (p := fun (x : G) ↦ x ∈ T) ((↑x : G)⁻¹ * g) hx)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1)
hx : (↑x : G)⁻¹ * g ∈ T
hx' : ∀ (y : (↑S : Type u_1)), (fun (s : (↑S : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
exact ⟨(x, ⟨_, hx⟩), by simp, by aesop⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
⊢ (fun (s : (↑S : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ T) x.1

Tactic:
simp [← hx]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
y : (↑S : Type u_1)
hy : (fun (s : (↑S : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ T) y
⊢ (y, Subtype.mk (p := fun (x : G) ↦ x ∈ T) ((↑y : G)⁻¹ * g) hy) = x

Tactic:
simpa using hx' (y, ⟨_, hy⟩)

Premises used: Prod.mk, Subtype.mk
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
⊢ ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ T

Tactic:
exact ⟨x.1, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (y, ⟨_, hy⟩)).1⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
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
⊢ IsComplement S T ↔ ∀ (g : G), ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S

Tactic:
convert! isComplement_iff_existsUnique with g

Premises used: Subgroup.isComplement_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
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
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
⊢ (∃! 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
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑T : Type u_1)
hx : g * (↑x : G)⁻¹ ∈ S
hx' : ∀ (y : (↑T : Type u_1)), (fun (t : (↑T : Type u_1)) ↦ g * (↑t : G)⁻¹ ∈ S) y → y = x
⊢ (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (↑x : G)⁻¹) hx, x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑T : Type u_1)
hx : g * (↑x : G)⁻¹ ∈ S
hx' : ∀ (y : (↑T : Type u_1)), (fun (t : (↑T : Type u_1)) ↦ g * (↑t : G)⁻¹ ∈ S) y → y = x
⊢ ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y →
      y = (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (↑x : G)⁻¹) hx, x)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑T : Type u_1)
hx : g * (↑x : G)⁻¹ ∈ S
hx' : ∀ (y : (↑T : Type u_1)), (fun (t : (↑T : Type u_1)) ↦ g * (↑t : G)⁻¹ ∈ S) y → y = x
⊢ ∃! x : (↑S : Type u_1) × (↑T : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g

Tactic:
exact ⟨(⟨_, hx⟩, x), by simp, by aesop⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
⊢ (fun (t : (↑T : Type u_1)) ↦ g * (↑t : G)⁻¹ ∈ S) x.2

Tactic:
simp [← hx]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
y : (↑T : Type u_1)
hy : (fun (t : (↑T : Type u_1)) ↦ g * (↑t : G)⁻¹ ∈ S) y
⊢ (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (↑y : G)⁻¹) hy, y) = x

Tactic:
simpa using hx' (⟨_, hy⟩, y)

Premises used: Prod.mk, Subtype.mk
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
g : G
x : (↑S : Type u_1) × (↑T : Type u_1)
hx : (↑x.1 : G) * (↑x.2 : G) = g
hx' :
  ∀ (y : (↑S : Type u_1) × (↑T : Type u_1)),
    (fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G) = g) y → y = x
⊢ ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ S

Tactic:
exact ⟨x.2, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (⟨_, hy⟩, y)).2⟩
-- Module: Mathlib.GroupTheory.Complement
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
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
simp_rw₂ :
  (∀ (g : G), ∃! s : (↑S : Type u_1), Eq (α := G ⧸ H) (↑(↑s : G) : G ⧸ H) (↑g : G ⧸ H)) ↔
    ∀ (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

Tactic:
simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq,
    QuotientGroup.forall_mk]

Premises used: QuotientGroup.eq, SetLike.mem_coe, Subgroup.isComplement_iff_existsUnique_inv_mul_mem, QuotientGroup.forall_mk
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
simp_rw :
  (∀ (g : G), ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ (↑H : Set G)) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
simp_rw₁ :
  (∀ (g : G), ∃! t : (↑T : Type u_1), g * (↑t : G)⁻¹ ∈ H) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
simp_rw₂ :
  (∀ (g : G), ∃! t : (↑T : Type u_1), (QuotientGroup.rightRel H : G → G → Prop) (↑t : G) g) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
simp_rw₃ :
  (∀ (g : G),
      ∃! t : (↑T : Type u_1),
        Eq (α := Quotient (QuotientGroup.rightRel H)) (Quotient.mk'' (↑t : G)) (Quotient.mk'' g)) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
⊢ IsComplement (↑H : Set G) T ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q

Tactic:
simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
    ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]

Premises used: Quotient.forall, Quotient.eq'', QuotientGroup.rightRel_apply, SetLike.mem_coe, Subgroup.isComplement_iff_existsUnique_mul_inv_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S (↑H : Set G) ↔ Bijective (β := G ⧸ H) (S.restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)

Tactic:
isComplement_subgroup_right_iff_existsUnique_quotientGroupMk.trans
    (bijective_iff_existsUnique (S.restrict QuotientGroup.mk)).symm

Premises used: QuotientGroup.mk, Iff.trans, Set.restrict, Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk, Iff.symm, Function.bijective_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H : Set G) T ↔
    Bijective (β := Quotient (QuotientGroup.rightRel H))
      (T.restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk'')

Tactic:
isComplement_subgroup_left_iff_existsUnique_quotientMk''.trans
    (bijective_iff_existsUnique (T.restrict Quotient.mk'')).symm

Premises used: Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'', Quotient.mk'', Iff.trans, Set.restrict, Iff.symm, Function.bijective_iff_existsUnique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
h : IsComplement S (↑H : Set G)
⊢ Nat.card.{u_1} (↑S : Type u_1) = H.index

Tactic:
Nat.card_congr <| .ofBijective _ <| isComplement_subgroup_right_iff_bijective.mp h

Premises used: Nat.card_congr, Subgroup.index, Equiv.ofBijective, Iff.mp, Subgroup.isComplement_subgroup_right_iff_bijective
-- 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 : Nat.card.{u_1} (↑S : Type u_1) = H.index
rw₁ rw₂ : H.index = H.index
⊢ S.ncard = H.index

Tactic:
rw [← Nat.card_coe_set_eq, h.card_left]

Premises used: Nat.card_coe_set_eq, Subgroup.IsComplement.card_left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H : Set G) T
⊢ Nat.card.{u_1} (↑T : Type u_1) = H.index

Tactic:
Nat.card_congr <| (Equiv.ofBijective _ <| isComplement_subgroup_left_iff_bijective.mp h).trans <|
    QuotientGroup.quotientRightRelEquivQuotientLeftRel H

Premises used: Equiv.trans, QuotientGroup.quotientRightRelEquivQuotientLeftRel, Nat.card_congr, Subgroup.isComplement_subgroup_left_iff_bijective, Subgroup.index, Equiv.ofBijective, Iff.mp
-- 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 : Nat.card.{u_1} (↑T : Type u_1) = H.index
rw₁ rw₂ : H.index = H.index
⊢ T.ncard = H.index

Tactic:
rw [← Nat.card_coe_set_eq, h.card_right]

Premises used: Nat.card_coe_set_eq, Subgroup.IsComplement.card_right
-- 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
rw : Bijective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)
⊢ IsComplement (range f) (↑H : Set G)

Tactic:
rw [isComplement_subgroup_right_iff_bijective]

Premises used: Subgroup.isComplement_subgroup_right_iff_bijective
-- 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
⊢ Bijective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)

Tactic:
⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Function.Bijective, rfl
-- 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
refine : Injective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)
⊢ Bijective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)

Tactic:
refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩
-- 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₁ q₂ : G ⧸ H
h :
  Eq (α := G ⧸ H)
    ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯))
    ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₂) ⋯))
⊢ Eq (α := (↑(range f) : Type u_1)) (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₂) ⋯)

Tactic:
Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Premises used: congr_arg, Eq.symm, Eq.trans, Subtype.ext
-- 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₁ q₂ : G ⧸ H
h :
  Eq (α := G ⧸ H)
    ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯))
    ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₂) ⋯))
⊢ Eq (α := (↑(range f) : Type u_1)) (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₂) ⋯)

Tactic:
exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Premises used: congr_arg, Eq.symm, Eq.trans, Subtype.ext