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✝¹ : DirectedSystem G fun i j h => ↑(f' i j h)
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
i : ι
x : G i
hix : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
this : Nonempty ι
j : ι
s : Set ((i : ι) × G i)
H : ∀ (k : (i : ι) × G i), k ∈ s → k.fst ≤ j
hxs : IsSupported (FreeCommRing.of { fst := i, snd := x }) s
hixs : { fst := i, snd := x } ∈ s
hx :
  ↑(f' (↑{ val := { fst := i, snd := x }, property := hixs }).fst j
          (_ : (↑{ val := { fst := i, snd := x }, property := hixs }).fst ≤ j))
      (↑{ val := { fst := i, snd := x }, property := hixs }).snd =
    0
⊢ ↑(f' i j (_ : { fst := i, snd := x }.fst ≤ j)) 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✝¹ : DirectedSystem G fun i j h => ↑(f' i j h)
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
i : ι
x : G i
hix : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
this : Nonempty ι
j : ι
s : Set ((i : ι) × G i)
H : ∀ (k : (i : ι) × G i), k ∈ s → k.fst ≤ j
hxs : IsSupported (FreeCommRing.of { fst := i, snd := x }) s
hx :
  ↑(↑lift fun ix => ↑(f' (↑ix).fst j (_ : (↑ix).fst ≤ j)) (↑ix).snd)
      (↑(restriction s) (FreeCommRing.of { fst := i, snd := x })) =
    0
hixs : { fst := i, snd := x } ∈ s
⊢ ↑(f' i j (_ : { fst := i, snd := x }.fst ≤ j)) x = 0
rw [restriction_of, dif_pos hixs, lift_of] at hx
no goals
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✝¹ : DirectedSystem G fun i j h => ↑(f' i j h)
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
i : ι
x : G i
hix : ↑(of G (fun i j h => ↑(f' i j h)) i) x = 0
this : Nonempty ι
j : ι
s : Set ((i : ι) × G i)
H : ∀ (k : (i : ι) × G i), k ∈ s → k.fst ≤ j
hxs : IsSupported (FreeCommRing.of { fst := i, snd := x }) s
hixs : { fst := i, snd := x } ∈ s
hx :
  ↑(f' (↑{ val := { fst := i, snd := x }, property := hixs }).fst j
          (_ : (↑{ val := { fst := i, snd := x }, property := hixs }).fst ≤ j))
      (↑{ val := { fst := i, snd := x }, property := hixs }).snd =
    0
⊢ ↑(f' i j (_ : { fst := i, snd := x }.fst ≤ j)) x = 0
exact hx