R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) p = ↑(RingHom.id (MvPolynomial σ R)) p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ↑(rename f) (↑(aeval fun i => Option.elim' 0 X (partialInv f i)) p) = p
show (rename f).toRingHom.comp _ p = RingHom.id _ p
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C =
    RingHom.comp (RingHom.id (MvPolynomial σ R)) C

case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ∀ (i : σ),
    i ∈ vars p →
      i ∈ vars p →
        ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
          ↑(RingHom.id (MvPolynomial σ R)) (X i)

case refine'_3
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ p = p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) p = ↑(RingHom.id (MvPolynomial σ R)) p
refine' hom_congr_vars _ _ _
case refine'_1.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C) x✝ =
    ↑(RingHom.comp (RingHom.id (MvPolynomial σ R)) C) x✝
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C =
    RingHom.comp (RingHom.id (MvPolynomial σ R)) C
ext1
no goals
case refine'_1.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C) x✝ =
    ↑(RingHom.comp (RingHom.id (MvPolynomial σ R)) C) x✝
simp [algebraMap_eq]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : σ
hip a✝ : i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
    ↑(RingHom.id (MvPolynomial σ R)) (X i)
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ∀ (i : σ),
    i ∈ vars p →
      i ∈ vars p →
        ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
          ↑(RingHom.id (MvPolynomial σ R)) (X i)
intro i hip _
case refine'_2.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : τ
hip a✝ : f i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X (f i)) =
    ↑(RingHom.id (MvPolynomial σ R)) (X (f i))
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : σ
hip a✝ : i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
    ↑(RingHom.id (MvPolynomial σ R)) (X i)
rcases hf hip with ⟨i, rfl⟩
no goals
case refine'_2.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : τ
hip a✝ : f i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X (f i)) =
    ↑(RingHom.id (MvPolynomial σ R)) (X (f i))
simp [partialInv_left hfi]
no goals
case refine'_3
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ p = p
rfl