awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (hypothesis)
Goal:
A B : GrpCat
f : A ⟶ B
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
have eq1 : Eq (α := X')
  ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    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)) sorry) :
    X')
Tactic: have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
        fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
      change ((τ).symm.trans (g b)).trans τ _ = _
      dsimp [tau]
      simp [g_apply_infinity f]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (hypothesis)
Goal:
A B : GrpCat
f : A ⟶ B
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))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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')
⊢ False
have eq2 : Eq (α := X')
  ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    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')
Tactic: have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
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))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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')
eq2 :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
⊢ 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)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
have rw : Eq (α := X')
  ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    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')
Tactic: rw [← eq1, ← eq2, DFunLike.congr_fun hb]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
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))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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')
eq2 :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
rw :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
⊢ 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)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
have rw₁ : Eq (α := X')
  ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    X')
  ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    X')
Tactic: rw [← eq1, ← eq2, DFunLike.congr_fun hb]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
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))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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')
eq2 :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
rw :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
rw₁ :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : SX') : (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')
    ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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')
⊢ 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)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
have rw₂ : Eq (α := X')
  ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    X')
  ((((g : (a : (↑B : Type u)) → SX') b : SX') : (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)) sorry)) :
    X')
Tactic: rw [← eq1, ← eq2, DFunLike.congr_fun hb]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
⊢ f ≫ ofHom g = f ≫ ofHom h
have hf : ∀ (a : (↑A : Type u)) (x : X'),
  Eq (α := X')
    ((((Hom.hom (f ≫ ofHom g) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')
    ((((Hom.hom (f ≫ ofHom h) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
⊢ Eq (α := X')
    ((((Hom.hom (f ≫ ofHom g) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')
    ((((Hom.hom (f ≫ ofHom h) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')
have hf : Eq (α := X')
  ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
        (a : X') → X')
      x :
    X')
  ((((h : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
        (a : X') → X')
      x :
    X')
Tactic: simp only [hom_comp, hom_ofHom, MonoidHom.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
⊢ Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {b : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : 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))
have rw : Membership.mem (α := (↑B : Type u)) (↑(Hom.hom f).range : Set (↑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))
Tactic: rw [← agree]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
w : (↑A : Type u)
⊢ Membership.mem (α := (↑B : Type u)) (↑(Hom.hom f).range : Set (↑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))
have h : Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑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))
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (hypothesis)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
⊢ Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
    ((((h : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
have this : Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
  {b : (↑B : Type u) |
    Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : 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))
Tactic: have : f a ∈ { b | h b = g b } := by
    rw [← agree]
    use a
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
this :
  Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {b : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : 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))
⊢ Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
    ((((h : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
have hf : Eq (α := X')
  ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
        (a : X') → 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 :
    X')
Tactic: rw [this]
-- 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
r : g = h
⊢ False
have apply : Eq (α := X')
  (fromCoset
    (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X 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)
      (↑(Hom.hom f).range : Set (↑B : Type u)) sorry))
Tactic: apply fromCoset_ne_of_nin_range _ hx
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (hypothesis)
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∉ (Hom.hom f).range
r : g = h
⊢ Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X 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)) ⋯))
have r₁ : Eq (α := 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)
          (↑(Hom.hom f).range : Set (↑B : Type u)) sorry)) :
    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))) X x)
          (↑(Hom.hom f).range : Set (↑B : Type u)) sorry)) :
    X')
Tactic: replace r :=
    DFunLike.congr_fun (DFunLike.congr_fun r x) (fromCoset ⟨f.hom.range, ⟨1, one_leftCoset _⟩⟩)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
inst : Epi f
⊢ ∀ (b : (↑B : Type u)),
    ∃ (a : (↑A : 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
have by_contra! : ∀ (b : (↑B : Type u))
  (hb :
    ∀ (a : (↑A : 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),
  False
Tactic: by_contra! ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
have refine : Epi f → Epi (groupAddGroupEquivalence.inverse.map f)
Tactic: refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (hypothesis)
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
Tactic: have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) := by
    refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
    apply groupAddGroupEquivalence.inverse.map_epi
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : AddGrpCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
have rwa : ∀
  (i1 :
    Epi f ↔
      Function.Surjective (α := (↑(groupAddGroupEquivalence.inverse.obj A) : Type u)) (β :=
        (↑(groupAddGroupEquivalence.inverse.obj B) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              GrpCat.carrier) (groupAddGroupEquivalence.inverse.map f)) :
          (a : (↑(groupAddGroupEquivalence.inverse.obj A) : Type u)) →
            (↑(groupAddGroupEquivalence.inverse.obj B) : Type u))),
  Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
Tactic: rwa [GrpCat.epi_iff_surjective] at i1
Cleared hypotheses: i1
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f_1 : A ⟶ B
X Y : GrpCat
f : X ⟶ Y
e : Mono f
⊢ Mono (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
have rwa : ∀
  (e :
    Function.Injective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
  Mono (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
Tactic: rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f_1 : A ⟶ B
X Y : GrpCat
f : X ⟶ Y
e : Mono f
rwa :
  ∀
    (e :
      Function.Injective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
    Mono (X :=
      Functor.obj
        (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
⊢ Mono (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
have rwa₁ : ∀
  (e :
    Mono (X := (↑X : Type u_1)) (Y := (↑Y : Type u_1))
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1)))),
  Mono (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
Tactic: rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f_1 : A ⟶ B
X Y : GrpCat
f : X ⟶ Y
e : Epi f
⊢ Epi (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
have rwa : ∀
  (e :
    Function.Surjective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
  Epi (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
Tactic: rwa [epi_iff_surjective, ← CategoryTheory.ofHom_epi_iff_surjective] at e
Cleared hypotheses: e