case intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 x.hom = LinearMap.range y.hom
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ LinearMap.range x.hom = LinearMap.range y.hom
obtain ⟨P, p, q, hp, hq, H⟩ := h
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 x.hom
⊢ a ∈ LinearMap.range y.hom

case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 y.hom
⊢ a ∈ LinearMap.range x.hom
case intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 x.hom = LinearMap.range y.hom
refine' Submodule.ext fun a => ⟨fun ha => _, fun ha => _⟩
case intro.intro.intro.intro.intro.refine'_1.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
⊢ a ∈ LinearMap.range y.hom
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 x.hom
⊢ a ∈ LinearMap.range y.hom
obtain ⟨a', ha'⟩ := ha
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ a ∈ LinearMap.range y.hom
case intro.intro.intro.intro.intro.refine'_1.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
⊢ a ∈ LinearMap.range y.hom
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ ↑y.hom (↑q a'') = a
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ a ∈ LinearMap.range y.hom
refine' ⟨q a'', _⟩
no goals
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ ↑y.hom (↑q a'') = a
rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, ← H, ModuleCat.comp_def, LinearMap.comp_apply,
  ha'', ha']
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
⊢ a ∈ LinearMap.range x.hom
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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 y.hom
⊢ a ∈ LinearMap.range x.hom
obtain ⟨a', ha'⟩ := ha
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ a ∈ LinearMap.range x.hom
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
⊢ a ∈ LinearMap.range x.hom
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ ↑x.hom (↑p a'') = a
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ a ∈ LinearMap.range x.hom
refine' ⟨p a'', _⟩
no goals
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
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' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ ↑x.hom (↑p a'') = a
rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, H, ModuleCat.comp_def, LinearMap.comp_apply,
  ha'', ha']