awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i_1 : F
hi_1 : i_1 ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
i : F
hi : i ∈ s
simp_rw :
  m i •
      ((∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) *
        (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
    HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
simp_rw₁ :
  m i •
      ((∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) *
          HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E) *
        (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
    HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
⊢ m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
    HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))

Tactic:
simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]

Premises used: Finset.prod_erase_mul, mul_inv_cancel_right₀
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
⊢ ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))

Tactic:
have h1 : ∀ i ∈ s, m i • (b * (x - algebraMap F E i)⁻¹) =
      m i • (s.erase i).prod fun j ↦ x - algebraMap F E j := fun i hi ↦ by
    simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
⊢ b * ∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹ = b * 0

Tactic:
replace hm := congr(b * $(hm))
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
hm : b * ∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹ = b * 0
⊢ Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
    0

Tactic:
simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] at hm

Premises used: Finset.mul_sum, MulZeroClass.mul_zero, mul_smul_comm, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
hm :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
    0
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
⊢ Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)

Tactic:
replace hm := congr(Polynomial.aeval i $(H p (by simp_rw [← hm, p, map_sum, map_mul, map_prod,
    map_sub, aeval_X, aeval_C, Algebra.smul_def])))
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
j : F
hj : j ∈ s.erase i
⊢ i ∈ s.erase j

Tactic:
have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
j : F
hj : j ∈ s.erase i
this : i ∈ s.erase j
simp_rw : m j * ((∏ x ∈ (s.erase j).erase i, (i - x)) * (i - i)) = 0
simp_rw₁ : m j * HMul.hMul (α := F) (∏ x ∈ (s.erase j).erase i, (i - x)) 0 = 0
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]

Premises used: Finset.prod_erase_mul, sub_self, MulZeroClass.mul_zero, Finset.erase
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
⊢ ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
have h2 : ∀ j ∈ s.erase i, m j * ((s.erase j).prod fun x ↦ i - x) = 0 := fun j hj ↦ by
    have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
    simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
⊢ m i * ∏ x ∈ s.erase i, (i - x) = 0

Tactic:
simp_rw [map_zero, p, map_sum, map_mul, map_prod, map_sub, aeval_X,
    aeval_C, Algebra.algebraMap_self_apply, ← s.sum_erase_add _ hi,
    Finset.sum_eq_zero h2, zero_add] at hm

Premises used: Algebra.algebraMap_self_apply, map_sub, Finset.sum_eq_zero, map_zero, map_sum, zero_add, map_prod, map_mul, Finset.sum_erase_add, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : m i * ∏ x ∈ s.erase i, (i - x) = 0
⊢ m i = 0

Tactic:
eq_zero_of_ne_zero_of_mul_right_eq_zero (Finset.prod_ne_zero_iff.2 fun j hj ↦
    sub_ne_zero.2 (Finset.ne_of_mem_erase hj).symm) hm

Premises used: Iff.mpr, sub_ne_zero, Finset.ne_of_mem_erase, Ne.symm, Finset.prod_ne_zero_iff, eq_zero_of_ne_zero_of_mul_right_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : m i * ∏ x ∈ s.erase i, (i - x) = 0
⊢ m i = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (Finset.prod_ne_zero_iff.2 fun j hj ↦
    sub_ne_zero.2 (Finset.ne_of_mem_erase hj).symm) hm

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, eq_zero_of_ne_zero_of_mul_right_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
rw :
  ∀ (hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
rw [transcendental_iff_injective] at hf ⊢

Premises used: transcendental_iff_injective
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
⊢ Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])

Tactic:
replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
hf :
  Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
apply :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
      (⇑(optionEquivRight R (↑s : Type u_1)) :
        (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
      (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
        (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R))
⊢ Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (Function.comp (β := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
      (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
      (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
        (⇑(optionEquivRight R (↑s : Type u_1)) :
          (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
        (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
          (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R)))

Tactic:
apply hf.comp

Premises used: Function.Injective.comp
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
hf :
  Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
⊢ Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
      (⇑(optionEquivRight R (↑s : Type u_1)) :
        (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
      (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
        (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R))

Tactic:
simp only [EquivLike.comp_injective, EquivLike.injective]

Premises used: EquivLike.comp_injective, EquivLike.injective
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
hf :
  Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
⊢ Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)

Tactic:
replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
hX :
  Eq (α := MvPolynomial σ R) ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) Polynomial.X : MvPolynomial σ R)
    ((AlgHom.comp
            (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
              (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
                MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
            (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))) :
          (a : R[X]) → MvPolynomial σ R)
        Polynomial.X :
      MvPolynomial σ R)
⊢ Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
    (AlgHom.comp
      (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
        (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
          MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
      (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))

Tactic:
ext1