awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
rw :
  Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 : MvPolynomial τ R) ↔
    p = 0
rw₁ rw₂ : p = 0 ↔ p = 0
⊢ Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (0 : MvPolynomial τ R) ↔
    p = 0

Tactic:
rw [← rename_zero f, (MvPolynomial.rename_injective _ hf).eq_iff]

Premises used: Function.Injective.eq_iff, MvPolynomial.rename_zero, MvPolynomial.rename_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → σ
hf : LeftInverse f g
x : MvPolynomial τ R
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((rename g : (a : MvPolynomial τ R) → MvPolynomial σ R) x) = x

Tactic:
simp [hf.comp_eq_id]

Premises used: Function.LeftInverse.comp_eq_id
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → σ
hf : RightInverse f g
⊢ RightInverse (α := MvPolynomial τ R) (β := MvPolynomial σ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (⇑(rename g) : (a : MvPolynomial τ R) → MvPolynomial σ R)

Tactic:
rename_leftInverse hf

Premises used: Function.RightInverse, MvPolynomial.rename_leftInverse
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Surjective f
⊢ Surjective (α := MvPolynomial σ R) (β := MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)

Tactic:
let ⟨_, hf⟩ := hf.hasRightInverse; rename_rightInverse hf |>.surjective

Premises used: Function.Surjective.hasRightInverse, MvPolynomial.rename, MvPolynomial.rename_rightInverse, Function.RightInverse.surjective, DFunLike.coe, Function.Surjective, _private.0.MvPolynomial.rename_surjective.match_1
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial τ R) r) : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
algHom_C _ _

Premises used: MvPolynomial.algHom_C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
dsimp :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((AlgHom.comp (killCompl hf) (rename f) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)

Tactic:
dsimp
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((X ∘ f) i) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        (X (f i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₄ :
  Eq (α := MvPolynomial σ R)
    (if h : f i ∈ range f then
      X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) h))
    else 0)
    (X i)
rw₅ :
  Eq (α := MvPolynomial σ R)
    (X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) ⋯)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₆ rw₇ : Eq (α := MvPolynomial σ R) (X i) (X i)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)

Tactic:
rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]

Premises used: MvPolynomial.killCompl, MvPolynomial.aeval_X, dif_pos, Equiv.ofInjective_symm_apply, MvPolynomial.rename, Function.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial σ R
⊢ (killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p

Tactic:
AlgHom.congr_fun (killCompl_comp_rename hf) p

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.killCompl_comp_rename, Finsupp.sum, MvPolynomial.eval₂, AlgHom.congr_fun, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
simp :
  Eq (α := MvPolynomial σ S)
    ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)
    ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((killCompl hf : (a : MvPolynomial τ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial τ R) → MvPolynomial τ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)

Tactic:
simp only [← AlgHom.coe_toRingHom, ← RingHom.comp_apply]

Premises used: AlgHom.coe_toRingHom, RingHom.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
e_a :
  RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) =
    RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ S)
    ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)
    ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
e_a :
  ∀ (i : R) (n : σ →₀ ℕ),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ)) C :
            (a : R) → MvPolynomial σ S)
          i))
      (coeff n
        ((RingHom.comp (RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)) C :
            (a : R) → MvPolynomial σ S)
          i))
e_a₁ :
  ∀ (i : τ) (n : σ →₀ ℕ),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
      (coeff n
        ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
⊢ RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) =
    RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)

Tactic:
ext i n
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : R
n : σ →₀ ℕ
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ)) C :
          (a : R) → MvPolynomial σ S)
        i))
    (coeff n
      ((RingHom.comp (RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)) C :
          (a : R) → MvPolynomial σ S)
        i))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
pos :
  ∀ (h : i ∈ range f),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
      (coeff n
        ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
neg :
  ∀ (h : i ∉ range f),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
      (coeff n
        ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))

Tactic:
by_cases h : i ∈ Set.range f

Premises used: Set.range
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
h : i ∈ range f
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))

Tactic:
simp [killCompl, h]

Premises used: MvPolynomial.killCompl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
h : i ∉ range f
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))

Tactic:
simp [killCompl, h]

Premises used: MvPolynomial.killCompl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : σ →₀ ℕ
c : R
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((monomial (Finsupp.mapDomain f s) : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial s : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)

Tactic:
simp [← rename_monomial]

Premises used: MvPolynomial.rename_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      (∏ a ∈ s.support,
          HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
            (if h : a ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
            else 0)
            ((s : (a : τ) → ℕ) a : ℕ) :
        MvPolynomial σ R) =
    0
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
rw [killCompl, aeval_monomial, Finsupp.prod]

Premises used: MvPolynomial.killCompl, MvPolynomial.aeval_monomial, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
h :
  Eq (α := MvPolynomial σ R)
    (∏ a ∈ s.support,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
        (if h : a ∈ range f then
          X
            (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
              (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
        else 0)
        ((s : (a : τ) → ℕ) a : ℕ))
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      (∏ a ∈ s.support,
          HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
            (if h : a ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
            else 0)
            ((s : (a : τ) → ℕ) a : ℕ) :
        MvPolynomial σ R) =
    0

Tactic:
apply mul_eq_zero_of_right

Premises used: mul_eq_zero_of_right
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
h :
  HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
      (if h : a ∈ range f then
        X
          (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
            (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
      else 0)
      ((s : (a : τ) → ℕ) a : ℕ) =
    0
⊢ Eq (α := MvPolynomial σ R)
    (∏ a ∈ s.support,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
        (if h : a ∈ range f then
          X
            (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
              (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
        else 0)
        ((s : (a : τ) → ℕ) a : ℕ))
    0

Tactic:
apply Finset.prod_eq_zero ha

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
      (if h : a ∈ range f then
        X
          (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
            (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
      else 0)
      ((s : (a : τ) → ℕ) a : ℕ) =
    0

Tactic:
simp [hs, zero_pow (Finsupp.mem_support_iff.mp ha)]

Premises used: Finsupp.mem_support_iff, Iff.mp, zero_pow
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ¬(↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
have ⟨_, ha, hs⟩ := Set.not_subset.mp hs
  killCompl_monomial_eq_zero_of_notMem_range hf c ha hs

Premises used: MvPolynomial.killCompl, MvPolynomial.monomial, _private.0.MvPolynomial.killCompl_monomial_eq_zero_of_not_subset.match_1, Set.not_subset, Iff.mp, OfNat.ofNat, Eq, DFunLike.coe, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : (↑s.support : Set τ) ⊆ range f
nth_rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((monomial (Finsupp.mapDomain f (Finsupp.comapDomain f s ⋯)) : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
nth_rw₁ nth_rw₂ :
  Eq (α := MvPolynomial σ R) ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)

Tactic:
nth_rw 1 [← s.mapDomain_comapDomain f hf hs, killCompl_monomial_mapDomain]

Premises used: Finsupp.mapDomain_comapDomain, MvPolynomial.killCompl_monomial_mapDomain
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
pos :
  ∀ (h : (↑s.support : Set τ) ⊆ range f),
    Eq (α := MvPolynomial σ R)
      ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
        MvPolynomial σ R)
      ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
neg :
  ∀ (h : ¬(↑s.support : Set τ) ⊆ range f),
    Eq (α := MvPolynomial σ R)
      ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (if (↑s.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c
      else 0 :
      MvPolynomial σ R)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
h : (↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)

Tactic:
killCompl_monomial_eq_monomial_comapDomain_of_subset hf c h

Premises used: MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
h : (↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)

Tactic:
exact killCompl_monomial_eq_monomial_comapDomain_of_subset hf c h

Premises used: MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
h : ¬(↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
killCompl_monomial_eq_zero_of_not_subset hf c h

Premises used: MvPolynomial.killCompl_monomial_eq_zero_of_not_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
h : ¬(↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
exact killCompl_monomial_eq_zero_of_not_subset hf c h

Premises used: MvPolynomial.killCompl_monomial_eq_zero_of_not_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
monomial :
  ∀ (u : τ →₀ ℕ) (a : R),
    Eq.{u_4 + 1} (α := R)
      (coeff s
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a)))
      (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a))
add :
  ∀ (p q : MvPolynomial τ R),
    coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p →
      coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) q) = coeff (Finsupp.mapDomain f s) q →
        coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) (p + q)) =
          coeff (Finsupp.mapDomain f s) (p + q)
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p

Tactic:
apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))

Premises used: MvPolynomial.induction_on'