case refine'_1
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ degree (f %ₘ g) < degree g

case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ ∃ q r,
    degree r < degree g ∧
      ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
        ↑(algebraMap R[X] K) q + ↑(algebraMap R[X] K) r / ↑(algebraMap R[X] K) g
refine' ⟨f /ₘ g, f %ₘ g, _, _⟩
no goals
case refine'_1
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ degree (f %ₘ g) < degree g
exact degree_modByMonic_lt _ hg
case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
have hg' : algebraMap R[X] K g ≠ 0 :=
  (map_ne_zero_iff _ (IsFractionRing.injective R[X] K)).mpr (Monic.ne_zero hg)
case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f = ↑(algebraMap R[X] K) (f /ₘ g) * ↑(algebraMap R[X] K) g + ↑(algebraMap R[X] K) (f %ₘ g)
case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
field_simp [hg']
no goals
case refine'_2
R : Type u_1
G : Type ?u.275691
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f = ↑(algebraMap R[X] K) (f /ₘ g) * ↑(algebraMap R[X] K) g + ↑(algebraMap R[X] K) (f %ₘ g)
rw [add_comm, mul_comm, ← map_mul, ← map_add, modByMonic_add_div f hg]