-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem ModuleCat.eq_range_of_pseudoequal {R : Type*} [CommRing R] {G : ModuleCat R} {x y : Over G}
    (h : PseudoEqual G x y) : LinearMap.range x.hom.hom = LinearMap.range y.hom.hom

Proof state:
case intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

Tactic:
obtain ⟨a', ha'⟩ := ha

Result:
case intro.intro.intro.intro.intro.refine_1.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

Proof state:
case intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)

Tactic:
obtain ⟨a', ha'⟩ := ha

Result:
case intro.intro.intro.intro.intro.refine_2.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)

Proof state:
case intro.intro.intro.intro.intro.refine_2.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom) ((ConcreteCategory.hom p) a'') = a

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.refine_2.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)

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

Result:
case intro.intro.intro.intro.intro.refine_2.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom) ((ConcreteCategory.hom p) a'') = a

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

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

Result:
case intro.intro.intro.intro.intro.refine_1.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

Proof state:
case intro.intro.intro.intro.intro.refine_2.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)

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

Result:
case intro.intro.intro.intro.intro.refine_2.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

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

Result:
case intro.intro.intro.intro.intro.refine_1.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) ((ConcreteCategory.hom q) a'') = a

Proof state:
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ LinearMap.range (ModuleCat.Hom.hom x.hom) = LinearMap.range (ModuleCat.Hom.hom y.hom)

Tactic:
obtain ⟨P, p, q, hp, hq, H⟩ := h

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ LinearMap.range (ModuleCat.Hom.hom x.hom) = LinearMap.range (ModuleCat.Hom.hom y.hom)

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) ((ConcreteCategory.hom q) a'') = a

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

Result:
no goals