-- Mathlib/Algebra/Colimit/Ring.lean
theorem Polynomial.exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)]
    (q : Polynomial (DirectLimit G fun i j h ↦ f' i j h)) :
    ∃ i p, Polynomial.map (of G (fun i j h ↦ f' i j h) i) p = q :=
  Polynomial.induction_on q
    (fun z ↦
      let ⟨i, x, h⟩ := exists_of z
      ⟨i, C x, by rw [map_C, h]⟩)
    (fun q₁ q₂ ⟨i₁, p₁, ih₁⟩ ⟨i₂, p₂, ih₂⟩ ↦
      let ⟨i, h1, h2⟩ := exists_ge_ge i₁ i₂
      ⟨i, p₁.map (f' i₁ i h1) + p₂.map (f' i₂ i h2), by
        rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]
        congr 2 <;> ext x <;> simp_rw [RingHom.comp_apply, of_f]⟩)
    fun n z _ ↦
    let ⟨i, x, h⟩ := exists_of z
    ⟨i, C x * X ^ (n + 1), by rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]⟩

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂

Tactic:
congr 2 <;> ext x <;> simp_rw [RingHom.comp_apply, of_f]

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h => ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h => ⇑(f' i j h)) i) x = z
⊢ Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (C x * X ^ (n + 1)) = C z * X ^ (n + 1)

Tactic:
rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (Polynomial.map (f' i₁ i h1) p₁ + Polynomial.map (f' i₂ i h2) p₂) =
    q₁ + q₂

Tactic:
rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]

Result:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]
z : DirectLimit G fun i j h => ⇑(f' i j h)
i : ι
x : G i
h : (of G (fun i j h => ⇑(f' i j h)) i) x = z
⊢ Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (C x) = C z

Tactic:
rw [map_C, h]

Result:
no goals