awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
e_a :
  b • (↑(Hom.hom f).range : Set (↑B : Type u)) =
    HSMul.hSMul (α := (↑B : Type u)) 1 (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ b • (↑(Hom.hom f).range : Set (↑B : Type u)) = (↑(Hom.hom f).range : Set (↑B : Type u))

Tactic:
nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm]

Premises used: MonoidHom.range, one_leftCoset, GrpCat.Hom.hom, SetLike.coe, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
e_a : b⁻¹ ∈ (Hom.hom f).range
⊢ b • (↑(Hom.hom f).range : Set (↑B : Type u)) =
    HSMul.hSMul (α := (↑B : Type u)) 1 (↑(Hom.hom f).range : Set (↑B : Type u))

Tactic:
rw [leftCoset_eq_iff, mul_one]

Premises used: leftCoset_eq_iff, mul_one
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ ∈ (Hom.hom f).range

Tactic:
Subgroup.inv_mem _ hb

Premises used: Subgroup.inv_mem
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ ∈ (Hom.hom f).range

Tactic:
exact Subgroup.inv_mem _ hb

Premises used: Subgroup.inv_mem
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r :
  Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
⊢ b • (↑(Hom.hom f).range : Set (↑B : Type u)) = (↑(Hom.hom f).range : Set (↑B : Type u))

Tactic:
simp only [fromCoset.injEq, Subtype.mk.injEq] at r

Premises used: GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset.injEq, Subtype.mk.injEq
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : b • (↑(Hom.hom f).range : Set (↑B : Type u)) = (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ b • (↑(Hom.hom f).range : Set (↑B : Type u)) =
    HSMul.hSMul (α := (↑B : Type u)) 1 (↑(Hom.hom f).range : Set (↑B : Type u))

Tactic:
nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm] at r

Premises used: MonoidHom.range, one_leftCoset, GrpCat.Hom.hom, SetLike.coe, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r :
  b • (↑(Hom.hom f).range : Set (↑B : Type u)) =
    HSMul.hSMul (α := (↑B : Type u)) 1 (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ b⁻¹ ∈ (Hom.hom f).range

Tactic:
rw [leftCoset_eq_iff, mul_one] at r

Premises used: leftCoset_eq_iff, mul_one
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False

Tactic:
hb (inv_inv b ▸ Subgroup.inv_mem _ r)

Premises used: Eq.rec, Subgroup.inv_mem, inv_inv
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False

Tactic:
exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)

Premises used: Eq.rec, Subgroup.inv_mem, inv_inv
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
⊢ Eq (α := X') ((τ : (a : X') → X') ∞ : X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
          Membership.mem (γ := Set (Set (↑B : Type u)))
            (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
      X')

Tactic:
Equiv.swap_apply_right _ _

Premises used: Equiv.swap_apply_right
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
⊢ Eq (α := X')
    ((τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
            Membership.mem (γ := Set (Set (↑B : Type u)))
              (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    (∞ : X')

Tactic:
Equiv.swap_apply_left _ _

Premises used: Equiv.swap_apply_left
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
⊢ Eq (α := X')
    ((τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
            Membership.mem (γ := Set (Set (↑B : Type u)))
              (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
            (x • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯)) :
      X')
    (∞ : X')

Tactic:
(fromCoset_eq_of_mem_range _ hx).symm ▸ τ_apply_fromCoset _

Premises used: GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset, GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
rw :
  Eq (α := X')
    ((Equiv.symm
            (Equiv.swap
              (fromCoset
                (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                  (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
              ∞) :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    (∞ : X')
rw₁ :
  Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    (∞ : X')
rw₂ rw₃ : Eq.{u + 1} (α := X') ∞ ∞
⊢ Eq (α := X')
    ((Equiv.symm τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    (∞ : X')

Tactic:
rw [tau, Equiv.symm_swap, Equiv.swap_apply_left]

Premises used: Equiv.symm_swap, GrpCat.SurjectiveOfEpiAuxs.tau, Equiv.swap_apply_left
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
rw :
  Eq (α := X')
    ((Equiv.symm
            (Equiv.swap
              (fromCoset
                (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                  (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
              ∞) :
          (a : X') → X')
        ∞ :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
      X')
rw₁ :
  Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        ∞ :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
      X')
rw₂ rw₃ :
  Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
⊢ Eq (α := X') ((Equiv.symm τ : (a : X') → X') ∞ : X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
      X')

Tactic:
rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]

Premises used: Equiv.symm_swap, GrpCat.SurjectiveOfEpiAuxs.tau, Equiv.swap_apply_right
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
β : (↑B : Type u)
x : X'
dsimp : β⁻¹ • β • x = x
⊢ (fun (x : X') ↦ β⁻¹ • x) ((fun (x : X') ↦ β • x) x) = x

Tactic:
dsimp only
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
β : (↑B : Type u)
x : X'
rw : (β⁻¹ * β) • x = x
rw₁ : HSMul.hSMul (α := (↑B : Type u)) 1 x = x
rw₂ rw₃ : x = x
⊢ β⁻¹ • β • x = x

Tactic:
rw [← mul_smul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, GrpCat.SurjectiveOfEpiAuxs.mul_smul, GrpCat.SurjectiveOfEpiAuxs.one_smul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
β : (↑B : Type u)
x : X'
dsimp : β • β⁻¹ • x = x
⊢ (fun (x : X') ↦ β • x) ((fun (x : X') ↦ β⁻¹ • x) x) = x

Tactic:
dsimp only
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
β : (↑B : Type u)
x : X'
rw : (β * β⁻¹) • x = x
rw₁ : HSMul.hSMul (α := (↑B : Type u)) 1 x = x
rw₂ rw₃ : x = x
⊢ β • β⁻¹ • x = x

Tactic:
rw [← mul_smul, mul_inv_cancel, one_smul]

Premises used: mul_inv_cancel, GrpCat.SurjectiveOfEpiAuxs.mul_smul, GrpCat.SurjectiveOfEpiAuxs.one_smul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
H :
  ∀ (x : X'),
    Eq (α := X')
      (({ toFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1 x,
              invFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1⁻¹ x, left_inv := ⋯, right_inv := ⋯ } :
            (a : X') → X')
          x :
        X')
      ((1 : (a : X') → X') x : X')
⊢ Eq.{u + 1} (α := SX')
    { toFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1 x,
      invFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1⁻¹ x, left_inv := ⋯, right_inv := ⋯ }
    1

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : X'
⊢ Eq (α := X')
    (({ toFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1 x,
            invFun := fun (x : X') ↦ HSMul.hSMul (α := (↑B : Type u)) 1⁻¹ x, left_inv := ⋯, right_inv := ⋯ } :
          (a : X') → X')
        x :
      X')
    ((1 : (a : X') → X') x : X')

Tactic:
simp [one_smul]

Premises used: GrpCat.SurjectiveOfEpiAuxs.one_smul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b1 b2 : (↑B : Type u)
H :
  ∀ (x : X'),
    Eq (α := X')
      (({ toFun := fun (x : X') ↦ (b1 * b2) • x, invFun := fun (x : X') ↦ (b1 * b2)⁻¹ • x, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : X') → X')
          x :
        X')
      ((HMul.hMul (α := SX')
              { toFun := fun (x : X') ↦ b1 • x, invFun := fun (x : X') ↦ b1⁻¹ • x, left_inv := ⋯, right_inv := ⋯ :
                X' ≃ X' }
              { toFun := fun (x : X') ↦ b2 • x, invFun := fun (x : X') ↦ b2⁻¹ • x, left_inv := ⋯, right_inv := ⋯ :
                X' ≃ X' } :
            (a : X') → X')
          x :
        X')
⊢ { toFun := fun (x : X') ↦ (b1 * b2) • x, invFun := fun (x : X') ↦ (b1 * b2)⁻¹ • x, left_inv := ⋯, right_inv := ⋯ } =
    HMul.hMul (α := SX')
      { toFun := fun (x : X') ↦ b1 • x, invFun := fun (x : X') ↦ b1⁻¹ • x, left_inv := ⋯, right_inv := ⋯ : X' ≃ X' }
      { toFun := fun (x : X') ↦ b2 • x, invFun := fun (x : X') ↦ b2⁻¹ • x, left_inv := ⋯, right_inv := ⋯ : X' ≃ X' }

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b1 b2 : (↑B : Type u)
x : X'
⊢ Eq (α := X')
    (({ toFun := fun (x : X') ↦ (b1 * b2) • x, invFun := fun (x : X') ↦ (b1 * b2)⁻¹ • x, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : X') → X')
        x :
      X')
    ((HMul.hMul (α := SX')
            { toFun := fun (x : X') ↦ b1 • x, invFun := fun (x : X') ↦ b1⁻¹ • x, left_inv := ⋯, right_inv := ⋯ :
              X' ≃ X' }
            { toFun := fun (x : X') ↦ b2 • x, invFun := fun (x : X') ↦ b2⁻¹ • x, left_inv := ⋯, right_inv := ⋯ :
              X' ≃ X' } :
          (a : X') → X')
        x :
      X')

Tactic:
simp [mul_smul]

Premises used: GrpCat.SurjectiveOfEpiAuxs.mul_smul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
H :
  ∀ (x : X'),
    Eq (α := X') ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') 1)) τ : (a : X') → X') x : X')
      ((1 : (a : X') → X') x : X')
⊢ Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') 1)) τ = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : X'
⊢ Eq (α := X') ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') 1)) τ : (a : X') → X') x : X')
    ((1 : (a : X') → X') x : X')

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b1 b2 : (↑B : Type u)
H :
  ∀ (x : X'),
    Eq (α := X')
      ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') (b1 * b2))) τ : (a : X') → X') x : X')
      ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b1)) τ *
              Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b2)) τ :
            (a : X') → X')
          x :
        X')
⊢ Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') (b1 * b2))) τ =
    Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b1)) τ *
      Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b2)) τ

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b1 b2 : (↑B : Type u)
x : X'
⊢ Eq (α := X')
    ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') (b1 * b2))) τ : (a : X') → X') x : X')
    ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b1)) τ *
            Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') b2)) τ :
          (a : X') → X')
        x :
      X')

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
y : (↑X : Type u)
obtain :
  ∀ (z : (↑B : Type u))
    (hz : (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) z = (↑y : Set (↑B : Type u))),
    Membership.mem (γ := Set (Set (↑B : Type u))) X (x • (↑y : Set (↑B : Type u)))
⊢ Membership.mem (γ := Set (Set (↑B : Type u))) X (x • (↑y : Set (↑B : Type u)))

Tactic:
obtain ⟨z, hz⟩ := y.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
y : (↑X : Type u)
z : (↑B : Type u)
hz : (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) z = (↑y : Set (↑B : Type u))
⊢ (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) (x * z) = x • (↑y : Set (↑B : Type u))

Tactic:
simp [← hz, smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
y : (↑X : Type u)
z : (↑B : Type u)
hz : (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) z = (↑y : Set (↑B : Type u))
⊢ Membership.mem (γ := Set (Set (↑B : Type u))) X (x • (↑y : Set (↑B : Type u)))

Tactic:
exact ⟨x * z, by simp [← hz, smul_smul]⟩
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
y : (↑(Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) : Type u)
⊢ (((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X') (fromCoset y) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
        Membership.mem (γ := Set (Set (↑B : Type u)))
          (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
        (x • (↑y : Set (↑B : Type u))) ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
⊢ Eq (α := X') ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X') ∞ : X') (∞ : X')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
rw :
  Eq (α := X')
    ((τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (x •
              (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                    (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
                Set (↑B : Type u)))
            ⋯)) :
      X')
    (∞ : X')
⊢ Eq (α := X')
    ((τ : (a : X') → X')
        ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X') ((Equiv.symm τ : (a : X') → X') ∞)) :
      X')
    (∞ : X')

Tactic:
rw [τ_symm_apply_infinity, g_apply_fromCoset]

Premises used: GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
⊢ Eq (α := X')
    ((τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (x •
              (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                    (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
                Set (↑B : Type u)))
            ⋯)) :
      X')
    (∞ : X')

Tactic:
simpa only using τ_apply_fromCoset' f x hx

Premises used: GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset'
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
⊢ Eq (α := X')
    ((Equiv.trans ((Equiv.symm τ).trans ((g : (a : (↑B : Type u)) → SX') x)) τ : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯) :
      X')

Tactic:
simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]

Premises used: GrpCat.SurjectiveOfEpiAuxs.τ_apply_infinity, GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity, MonoidHom.coe_range, GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
⊢ Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
            Membership.mem (γ := Set (Set (↑B : Type u)))
              (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
            (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯)) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
          Membership.mem (γ := Set (Set (↑B : Type u)))
            (Set.range fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) x)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')

Tactic:
(fromCoset_eq_of_mem_range _ hb).symm ▸ h_apply_fromCoset f x

Premises used: GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range, Eq.rec, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
⊢ Ne (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
    ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
rw :
  Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
⊢ Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
          ((Equiv.symm
                (Equiv.swap
                  (fromCoset
                    (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                      (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
                  ∞) :
              (a : X') → X')
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯)))) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')

Tactic:
rw [Equiv.symm_swap,
    @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) ∞
      (fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]

Premises used: Equiv.symm_swap
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
simp :
  Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯)) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
⊢ Eq (α := X')
    ((Equiv.swap
            (fromCoset
              (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
            ∞ :
          (a : X') → X')
        ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')

Tactic:
simp only [g_apply_fromCoset, leftCoset_assoc]

Premises used: leftCoset_assoc, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset