awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  Bijective (β := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk'')
⊢ IsComplement (↑H : Set G) (range f)

Tactic:
rw [isComplement_subgroup_left_iff_bijective]

Premises used: Subgroup.isComplement_subgroup_left_iff_bijective
-- 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
⊢ Bijective (β := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.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 : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
refine :
  Injective (β := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk'')
⊢ Bijective (β := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.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 : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h :
  Eq (α := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk''
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.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 : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h :
  Eq (α := Quotient (QuotientGroup.rightRel H))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk''
      (Subtype.mk (p := fun (x : G) ↦ x ∈ range f) (f q₁) ⋯))
    ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.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
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S

Tactic:
⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
    QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Premises used: Function.update, QuotientGroup.mk, Quotient.out, Subgroup.isComplement_range_left, And.intro, Exists.intro, Set.range
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
refine :
  ∀ (q : G ⧸ H),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
    QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
pos :
  ∀ (hq : q = Quotient.mk'' g),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
neg :
  ∀ (hq : ¬q = Quotient.mk'' g),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Premises used: Quotient.mk''
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q

Tactic:
hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Premises used: Eq.rec, congr_arg, Eq.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q

Tactic:
simp [Function.update, dif_neg hq, q.out_eq']

Premises used: Quotient.out_eq', Function.update, dif_neg
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
refine :
  ∀ (q : G ⧸ H),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
pos :
  ∀ (q : G ⧸ H) (hq : q = Quotient.mk'' g),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
neg neg₁ :
  ∀ (q : G ⧸ H) (hq : ¬q = Quotient.mk'' g),
    (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S

Tactic:
classical
  refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
    QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
  by_cases hq : q = Quotient.mk'' g
  · exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
  · simp [Function.update, dif_neg hq, q.out_eq']

Premises used: Function.update, Quotient.mk''
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T

Tactic:
⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Premises used: Function.update, Subgroup.isComplement_range_right, Quotient.mk'', Quotient.out, And.intro, Exists.intro, Set.range
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
refine :
  ∀ (q : Quotient (QuotientGroup.rightRel H)),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
pos :
  ∀ (hq : q = Quotient.mk'' g),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
neg :
  ∀ (hq : ¬q = Quotient.mk'' g),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Premises used: Quotient.mk''
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Premises used: Eq.rec, congr_arg, Eq.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
simp [Function.update, dif_neg hq, q.out_eq']

Premises used: Quotient.out_eq', Function.update, dif_neg
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
refine :
  ∀ (q : Quotient (QuotientGroup.rightRel H)),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
pos :
  ∀ (q : Quotient (QuotientGroup.rightRel H)) (hq : q = Quotient.mk'' g),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
neg neg₁ :
  ∀ (q : Quotient (QuotientGroup.rightRel H)) (hq : ¬q = Quotient.mk'' g),
    Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) =
      q
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T

Tactic:
classical
  refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
  by_cases hq : q = Quotient.mk'' g
  · exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
  · simp [Function.update, dif_neg hq, q.out_eq']

Premises used: Function.update, Quotient.mk''
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ H' = map H.subtype H''

Tactic:
simp [H'', h]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ H' = map H.subtype H''

Tactic:
have : H' = H''.map H.subtype := by simp [H'', h]
-- Module: Mathlib.GroupTheory.Complement
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''
rw :
  ∃ (S : Set G),
    S * (↑(map H.subtype H'') : Set G) = (↑H : Set G) ∧
      Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H
⊢ ∃ (S : Set G),
    S * (↑H' : Set G) = (↑H : Set G) ∧ Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥H' = Nat.card.{u_1} ↥H

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Complement
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''
obtain :
  ∀ (S : Set ↥H) (cmem : IsComplement S (↑H'' : Set ↥H)),
    ∃ (S : Set G),
      S * (↑(map H.subtype H'') : Set G) = (↑H : Set G) ∧
        Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H
⊢ ∃ (S : Set G),
    S * (↑(map H.subtype H'') : Set G) = (↑H : Set G) ∧
      Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H

Tactic:
obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_left 1

Premises used: Subgroup.exists_isComplement_left, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ ∃ (S : Set G),
    S * (↑(map H.subtype H'') : Set G) = (↑H : Set G) ∧
      Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H

Tactic:
⟨H.subtype '' S, ?_, ?_⟩

Premises used: Subgroup.subtype, And.intro, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
refine_1 : (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G) = (↑H : Set G)
refine_2 :
  Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') =
    Nat.card.{u_1} ↥H
⊢ ∃ (S : Set G),
    S * (↑(map H.subtype H'') : Set G) = (↑H : Set G) ∧
      Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H

Tactic:
refine ⟨H.subtype '' S, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ (⇑H.subtype : (a : ↥H) → G) '' (S * (↑H'' : Set ↥H)) =
    (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G)

Tactic:
have : H.subtype '' (S * H'') = H.subtype '' S * H''.map H.subtype := image_mul H.subtype
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
this :
  (⇑H.subtype : (a : ↥H) → G) '' (S * (↑H'' : Set ↥H)) =
    (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G)
refine_1 : image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) univ = (↑H : Set G)
⊢ (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G) = (↑H : Set G)

Tactic:
rw [← this, cmem.mul_eq]

Premises used: Subgroup.IsComplement.mul_eq
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
this :
  (⇑H.subtype : (a : ↥H) → G) '' (S * (↑H'' : Set ↥H)) =
    (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G)
⊢ image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) univ = (↑H : Set G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
refine_2 :
  Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') =
    Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') =
    Nat.card.{u_1} ↥H

Tactic:
rw [← cmem.card_mul_card]

Premises used: Subgroup.IsComplement.card_mul_card
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') =
    Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)

Tactic:
congr_arg₂ (· * ·) ?_ ?_

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
refine_2 : Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)
refine_2₁ : Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) * Nat.card.{u_1} ↥(map H.subtype H'') =
    Nat.card.{u_1} (↑S : Type u_1) * Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)

Tactic:
Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)

Tactic:
Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
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 S (↑H'' : Set ↥H)
⊢ Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
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''
rw :
  ∃ (S : Set G),
    (↑(map H.subtype H'') : Set G) * S = (↑H : Set G) ∧
      Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ ∃ (S : Set G),
    (↑H' : Set G) * S = (↑H : Set G) ∧ Nat.card.{u_1} ↥H' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Complement
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''
obtain :
  ∀ (S : Set ↥H) (cmem : IsComplement (↑H'' : Set ↥H) S),
    ∃ (S : Set G),
      (↑(map H.subtype H'') : Set G) * S = (↑H : Set G) ∧
        Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ ∃ (S : Set G),
    (↑(map H.subtype H'') : Set G) * S = (↑H : Set G) ∧
      Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H

Tactic:
obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_right 1

Premises used: OfNat.ofNat, Subgroup.exists_isComplement_right
-- Module: Mathlib.GroupTheory.Complement
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
⊢ ∃ (S : Set G),
    (↑(map H.subtype H'') : Set G) * S = (↑H : Set G) ∧
      Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H

Tactic:
⟨H.subtype '' S, ?_, ?_⟩

Premises used: Subgroup.subtype, And.intro, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.GroupTheory.Complement
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
refine_1 : (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S = (↑H : Set G)
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
⊢ ∃ (S : Set G),
    (↑(map H.subtype H'') : Set G) * S = (↑H : Set G) ∧
      Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H

Tactic:
refine ⟨H.subtype '' S, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Complement
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
⊢ (⇑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
-- Module: Mathlib.GroupTheory.Complement
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
refine_1 : image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) univ = (↑H : Set G)
⊢ (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S = (↑H : Set G)

Tactic:
rw [← this, cmem.mul_eq]

Premises used: Subgroup.IsComplement.mul_eq
-- Module: Mathlib.GroupTheory.Complement
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
⊢ image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) univ = (↑H : Set G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
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} ↥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
-- Module: Mathlib.GroupTheory.Complement
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.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)
⊢ 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

Tactic:
rw [← this]