awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
h :
  ∃ (q₁_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R) (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₁_1 :
          MvPolynomial σ R) ∧
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)
⊢ ∃ (s : Finset σ) (q₁_1 : MvPolynomial.{u_1, u_4} (↥s) R) (q₂_1 : MvPolynomial.{u_1, u_4} (↥s) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₁_1 :
          MvPolynomial σ R) ∧
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₂_1 :
          MvPolynomial σ R)

Tactic:
use s₁ ∪ s₂
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
h :
  ∃ (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
                (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
              q₁) :
          MvPolynomial σ R) ∧
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)
⊢ ∃ (q₁_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R) (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₁_1 :
          MvPolynomial σ R) ∧
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)

Tactic:
use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁

Premises used: MvPolynomial.rename, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
h :
  Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₁) :
        MvPolynomial σ R) ∧
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₂) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₂) :
        MvPolynomial σ R)
⊢ ∃ (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
                (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
              q₁) :
          MvPolynomial σ R) ∧
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)

Tactic:
use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂

Premises used: MvPolynomial.rename, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
h :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
        ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
            (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
          q₁) :
      MvPolynomial σ R)
h₁ :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
        ((rename fun (x : ↥s₂) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
            (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
          q₂) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₁) :
        MvPolynomial σ R) ∧
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₂) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₂) :
        MvPolynomial σ R)

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
⊢ Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
        ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
            (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
          q₁) :
      MvPolynomial σ R)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
⊢ Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
        ((rename fun (x : ↥s₂) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
            (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
          q₂) :
      MvPolynomial σ R)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
obtain :
  ∀ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q_1 : MvPolynomial (Fin n) R),
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
          MvPolynomial σ R)
        ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q_1 : MvPolynomial σ R)
⊢ ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q : MvPolynomial (Fin n) R),
    p = (rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q

Tactic:
obtain ⟨s, q, rfl⟩ := exists_finset_rename p

Premises used: MvPolynomial.exists_finset_rename, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset σ
q : MvPolynomial.{u_1, u_4} (↥s) R
n : ℕ := Fintype.card.{u_1} ↥s
e : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) := Fintype.equivFin ↥s
⊢ ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q_1 : MvPolynomial (Fin n) R),
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q_1 : MvPolynomial σ R)

Tactic:
⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩

Premises used: Function.comp, MvPolynomial.rename, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset σ
q : MvPolynomial.{u_1, u_4} (↥s) R
n : ℕ := Fintype.card.{u_1} ↥s
e : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) := Fintype.equivFin ↥s
refine :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
      MvPolynomial σ R)
    ((rename (comp (β := ↥s) (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) (⇑e.symm : (a : Fin (Fintype.card ↥s)) → ↥s)) :
          (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((rename (⇑e : (a : ↥s) → Fin (Fintype.card ↥s)) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (Fin (Fintype.card ↥s)) R)
          q) :
      MvPolynomial σ R)
⊢ ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q_1 : MvPolynomial (Fin n) R),
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q_1 : MvPolynomial σ R)

Tactic:
refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset σ
q : MvPolynomial.{u_1, u_4} (↥s) R
n : ℕ := Fintype.card.{u_1} ↥s
e : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) := Fintype.equivFin ↥s
rw :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        ((rename
              (comp (β := Fin (Fintype.card.{u_1} ↥s)) (⇑e.symm : (a : Fin (Fintype.card ↥s)) → ↥s)
                (⇑e : (a : ↥s) → Fin (Fintype.card ↥s))) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (↥s) R)
          q) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
      MvPolynomial σ R)
    ((rename (comp (β := ↥s) (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) (⇑e.symm : (a : Fin (Fintype.card ↥s)) → ↥s)) :
          (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((rename (⇑e : (a : ↥s) → Fin (Fintype.card ↥s)) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (Fin (Fintype.card ↥s)) R)
          q) :
      MvPolynomial σ R)

Tactic:
rw [← rename_rename, rename_rename e]

Premises used: MvPolynomial.rename_rename, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset σ
q : MvPolynomial.{u_1, u_4} (↥s) R
n : ℕ := Fintype.card.{u_1} ↥s
e : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) := Fintype.equivFin ↥s
⊢ Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        ((rename
              (comp (β := Fin (Fintype.card.{u_1} ↥s)) (⇑e.symm : (a : Fin (Fintype.card ↥s)) → ↥s)
                (⇑e : (a : ↥s) → Fin (Fintype.card ↥s))) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (↥s) R)
          q) :
      MvPolynomial σ R)

Tactic:
simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

Premises used: MvPolynomial.rename_rename, Equiv.symm_apply_apply, Function.comp_def
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
⊢ eval₂ c (g ∘ f) p =
    eval₂ c g
      (((rename f : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) (MvPolynomial τ ℤ)) :
          (a : MvPolynomial σ ℤ) → MvPolynomial τ ℤ)
        p)

Tactic:
(eval₂_rename c f g p).symm

Premises used: MvPolynomial.eval₂_rename, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
monomial : (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0
⊢ Eq.{u_4 + 1} (α := R)
    (coeff (Finsupp.mapDomain f d)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) r)))
    (coeff d ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) r))

Tactic:
rw [rename_monomial, coeff_monomial, coeff_monomial]

Premises used: MvPolynomial.rename_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0

Tactic:
simp only [(Finsupp.mapDomain_injective hf).eq_iff]

Premises used: Function.Injective.eq_iff, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
d : σ →₀ ℕ
p q : MvPolynomial σ R
h : coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = coeff d p
h_1 : coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = coeff d q
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) = coeff d (p + q)

Tactic:
simp only [*, map_add, coeff_add]

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

Tactic:
induction φ using MvPolynomial.induction_on' with
  | monomial u r =>
    rw [rename_monomial, coeff_monomial, coeff_monomial]
    simp only [(Finsupp.mapDomain_injective hf).eq_iff]
  | add =>
    simp only [*, map_add, coeff_add]

Premises used: MvPolynomial.monomial, Function.Injective.eq_iff, map_add, MvPolynomial.rename_monomial, MvPolynomial.coeff_add, MvPolynomial.coeff_monomial, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
monomial :
  ∀ (u : σ →₀ ℕ) (r : R),
    Eq.{u_4 + 1} (α := R)
      (coeff (Finsupp.mapDomain f d)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) r)))
      (coeff d ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) r))
add :
  ∀ (p q : MvPolynomial σ R),
    coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = coeff d p →
      coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = coeff d q →
        coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) = coeff d (p + q)
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ

Tactic:
classical
  induction φ using MvPolynomial.induction_on' with
  | monomial u r =>
    rw [rename_monomial, coeff_monomial, coeff_monomial]
    simp only [(Finsupp.mapDomain_injective hf).eq_iff]
  | add =>
    simp only [*, map_add, coeff_add]

Premises used: MvPolynomial.monomial, Function.Injective.eq_iff, map_add, MvPolynomial.rename_monomial, MvPolynomial.coeff_add, MvPolynomial.coeff_monomial, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
rw :
  coeff.{u_4, u_2} (σ := τ) (Finsupp.mapDomain (⇑f : (a : σ) → τ) d)
      ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) =
    coeff d φ
rw₁ rw₂ : coeff d φ = coeff d φ
⊢ coeff (embDomain f d) ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ

Tactic:
rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]

Premises used: MvPolynomial.coeff_rename_mapDomain, Finsupp.embDomain_eq_mapDomain, Function.Embedding.injective, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
rw : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0

Tactic:
rw [rename_eq, ← notMem_support_iff]

Premises used: MvPolynomial.notMem_support_iff, MvPolynomial.rename_eq
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ d ∈ Finset.image (Finsupp.mapDomain f) φ.support

Tactic:
replace H := mapDomain_support H
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ ∃ a ∈ φ.support, Finsupp.mapDomain f a = d

Tactic:
rw [Finset.mem_image] at H

Premises used: Finset.mem_image
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d
obtain :
  ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
    (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
⊢ False

Tactic:
obtain ⟨u, hu, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ coeff u φ = 0

Tactic:
specialize h u rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)

Tactic:
rw [Finsupp.mem_support_iff] at hu

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
hu₁ : Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)
⊢ coeff u φ = 0

Tactic:
rw [Finsupp.mem_support_iff] at hu

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)
h : coeff u φ = 0
⊢ False

Tactic:
contradiction