awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: classical
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain₁ : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
  (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: classical
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₁ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain₂ : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
  (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
  (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: classical
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₁ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₂ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain₃ : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
  (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
  (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)) (hAB : A ≤ A ⊔ Algebra.adjoin R (↑{s} : Set S)),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: classical
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] N) (f.toFun' S) (toFun S f)
have h : ∀ (t : S ⊗[R] M), f.toFun' S t = toFun S f t
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ f.toFun' S t = toFun S f t
have h : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  f.toFun' S t = toFun S f t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
⊢ f.toFun' S t = toFun S f t
have h : f.toFun' S t = f.toFun' S ((rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p)
Tactic: simp only [f.toFun_eq_rTensor_φ_toFun' ha, f.isCompat_apply']
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
have obtain : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
x : S
hx : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (AlgHom.range (φ R s'))
    ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx) :
      T)
have simp : ∀ (hx_1 : Membership.mem (γ := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) x),
  Membership.mem (α := T) (γ := Subalgebra R T) (Algebra.adjoin R (↑s' : Set T))
    ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx) :
      T)
Tactic: simp only [range_φ] at hx ⊢
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
x : S
hx_1 : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x
hx : Membership.mem (γ := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) x
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Algebra.adjoin R (↑s' : Set T))
    ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx_1) :
      T)
have simp : Membership.mem (α := T) (Subalgebra.map h (Algebra.adjoin R (↑s : Set S))) ((h : (a : S) → T) x : T)
Tactic: simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
⊢ AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
have hf : ∀ (p : Fin s.card),
  Eq.{w + 1} (α := T) ((AlgHom.comp (φ R s') (rename j) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
    ((h.comp (φ R s) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p_1 : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
⊢ Eq.{w + 1} (α := T) ((AlgHom.comp (φ R s') (rename j) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
    ((h.comp (φ R s) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
have hf : Eq.{w + 1} (α := T)
  ((aeval ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) :
        (a : MvPolynomial (Fin s.card) R) → T)
      (X p) :
    T)
  ((aeval fun (i : Fin s.card) ↦ (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S) :
        (a : MvPolynomial (Fin s.card) R) → T)
      (X p) :
    T)
Tactic: simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p_1 : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
⊢ Eq.{w + 1} (α := T)
    ((aeval ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)
    ((aeval fun (i : Fin s.card) ↦ (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)
have hf : Eq.{w + 1} (α := Fin s.card → T) ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j)
  fun (i : Fin s.card) ↦ (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p_1 : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
⊢ Eq.{w + 1} (α := Fin s.card → T)
    ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) fun (i : Fin s.card) ↦
    (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S)
have hf : ∀ (n : Fin s.card),
  Eq.{w + 1} (α := T) (((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) n : T)
    ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S) : T)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
have eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
Tactic: have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
    ext p
    simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
    congr
    ext n
    simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
have ha' : Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
  ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
Tactic: have ha' : π R M T (⟨s', p'⟩ : lifts R M T) = rTensor M h.toLinearMap t := by
    simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]