awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 (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)
have 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)
Tactic: rw [← rename_rename, rename_rename e]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ Eq.{u_4 + 1} (α := R)
    (coeff (Finsupp.mapDomain f d)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial u : (a : R) → MvPolynomial σ R) r)))
    (coeff d ((monomial u : (a : R) → MvPolynomial σ R) r))
have monomial : (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0
Tactic: rw [rename_monomial, coeff_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have monomial : ∀ (u : σ →₀ ℕ) (r : R),
  Eq.{u_4 + 1} (α := R)
    (coeff (Finsupp.mapDomain f d)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial u : (a : R) → MvPolynomial σ R) r)))
    (coeff d ((monomial u : (a : R) → MvPolynomial σ R) r))
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]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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))
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have 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)
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]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have monomial : ∀ (u : σ →₀ ℕ) (r : R),
  Eq.{u_4 + 1} (α := R)
    (coeff (Finsupp.mapDomain f d)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial u : (a : R) → MvPolynomial σ R) r)))
    (coeff d ((monomial u : (a : R) → MvPolynomial σ R) r))
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]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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))
⊢ coeff (Finsupp.mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have 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)
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]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (embDomain f d) ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have rw : coeff.{u_4, u_2} (σ := τ) (Finsupp.mapDomain (⇑f : (a : σ) → τ) d)
    ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) =
  coeff d φ
Tactic: rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 φ
⊢ coeff (embDomain f d) ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) = coeff d φ
have rw₁ : coeff d φ = coeff d φ
Tactic: rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
Tactic: rw [rename_eq, ← notMem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (hypothesis)
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) φ)
⊢ False
have H₁ : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
Tactic: replace H := mapDomain_support H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (hypothesis)
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
⊢ False
have H₁ : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d
Tactic: rw [Finset.mem_image] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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
⊢ False
have obtain : ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
  (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
Tactic: obtain ⟨u, hu, rfl⟩ := H
Cleared hypotheses: d, h, H
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (hypothesis)
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
⊢ False
have h₁ : coeff u φ = 0
Tactic: specialize h u rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (hypothesis)
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
⊢ False
have hu₁ : Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)
Tactic: rw [Finsupp.mem_support_iff] at hu
Cleared hypotheses: hu, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₁ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₆ : ∀ (H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d), False
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
rw₆ : ∀ (H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₇ : ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
  (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
rw₆ : ∀ (H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d), False
rw₇ :
  ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
    (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₈ : ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support) (h : coeff u φ = 0), False
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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 : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
rw₆ : ∀ (H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d), False
rw₇ :
  ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
    (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
rw₈ : ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support) (h : coeff u φ = 0), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
have rw₉ : ∀ (u : σ →₀ ℕ) (hu : Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)) (h : coeff u φ = 0), False
Tactic: classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : Ne.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
⊢ ∃ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0
have contrapose! : ∀ (h : ∀ (u : σ →₀ ℕ) (_ : Finsupp.mapDomain f u = d), coeff u φ = 0),
  Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) φ : R)
have C : ∀ (a : R),
  Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : R)
Tactic: apply φ.induction_on
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
            MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) φ : R)
have add : ∀ (p q : MvPolynomial σ R),
  Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) →
    Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) q : R) →
      Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q) : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) (p + q) : R)
Tactic: apply φ.induction_on
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
            MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) →
      Eq.{u_4 + 1} (α := R)
          ((constantCoeff : (a : MvPolynomial τ R) → R)
              ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q : MvPolynomial τ R) :
            R)
          ((constantCoeff : (a : MvPolynomial σ R) → R) q : R) →
        Eq.{u_4 + 1} (α := R)
          ((constantCoeff : (a : MvPolynomial τ R) → R)
              ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q) : MvPolynomial τ R) :
            R)
          ((constantCoeff : (a : MvPolynomial σ R) → R) (p + q) : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) φ : R)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) →
    Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n) : MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R) (p * X n) : R)
Tactic: apply φ.induction_on
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst_1 : DecidableEq τ
h : Injective f
⊢ support.{u_4, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    Finset.image (Finsupp.mapDomain f) p.support
have rw : support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support
Tactic: rw [rename_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ support.{u_4, u_2} (R := R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
have rw : {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ p.support
Tactic: rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ support.{u_4, u_2} (R := R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
have rw : Finset.image (Finsupp.mapDomain f)
    (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
  p.support
Tactic: classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
rw :
  Finset.image (Finsupp.mapDomain f)
      (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
⊢ support.{u_4, u_2} (R := R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
have rw₁ : Finset.image (Finsupp.mapDomain f) (p.support.preimage (Finsupp.mapDomain f) sorry) ⊆ p.support
Tactic: classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..