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
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
        ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2) :
      ↥H × (↑T : Type u_1))
have refine_2 : (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).1 :
    G) =
  (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
    G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
        ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2) :
      ↥H × (↑T : Type u_1))
have refine_2₁ : Eq (α := G)
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
          ((↑h : G) * g)).2 :
    G)
  (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).2 :
    G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
have refine_2 : (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).1 :
    G) =
  (↑h : G) *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
Tactic: rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
have refine_2₁ : (↑h : G) * g *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
              ((↑h : G) * g)).2 :
        G)⁻¹ =
  (↑h : G) *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
Tactic: rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₁ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
                ((↑h : G) * g)).2 :
          G)⁻¹ =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
have refine_2₂ : (↑h : G) * g *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
  (↑h : G) *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
Tactic: rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₁ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
                ((↑h : G) * g)).2 :
          G)⁻¹ =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₂ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
have refine_2₃ : (↑h : G) * g *
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
  (↑h : G) *
    (g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹)
Tactic: rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₁ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
                ((↑h : G) * g)).2 :
          G)⁻¹ =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₂ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
    (↑h : G) *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)
refine_2₃ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
    (↑h : G) *
      (g *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 :
            G)⁻¹)
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).1 :
      G)
have refine_2₄ : (↑h : G) *
    (g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 :
          G)⁻¹) =
  (↑h : G) *
    (g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹)
Tactic: rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
⊢ Eq (α := G)
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).2 :
      G)
    (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
            ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).2 :
      G)
have refine_2 : Eq (α := G)
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)
  (↑(h * ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1,
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2).2 :
    G)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ (hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) 1 =
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 hs1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 ht1)
have rw : Eq (α := G) (1 : G)
  ((hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 hs1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 ht1) :
    G)
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g ↔ g ∈ S
have mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g → g ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g → g ∈ S
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g ↔ g ∈ S
have mpr : g ∈ S → (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
⊢ g ∈ S
have mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) ∈ S
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : g ∈ S
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g
have mpr : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) g h) : G) = g
Tactic: rw [hST.equiv_fst_eq_self_of_mem_of_one_mem h1 h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g ↔ g ∈ T
have mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g → g ∈ T
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g → g ∈ T
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g ↔ g ∈ T
have mpr : g ∈ T → (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
⊢ g ∈ T
have mp : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ∈ T
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g
have mpr : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) g h) : G) = g
Tactic: rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ 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
have rw : g * (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ = 1 ↔ g ∈ T
Tactic: rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
rw : g * (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ = 1 ↔ 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
have rw₁ : g = (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) ↔ g ∈ T
Tactic: rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
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
⊢ 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
have rw₂ : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) = g ↔ g ∈ T
Tactic: rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
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
⊢ 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
have rw₃ : g ∈ T ↔ g ∈ T
Tactic: rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ 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
have rw : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g = 1 ↔ g ∈ S
Tactic: rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
rw : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g = 1 ↔ 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
have rw₁ : (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) = g ↔ g ∈ S
Tactic: rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
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
⊢ 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
have rw₂ : g ∈ S ↔ g ∈ S
Tactic: rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]
-- 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)
⊢ Finite.{u_1 + 1} (↑S : Type u_1) ↔ H.FiniteIndex
have rw : Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex
Tactic: rw [← h.leftQuotientEquiv.finite_iff]
-- 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
q : G ⧸ H
⊢ (↑((⋯.leftQuotientEquiv (S := range f) : (a : G ⧸ H) → (↑(range f) : Type u_1)) q) : G) = f q
have refine : Eq (α := { x : G // x ∈ range f })
  ((sorry.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) sorry : { x : G // x ∈ range f })
Tactic: refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)⁻¹ = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
have rw : g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)⁻¹⁻¹ = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
Tactic: rw [mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ ((↑(hS.toLeftFun (S := S) g) : G)⁻¹ * g)⁻¹ = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
have rw₁ : g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G) = g⁻¹ * (↑(hS.toLeftFun (S := S) g) : G)
Tactic: rw [mul_inv_rev, inv_inv]
-- 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
⊢ Finite.{u_1 + 1} (↑T : Type u_1) ↔ H.FiniteIndex
have rw : Finite.{u_1 + 1} (G ⧸ H) ↔ H.FiniteIndex
Tactic: rw [← h.rightQuotientEquiv.finite_iff,
    (QuotientGroup.quotientRightRelEquivQuotientLeftRel H).finite_iff]
-- 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
q : Quotient (QuotientGroup.rightRel H)
⊢ (↑((⋯.rightQuotientEquiv (T := range f) : (a : Quotient (QuotientGroup.rightRel H)) → (↑(range f) : Type u_1)) q) :
      G) =
    f q
have refine : Eq (α := { x : G // x ∈ range f })
  ((sorry.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) sorry : { x : G // x ∈ range f })
Tactic: refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)