awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : S
⊢ eval₂ φ (fun (x : σ) ↦ a) ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f) =
    Polynomial.eval₂ φ a f
have rw : Polynomial.eval₂ φ a f = Polynomial.eval₂ φ a f
Tactic: rw [eval₂_uniqueAlgEquiv_symm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) = eval₂ φ (fun (x : σ) ↦ a) f
have rw : Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) =
  Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f)
Tactic: rw [← eval₂_uniqueAlgEquiv]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : IsEmpty σ
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R)
    (AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a))
    (AlgHom.id R (MvPolynomial σ R))
have hf : ∀ (i : σ) (m : σ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X i)))
    (coeff m ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
Tactic: ext i m
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))
have hf : ∀ (i : σ),
  Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R) : (a : MvPolynomial σ R) → S₁)
        (X i) :
      S₁)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
⊢ Injective (α := MvPolynomial σ R) (β := S₁) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) ↔
    Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑(algebraMap R S₁) : (a : R) → S₁)
have this : Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
  (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))
Tactic: have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom := by
    ext i
    exact IsEmpty.elim' ‹IsEmpty σ› i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
this :
  Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))
⊢ Injective (α := MvPolynomial σ R) (β := S₁) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) ↔
    Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑(algebraMap R S₁) : (a : R) → S₁)
have rw : Injective (α := MvPolynomial σ R) (β := S₁)
    (⇑(AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R)) :
      (a : MvPolynomial σ R) → S₁) ↔
  Injective (α := MvPolynomial σ R) (β := S₁)
    (Function.comp (β := R) (⇑(algebraMap R S₁) : (a : R) → S₁) (⇑(isEmptyAlgEquiv R σ) : (a : MvPolynomial σ R) → R))
Tactic: rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : IsEmpty σ
x : MvPolynomial σ R
⊢ (isEmptyRingEquiv R σ : (a : MvPolynomial σ R) → R) x = coeff 0 x
have obtain : ∀ (x : R),
  Eq.{u_3 + 1} (α := R)
    ((isEmptyRingEquiv R σ : (a : MvPolynomial σ R) → R)
        ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) :
      R)
    (coeff.{u_3, u_2} (σ := σ) 0 ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x) : R)
Tactic: obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
have hfgC : Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
  (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
Tactic: apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hfgC :
  Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
have hfgX : ∀ (n : S₁),
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X n)) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    (X n : MvPolynomial S₁ (MvPolynomial S₂ R))
Tactic: apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hfgC :
  Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
hfgX :
  ∀ (n : S₁),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X n)) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      (X n : MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
have hgfC : Eq (α := R →+* MvPolynomial (S₁ ⊕ S₂) R) (RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) C
Tactic: apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hfgC :
  Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
hfgX :
  ∀ (n : S₁),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X n)) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      (X n : MvPolynomial S₁ (MvPolynomial S₂ R))
hgfC :
  Eq (α := R →+* MvPolynomial (S₁ ⊕ S₂) R) (RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) C
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
have hgfX : ∀ (n : S₁ ⊕ S₂),
  Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
        ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n)) :
      MvPolynomial (S₁ ⊕ S₂) R)
    (X n : MvPolynomial (S₁ ⊕ S₂) R)
Tactic: apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
have refine : Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
  (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)
Tactic: refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
refine :
  Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)
⊢ Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
have refine₁ : ∀ (n : S₂),
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C :
          (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        (X n) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n) : MvPolynomial S₁ (MvPolynomial S₂ R))
Tactic: refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)
have a₃ : ∀ (x : R),
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C :
          (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        x :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp C C : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) x : MvPolynomial S₁ (MvPolynomial S₂ R))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := R →+* MvPolynomial (S₁ ⊕ S₂) R) (RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) C
have hgfC : ∀ (x : R),
  Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x :
      MvPolynomial (S₁ ⊕ S₂) R)
    ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x : MvPolynomial (S₁ ⊕ S₂) R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
r : R
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    (Equiv.toFun (RingEquiv.toEquiv (sumRingEquiv R S₁ S₂))
      ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r)
have A : Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
  ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r :
    MvPolynomial S₁ (MvPolynomial S₂ R))
  ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) r) :
    MvPolynomial S₁ (MvPolynomial S₂ R))
Tactic: have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) :) := rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
r : R
A :
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) r) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    (Equiv.toFun (RingEquiv.toEquiv (sumRingEquiv R S₁ S₂))
      ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r)
have B : Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
  ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)
  ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)
Tactic: have B : algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) r = C r := rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
⊢ Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
    (AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
      (rename Sum.inr))
    (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)))
have hf : ∀ (i : S₂) (m : S₁ →₀ ℕ) (m_1 : S₂ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m_1
      (coeff m
        ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
              (rename Sum.inr) :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
    (coeff m_1
      (coeff m
        ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)) :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
⊢ Eq (α := MvPolynomial S₁ R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
    (AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
      (rename Sum.inl))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R)))
have hf : ∀ (i : S₁) (m : S₁ →₀ ℕ) (m_1 : S₂ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m_1
      (coeff m
        ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
              (rename Sum.inl) :
            (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
    (coeff m_1
      (coeff m
        ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R)) :
            (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R))
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) p) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((map C : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R)) p : MvPolynomial S₂ (MvPolynomial S₁ R))
have suffices : Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
  (AlgHom.comp (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
  (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))
Tactic: suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
    exact DFunLike.congr_fun this p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
⊢ Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (AlgHom.comp
      (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))
have hf : ∀ (x : S₂),
  Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((AlgHom.comp
            (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
            (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) :
          (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
        (X x) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)) : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
        (X x) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := (MvPolynomial S₁ R)[X] →ₐ[R] (MvPolynomial S₁ R)[X])
    (AlgHom.comp
      (aeval fun (o : Option S₁) ↦
        o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (Polynomial.aevalTower (rename Option.some) (X none)))
    (AlgHom.id R (MvPolynomial S₁ R)[X])
have hC : ∀ (i : S₁),
  Eq (α := (MvPolynomial S₁ R)[X])
    ((AlgHom.comp
            (AlgHom.comp
              (aeval fun (o : Option S₁) ↦
                o.elim Polynomial.X fun (s : S₁) ↦
                  (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
              (Polynomial.aevalTower (rename Option.some) (X none)))
            CAlgHom :
          (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (X i) :
      (MvPolynomial S₁ R)[X])
    ((AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X]) CAlgHom : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (X i) :
      (MvPolynomial S₁ R)[X])
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hC :
  ∀ (i : S₁),
    Eq (α := (MvPolynomial S₁ R)[X])
      ((AlgHom.comp
              (AlgHom.comp
                (aeval fun (o : Option S₁) ↦
                  o.elim Polynomial.X fun (s : S₁) ↦
                    (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
                (Polynomial.aevalTower (rename Option.some) (X none)))
              CAlgHom :
            (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (X i) :
        (MvPolynomial S₁ R)[X])
      ((AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X]) CAlgHom : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (X i) :
        (MvPolynomial S₁ R)[X])
⊢ Eq (α := (MvPolynomial S₁ R)[X] →ₐ[R] (MvPolynomial S₁ R)[X])
    (AlgHom.comp
      (aeval fun (o : Option S₁) ↦
        o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (Polynomial.aevalTower (rename Option.some) (X none)))
    (AlgHom.id R (MvPolynomial S₁ R)[X])
have hX : ∀ (n : ℕ),
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff
      ((AlgHom.comp
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)) :
          (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X])
        Polynomial.X)
      n)
    (Polynomial.coeff
      ((AlgHom.id R (MvPolynomial S₁ R)[X] : (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X]) Polynomial.X) n)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] MvPolynomial.{v, u} (Option S₁) R)
    (AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
      (aeval fun (o : Option S₁) ↦
        o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)))
    (AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R))
have hf : ∀ (i : Option S₁) (m : Option S₁ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
i : Option S₁
m : Option S₁ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
have hf : Eq.{u + 1} (α := R)
  (coeff m
    ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
          (aeval fun (o : Option S₁) ↦
            o.elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
        (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
      (X none)))
  (coeff m
    ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
      (X none)))
Tactic: cases i
Cleared hypotheses: i