no goals
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
z : DirectLimit G f
⊢ Nonempty ι
infer_instance
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
z✝ : DirectLimit G f
ind : ι
z p q : ⨁ (i : ι), G i
x✝¹ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : ↑(of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : ↑(of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
z✝ : DirectLimit G f
ind : ι
z p q : ⨁ (i : ι), G i
x✝¹ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : ↑(of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : ↑(of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ ↑(of R ι G f k) (↑(f i k hik) x + ↑(f j k hjk) y) = Quotient.mk'' (p + q)
rw [LinearMap.map_add, of_f, of_f, ihx, ihy]
no goals
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
z✝ : DirectLimit G f
ind : ι
z p q : ⨁ (i : ι), G i
x✝¹ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, ↑(of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : ↑(of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : ↑(of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)
simp only [Submodule.Quotient.mk''_eq_mk, Quotient.mk_add]