case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) (↑φ 0)

case inr
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
rcases eq_or_ne q 0 with (rfl | hq)
no goals
case inr
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
exact map_apply_div_ne_zero _ _ _ _ hq
case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) (↑φ 0)
case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) (↑φ 0)
have : (0 : RatFunc K) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) 0 / ↑(algebraMap ((fun x => R[X]) 1) (RatFunc R)) 1 = 0

case inl.hq
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ 1 ≠ 0
case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) (↑φ 0)
rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one,
  map_one, div_one, map_zero, map_zero]
case inl.hq
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ 1 ≠ 0
case inl
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ ↑(algebraMap ((fun x => R[X]) 0) (RatFunc R)) 0 / ↑(algebraMap ((fun x => R[X]) 1) (RatFunc R)) 1 = 0

case inl.hq
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ 1 ≠ 0
simp only [map_zero, map_one, div_one]
no goals
case inl.hq
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
⊢ 1 ≠ 0
exact one_ne_zero
no goals
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ 0 = ↑(algebraMap K[X] (RatFunc K)) 0 / ↑(algebraMap K[X] (RatFunc K)) 1
simp