-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem exists_rename_eq_of_vars_subset_range (p : MvPolynomial σ R) (f : τ → σ) (hfi : Injective f)
    (hf : ↑p.vars ⊆ Set.range f) : ∃ q : MvPolynomial τ R, rename f q = p :=
  ⟨aeval (fun i : σ => Option.elim' 0 X <| partialInv f i) p,
    by
      show (rename f).toRingHom.comp _ p = RingHom.id _ p
      refine hom_congr_vars ?_ ?_ ?_
      · ext1
        simp [algebraMap_eq]
      · intro i hip _
        rcases hf hip with ⟨i, rfl⟩
        simp [partialInv_left hfi]
      · rfl⟩

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ (rename f) ((aeval fun i => Option.elim' 0 X (partialInv f i)) p) = p

Tactic:
show (rename f).toRingHom.comp _ p = RingHom.id _ p

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) p = (RingHom.id (MvPolynomial σ R)) p

Proof state:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

Tactic:
intro i hip _

Result:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : σ
hip a✝ : i ∈ p.vars
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
    (RingHom.id (MvPolynomial σ R)) (X i)

Proof state:
case refine_2.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : τ
hip a✝ : f i ∈ p.vars
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X (f i)) =
    (RingHom.id (MvPolynomial σ R)) (X (f i))

Tactic:
simp [partialInv_left hfi]

Result:
no goals

Proof state:
case refine_1.a
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
x✝ : R
⊢ (((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom).comp C) x✝ =
    ((RingHom.id (MvPolynomial σ R)).comp C) x✝

Tactic:
simp [algebraMap_eq]

Result:
no goals

Proof state:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : σ
hip a✝ : i ∈ p.vars
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
    (RingHom.id (MvPolynomial σ R)) (X i)

Tactic:
rcases hf hip with ⟨i, rfl⟩

Result:
case refine_2.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : τ
hip a✝ : f i ∈ p.vars
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X (f i)) =
    (RingHom.id (MvPolynomial σ R)) (X (f i))

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) p = (RingHom.id (MvPolynomial σ R)) p

Tactic:
refine hom_congr_vars ?_ ?_ ?_

Result:
case refine_1
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom).comp C =
    (RingHom.id (MvPolynomial σ R)).comp C

case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Proof state:
case refine_1
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom).comp C =
    (RingHom.id (MvPolynomial σ R)).comp C

Tactic:
ext1

Result:
case refine_1.a
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
x✝ : R
⊢ (((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom).comp C) x✝ =
    ((RingHom.id (MvPolynomial σ R)).comp C) x✝

Proof state:
case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
rfl

Result:
no goals