awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
simp_rw :
  (∀ (g : G), ∃! s : (↑S : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)) ↔
    ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
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
⊢ IsComplement S (↑H : Set G) ↔ ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
have simp_rw₂ : (∀ (g : G), ∃! s : (↑S : Type u_1), Eq (α := G ⧸ H) (↑(↑s : G) : G ⧸ H) (↑g : G ⧸ H)) ↔
  ∀ (q : G ⧸ H), ∃! s : (↑S : Type u_1), (↑(↑s : G) : G ⧸ H) = q
Tactic: simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq,
    QuotientGroup.forall_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H : Set G) T ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
have 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
Tactic: simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
    ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ IsComplement (↑H : Set G) T ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
have 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
Tactic: simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
    ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ IsComplement (↑H : Set G) T ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
have 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
Tactic: simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
    ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ IsComplement (↑H : Set G) T ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : (↑T : Type u_1), Quotient.mk'' (↑t : G) = q
have 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
Tactic: simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
    ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
h : IsComplement S (↑H : Set G)
⊢ S.ncard = H.index
have rw : Nat.card.{u_1} (↑S : Type u_1) = H.index
Tactic: rw [← Nat.card_coe_set_eq, h.card_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ S.ncard = H.index
have rw₁ : H.index = H.index
Tactic: rw [← Nat.card_coe_set_eq, h.card_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H : Set G) T
⊢ T.ncard = H.index
have rw : Nat.card.{u_1} (↑T : Type u_1) = H.index
Tactic: rw [← Nat.card_coe_set_eq, h.card_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ T.ncard = H.index
have rw₁ : H.index = H.index
Tactic: rw [← Nat.card_coe_set_eq, h.card_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), (↑(f q) : G ⧸ H) = q
⊢ IsComplement (range f) (↑H : Set G)
have rw : Bijective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)
Tactic: rw [isComplement_subgroup_right_iff_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
have refine : Injective (β := G ⧸ H) ((range f).restrict (π := fun (a : G) ↦ G ⧸ H) QuotientGroup.mk)
Tactic: refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ IsComplement (↑H : Set G) (range f)
have rw : Bijective (β := Quotient (QuotientGroup.rightRel H))
  ((range f).restrict (π := fun (a : G) ↦ Quotient (QuotientGroup.rightRel H)) Quotient.mk'')
Tactic: rw [isComplement_subgroup_left_iff_bijective]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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'')
have refine : Injective (β := 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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S
have refine : ∀ (q : G ⧸ H),
  (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
have pos : ∀ (hq : q = Quotient.mk'' g),
  (↑(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
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
have neg : ∀ (hq : ¬q = Quotient.mk'' g),
  (↑(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
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S
have refine : ∀ (q : G ⧸ H),
  (↑(update (β := fun (a : Quotient (QuotientGroup.leftRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) : G ⧸ H) = q
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']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
have 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
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']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ ∃ (S : Set G), IsComplement S (↑H : Set G) ∧ g ∈ S
have 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
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']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T
have refine : ∀ (q : Quotient (QuotientGroup.rightRel H)),
  Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q
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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q
have pos : ∀ (hq : q = Quotient.mk'' g),
  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
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q
have neg : ∀ (hq : ¬q = Quotient.mk'' g),
  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
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T
have refine : ∀ (q : Quotient (QuotientGroup.rightRel H)),
  Quotient.mk'' (update (β := fun (a : Quotient (QuotientGroup.rightRel H)) ↦ G) Quotient.out (Quotient.mk'' g) g q) = q
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']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
have 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
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']
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ ∃ (T : Set G), IsComplement (↑H : Set G) T ∧ g ∈ T
have 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
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']
-- 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'
⊢ ∃ (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
have this : H' = map H.subtype H''
Tactic: have : H' = H''.map H.subtype := by simp [H'', h]
-- 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 : H' = map H.subtype 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
have 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
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 : H' = map H.subtype 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
have 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
Tactic: obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_left 1
-- 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 : 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
have refine_1 : (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G) = (↑H : Set G)
Tactic: refine ⟨H.subtype '' S, ?_, ?_⟩
-- 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 : 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)
⊢ ∃ (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
have 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
Tactic: refine ⟨H.subtype '' S, ?_, ?_⟩
-- 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 S (↑H'' : Set ↥H)
⊢ (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G) = (↑H : Set G)
have this₁ : (⇑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
-- 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 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)
⊢ (⇑H.subtype : (a : ↥H) → G) '' S * (↑(map H.subtype H'') : Set G) = (↑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 (goal)
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} ↥H
have 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)
Tactic: rw [← 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 : 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)
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
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)
⊢ 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)
have refine_2₁ : Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} (↑(↑H'' : Set ↥H) : Type u_1)
Tactic: refine congr_arg₂ (· * ·) ?_ ?_
-- 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'
⊢ ∃ (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
have this : H' = map H.subtype H''
Tactic: have : H' = H''.map H.subtype := by simp [H'', h]
-- 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 : H' = map H.subtype 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
have 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
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 : H' = map H.subtype 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
have 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
Tactic: obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_right 1
-- 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 : 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
have refine_1 : (↑(map H.subtype H'') : Set G) * (⇑H.subtype : (a : ↥H) → G) '' S = (↑H : Set G)
Tactic: refine ⟨H.subtype '' S, ?_, ?_⟩
-- 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 : 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)
⊢ ∃ (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
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
Tactic: refine ⟨H.subtype '' S, ?_, ?_⟩