awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
this : a'.hom ≫ g = 0
⊢ 𝟙 R ≫ (app g (Over.mk a'')).hom = p ≫ (app g a).hom

Tactic:
simp [a'', sub_eq_add_neg, this]

Premises used: sub_eq_add_neg
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
this : a'.hom ≫ g = 0
⊢ app g (Over.mk a'') ≈ app g a

Tactic:
exact ⟨R, 𝟙 R, p, inferInstance, ep, by simp [a'', sub_eq_add_neg, this]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
obtain :
  ∀ (Z : C)
    (a :
      Z ⟶
        Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
          ((fun (g : Over.{v, u} P) ↦ app f g) x))
    (b :
      Z ⟶
        Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
          ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y))
    (ea : Epi a) (eb : Epi b)
    (comm :
      a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)),
    ∃ (s : Pseudoelement.{v, u} (pullback f g)),
      pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
⊢ ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h

Premises used: comm, Quotient.exact
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
simp : a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g

Tactic:
comm

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g

Tactic:
exact comm
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
obtain :
  ∀ (l : Z ⟶ pullback f g) (hl₁ : l ≫ pullback.fst f g = a ≫ x.hom) (hl₂ : l ≫ pullback.snd f g = b ≫ y.hom),
    ∃ (s : Pseudoelement.{v, u} (pullback f g)),
      pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
⊢ ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
      simp only [Category.assoc]
      exact comm)

Premises used: CategoryTheory.Limits.pullback.lift', CategoryTheory.CategoryStruct.comp, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
rwa rwa₁ rwa₂ rwa₃ :
  Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.fst f g) g_1) (Over.mk l)) = a ≫ x.hom
⊢ 𝟙 Z ≫ Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.fst f g) g_1) (Over.mk l)) = a ≫ x.hom

Tactic:
rwa [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
rwa rwa₁ rwa₂ rwa₃ :
  Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.snd f g) g_1) (Over.mk l)) = b ≫ y.hom
⊢ 𝟙 Z ≫ Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.snd f g) g_1) (Over.mk l)) = b ≫ y.hom

Tactic:
rwa [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
exact ⟨l, ⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
      Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
h : PseudoEqual G x y
obtain :
  ∀ (P : ModuleCat.{u_2, u_1} R) (p : P ⟶ x.left) (q : P ⟶ y.left) (hp : Epi p) (hq : Epi q)
    (H : p ≫ x.hom = q ≫ y.hom), (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨P, p, q, hp, hq, H⟩ := h
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Premises used: Iff.intro, Submodule.ext
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
refine_1 : ∀ (a : (↑G : Type u_2)) (ha : a ∈ (ModuleCat.Hom.hom x.hom).range), a ∈ (ModuleCat.Hom.hom y.hom).range
refine_2 : ∀ (a : (↑G : Type u_2)) (ha : a ∈ (ModuleCat.Hom.hom y.hom).range), a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Premises used: Iff.intro, Submodule.ext
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
ha : a ∈ (ModuleCat.Hom.hom x.hom).range
refine_1 :
  ∀ (a' : (↑x.left : Type u_2)) (ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a),
    a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑x.left : Type u_2)
ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
refine_1 :
  ∀ (a'' : (↑P : Type u_2))
    (ha'' :
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) p :
            (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
          a'' =
        a'),
    a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'

Premises used: ModuleCat.epi_iff_surjective, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑x.left : Type u_2)
ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) p :
        (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
      a'' =
    a'
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
⟨q a'', ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑x.left : Type u_2)
ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) p :
        (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
      a'' =
    a'
refine_1 :
  (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) q :
            (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
          a'' :
        (↑y.left : Type u_2)) =
    a
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
refine ⟨q a'', ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑x.left : Type u_2)
ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) p :
        (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
      a'' =
    a'
refine_1 :
  (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) q :
            (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
          a'' :
        (↑y.left : Type u_2)) =
    a
⊢ (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) q :
            (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
          a'' :
        (↑y.left : Type u_2)) =
    a

Tactic:
dsimp at ha' ⊢
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑x.left : Type u_2)
ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) p :
        (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
      a'' =
    a'
refine_1 :
  (ModuleCat.Hom.hom y.hom ∘ₗ
          ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
            (CC := ModuleCat.carrier) q :
        (a : (↑P : Type u_2)) → (↑G : Type u_2))
      a'' =
    a
refine_1₁ : (ModuleCat.Hom.hom (q ≫ y.hom) : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_1₂ : (ModuleCat.Hom.hom (p ≫ x.hom) : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_1₃ : (ModuleCat.Hom.hom x.hom ∘ₗ ModuleCat.Hom.hom p : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_1₄ :
  (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2))
      ((ModuleCat.Hom.hom p : (a : (↑P : Type u_2)) → (↑x.left : Type u_2)) a'' : (↑x.left : Type u_2)) =
    a
refine_1₅ : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a
refine_1₆ refine_1₇ : a = a
⊢ (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) q :
            (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
          a'' :
        (↑y.left : Type u_2)) =
    a

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← H,
      ModuleCat.hom_comp, LinearMap.comp_apply, ha'', ha']

Premises used: LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
ha : a ∈ (ModuleCat.Hom.hom y.hom).range
refine_2 :
  ∀ (a' : (↑y.left : Type u_2)) (ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a),
    a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑y.left : Type u_2)
ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
refine_2 :
  ∀ (a'' : (↑P : Type u_2))
    (ha'' :
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) q :
            (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
          a'' =
        a'),
    a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'

Premises used: ModuleCat.epi_iff_surjective, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑y.left : Type u_2)
ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) q :
        (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
      a'' =
    a'
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
⟨p a'', ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑y.left : Type u_2)
ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) q :
        (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
      a'' =
    a'
refine_2 :
  (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) p :
            (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
          a'' :
        (↑x.left : Type u_2)) =
    a
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
refine ⟨p a'', ?_⟩