R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
⊢ ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
⊢ Function.Injective ↑(of G (fun i j h => ↑(f' i j h)) i)
suffices ∀ x, of G (fun i j h => f' i j h) i x = 0 → x = 0 by
  intro x y hxy
  rw [← sub_eq_zero]
  apply this
  rw [(of G _ i).map_sub, hxy, sub_self]
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
⊢ x = 0
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
⊢ ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
intro x hx
case intro.intro
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
j : ι
hij : i ≤ j
hfx : ↑(f' i j hij) x = 0
⊢ x = 0
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
⊢ x = 0
rcases of.zero_exact hx with ⟨j, hij, hfx⟩
case intro.intro.a
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
j : ι
hij : i ≤ j
hfx : ↑(f' i j hij) x = 0
⊢ ↑(f' i j hij) x = ↑(f' i j hij) 0
case intro.intro
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
j : ι
hij : i ≤ j
hfx : ↑(f' i j hij) x = 0
⊢ x = 0
apply hf i j hij
no goals
case intro.intro.a
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
x : G i
hx : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
j : ι
hij : i ≤ j
hfx : ↑(f' i j hij) x = 0
⊢ ↑(f' i j hij) x = ↑(f' i j hij) 0
rw [hfx, (f' i j hij).map_zero]
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ x = y
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
⊢ Function.Injective ↑(of G (fun i j h => ↑(f' i j h)) i)
intro x y hxy
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ x - y = 0
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ x = y
rw [← sub_eq_zero]
case a
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ ↑(of G (fun i j h => ↑(f' i j h)) i) (x - y) = 0
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ x - y = 0
apply this
no goals
case a
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : DirectedSystem G fun i j h => ↑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ↑(f' i j hij)
i : ι
this : ∀ (x : G i), ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0 → x = 0
x y : G i
hxy : ↑(of G (fun i j h => ↑(f' i j h)) i) x = ↑(of G (fun i j h => ↑(f' i j h)) i) y
⊢ ↑(of G (fun i j h => ↑(f' i j h)) i) (x - y) = 0
rw [(of G _ i).map_sub, hxy, sub_self]