awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
y : (↑X : Type u)
⊢ Membership.mem (γ := Set (Set (↑B : Type u))) X (x • (↑y : Set (↑B : Type u)))
have 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)))
Tactic: obtain ⟨z, hz⟩ := y.2
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
⊢ Eq (α := X')
    ((τ : (a : X') → X')
        ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X') ((Equiv.symm τ : (a : X') → X') ∞)) :
      X')
    (∞ : X')
have 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)) sorry) :
              Set (↑B : Type u)))
          sorry)) :
    X')
  (∞ : X')
Tactic: rw [τ_symm_apply_infinity, g_apply_fromCoset]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
⊢ 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')
have 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)) sorry))
          ∞ :
        (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))) sorry))) :
    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))) sorry) :
    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)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
⊢ 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')
have 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)) sorry))
          ∞ :
        (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))) sorry)) :
    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))) sorry) :
    X')
Tactic: simp only [g_apply_fromCoset, leftCoset_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
⊢ 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')
have refine : ∀ (r : x * b ∈ (Hom.hom f).range), b ∈ (Hom.hom f).range
Tactic: refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
r : x * b ∈ (Hom.hom f).range
⊢ b ∈ (Hom.hom f).range
have h : b = x⁻¹ * (x * b)
Tactic: convert! Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * (x * b)
have h : b = x⁻¹ * x * b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
r : x * b ∈ (Hom.hom f).range
h : b = x⁻¹ * x * b
⊢ b = x⁻¹ * (x * b)
have h₁ : b = 1 * b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
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
r : x * b ∈ (Hom.hom f).range
h : b = x⁻¹ * x * b
h₁ : b = 1 * b
⊢ b = x⁻¹ * (x * b)
have h₂ : b = b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
⊢ (↑(Hom.hom f).range : Set (↑B : Type u)) =
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
have refine_1 : ∀ b ∈ (↑(Hom.hom f).range : Set (↑B : Type u)),
  Membership.mem (γ := Set (↑B : Type u))
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
    b
Tactic: refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
refine_1 :
  ∀ b ∈ (↑(Hom.hom f).range : Set (↑B : Type u)),
    Membership.mem (γ := Set (↑B : Type u))
      {x : (↑B : Type u) |
        Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
      b
⊢ (↑(Hom.hom f).range : Set (↑B : Type u)) =
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
have refine_2 : ∀ (b : (↑B : Type u))
  (hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX'))
  (r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))), False
Tactic: refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
⊢ Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
have refine_1 : Eq (α := SX')
  ((h : (a : (↑B : Type u)) → SX')
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a :
        (↑B : Type u)) :
    SX')
  ((g : (a : (↑B : Type u)) → SX')
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a :
        (↑B : Type u)) :
    SX')
Tactic: change h (f a) = g (f a)
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
⊢ Eq (α := SX')
    ((h : (a : (↑B : Type u)) → SX')
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      SX')
    ((g : (a : (↑B : Type u)) → SX')
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      SX')
have refine_1 : ∀ (y : (↑B : Type u)),
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry)) :
      X')
    ((((g : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry)) :
      X')
Tactic: ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
refine_1 :
  ∀ (y : (↑B : Type u)),
    Eq (α := X')
      ((((h : (a : (↑B : Type u)) → SX')
                ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) f :
                      (a : (↑A : Type u)) → (↑B : Type u))
                    a :
                  (↑B : Type u)) :
              SX') :
            (a : X') → X')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) :
        X')
      ((((g : (a : (↑B : Type u)) → SX')
                ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) f :
                      (a : (↑A : Type u)) → (↑B : Type u))
                    a :
                  (↑B : Type u)) :
              SX') :
            (a : X') → X')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) :
        X')
⊢ Eq (α := SX')
    ((h : (a : (↑B : Type u)) → SX')
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      SX')
    ((g : (a : (↑B : Type u)) → SX')
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      SX')
have refine_1₁ : Eq (α := X')
  ((((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      ∞ :
    X')
  ((((g : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      ∞ :
    X')
Tactic: ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
⊢ (((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑B : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
                (a : (↑A : Type u)) → (↑B : Type u))
              a :
            (↑B : Type u))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)
have pos : ∀ (m : y ∈ (Hom.hom f).range),
  (((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑B : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
                (a : (↑A : Type u)) → (↑B : Type u))
              a :
            (↑B : Type u))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry) :
            Set (↑B : Type u)))
        sorry)
Tactic: by_cases m : y ∈ f.hom.range
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∈ (Hom.hom f).range
⊢ (((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑B : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
                (a : (↑A : Type u)) → (↑B : Type u))
              a :
            (↑B : Type u))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)
have pos : 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)) sorry) =
  fromCoset
    (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
      (HSMul.hSMul (α := (↑B : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u))
        (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry) :
          Set (↑B : Type u)))
      sorry)
Tactic: rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∉ (Hom.hom f).range
⊢ (((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑B : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
                (a : (↑A : Type u)) → (↑B : Type u))
              a :
            (↑B : Type u))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)
have neg : fromCoset
    (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
      (HMul.hMul (α := (↑B : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
                (a : (↑A : Type u)) → (↑B : Type u))
              a :
            (↑B : Type u))
          y •
        (↑(Hom.hom f).range : Set (↑B : Type u)))
      sorry) =
  fromCoset
    (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
      (HSMul.hSMul (α := (↑B : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u))
        (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) sorry) :
          Set (↑B : Type u)))
      sorry)
Tactic: rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
⊢ Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        ∞ :
      X')
    ((((g : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        ∞ :
      X')
have refine_1 : Eq (α := X')
  ((((h : (a : (↑B : Type u)) → SX')
            ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    f :
                  (a : (↑A : Type u)) → (↑B : Type u))
                a :
              (↑B : Type u)) :
          SX') :
        (a : X') → X')
      ∞ :
    X')
  (∞ : X')
Tactic: rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
refine_1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        ∞ :
      X')
    (∞ : X')
⊢ Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        ∞ :
      X')
    ((((g : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        ∞ :
      X')
have refine_1₁ : Eq.{u + 1} (α := X') ∞ ∞
Tactic: rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]