no goals
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : ↑(Ring.DirectLimit.of G f i) x ≠ 0
⊢ ↑(Ring.DirectLimit.of G f i) x * ↑(Ring.DirectLimit.of G f i) x⁻¹ = 1
erw [← (Ring.DirectLimit.of _ _ _).map_mul,
  mul_inv_cancel fun h : x = 0 => H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
  (Ring.DirectLimit.of _ _ _).map_one]
no goals
R : Type u
inst✝⁴ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : ↑(Ring.DirectLimit.of G f i) x ≠ 0
h : x = 0
⊢ ↑(Ring.DirectLimit.of G f i) x = 0
rw [h, (Ring.DirectLimit.of _ _ _).map_zero]