awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
let let₁ let₂ :
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
let₃ :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
have mp : let RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := sorry, zero_mem' := sorry,
    smul_mem' := sorry };
Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
Tactic: classical
  let RHS : Ideal (MonoidAlgebra k G) :=
    { carrier := { p | ∀ m : G, m ∈ p.support → ∃ m' ∈ s, ∃ d, m = d * m' }
      add_mem' {x y} hx hy m hm := (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
      zero_mem' := by simp
      smul_mem' x y hy m hm := by
        simp only [smul_eq_mul, mul_def] at hm
        obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
        refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
        rintro ⟨d, rfl⟩
        exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
  change _ ↔ x ∈ RHS
  constructor
  · suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 1, ?_⟩
    simpa using Finsupp.support_single_subset hm
  · intro hx
    rw [← Finsupp.sum_single x]
    apply Ideal.sum_mem _ fun i hi ↦ ?_
    obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
    simpa using Ideal.mul_mem_left _ (.single d2 <| x (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
let let₁ let₂ :
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
let₃ :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
mp :
  let RHS : Ideal k[G] :=
    { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ };
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
have mpr : let RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := sorry, zero_mem' := sorry,
    smul_mem' := sorry };
x ∈ RHS → Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x
Tactic: classical
  let RHS : Ideal (MonoidAlgebra k G) :=
    { carrier := { p | ∀ m : G, m ∈ p.support → ∃ m' ∈ s, ∃ d, m = d * m' }
      add_mem' {x y} hx hy m hm := (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
      zero_mem' := by simp
      smul_mem' x y hy m hm := by
        simp only [smul_eq_mul, mul_def] at hm
        obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
        refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
        rintro ⟨d, rfl⟩
        exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
  change _ ↔ x ∈ RHS
  constructor
  · suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 1, ?_⟩
    simpa using Finsupp.support_single_subset hm
  · intro hx
    rw [← Finsupp.sum_single x]
    apply Ideal.sum_mem _ fun i hi ↦ ?_
    obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
    simpa using Ideal.mul_mem_left _ (.single d2 <| x (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Lift (goal)
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
| HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) a : R)
    ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) b : R)
have rw : HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
  ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)
Tactic: rw [← sum_single a, ← sum_single b]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Lift (goal)
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) a : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) b : R)
have conv_rhs : (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
  HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
    ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)
Tactic: conv_rhs => rw [← sum_single a, ← sum_single b]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Lift (goal)
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum a single) : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : k[G]) → R) (sum b single) : R)
have simp_rw : Eq.{u_2 + 1} (α := R)
  (sum a fun (a : G) (b_1 : k) ↦
    sum b fun (a_1 : G) (b : k) ↦
      HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * b) : R) ((g : (a : G) → R) (a * a_1) : R))
  (sum a fun (a : G) (c : k) ↦
    sum b fun (a_1 : G) (c_1 : k) ↦
      HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))
Tactic: simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Lift (goal)
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : Semiring R
g_hom : Type u_6
inst_3 : FunLike g_hom G R
inst_4 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm :
  ∀ {x y : G},
    y ∈ a.support → Commute.{u_2} (S := R) ((f : (a : k) → R) ((b : (a : G) → k) x : k) : R) ((g : (a : G) → R) y : R)
⊢ Eq.{u_2 + 1} (α := R)
    (sum a fun (a : G) (b_1 : k) ↦
      sum b fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (sum a fun (a : G) (c : k) ↦
      sum b fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))
have refine : ∀ (y : G) (hy : y ∈ a.support) (x : G) (_hx : x ∈ b.support),
  Eq.{u_2 + 1} (α := R)
    ((fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (HMul.hMul (α := k) ((a : (a : G) → k) y : k) b) : R)
          ((g : (a : G) → R) (y * a_1) : R))
      x ((b : (a : G) → k) x))
    ((fun (a_1 : G) (c : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) ((a : (a : G) → k) y : k) : R)
            ((g : (a : G) → R) y : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a_1 : R))
      x ((b : (a : G) → k) x))
Tactic: refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
a : M
r : R
⊢ Eq (α := R[N]) (mapDomain f (single a r)) (single (f a) r)
have hfg : ∀ (m : N), Eq.{u_3 + 1} (α := R) ((mapDomain f (single a r) : (a : N) → R) m : R) ((single (f a) r : (a : N) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
⊢ Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))
have simp_rw : Eq (α := Set S[M]) (Set.range (map f))
  (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) sorry ((coeffEquiv : (a : R[M]) → M →₀ R) x)))
Tactic: simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
simp_rw :
  Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x)))
⊢ Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))
have simp_rw₁ : Eq (α := Set (M →₀ S)) (Set.image (α := S[M]) (⇑coeffEquiv : (a : S[M]) → M →₀ S) (Set.range (map f)))
  (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) sorry ((coeffEquiv : (a : R[M]) → M →₀ R) x))
Tactic: simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
simp_rw :
  Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x)))
simp_rw₁ :
  Eq (α := Set (M →₀ S)) (Set.image (α := S[M]) (⇑coeffEquiv : (a : S[M]) → M →₀ S) (Set.range (map f)))
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x))
⊢ Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))
have simp_rw₂ : Eq (α := Set (M →₀ S)) (Set.range fun (x : R[M]) ↦ (coeffEquiv : (a : S[M]) → M →₀ S) (map f x))
  (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) sorry ((coeffEquiv : (a : R[M]) → M →₀ R) x))
Tactic: simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
simp_rw :
  Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x)))
simp_rw₁ :
  Eq (α := Set (M →₀ S)) (Set.image (α := S[M]) (⇑coeffEquiv : (a : S[M]) → M →₀ S) (Set.range (map f)))
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x))
simp_rw₂ :
  Eq (α := Set (M →₀ S)) (Set.range fun (x : R[M]) ↦ (coeffEquiv : (a : S[M]) → M →₀ S) (map f x))
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x))
⊢ Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))
have simp_rw₃ : Eq (α := Set (M →₀ S)) (Set.range fun (x : R[M]) ↦ (map f x).coeff)
  (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) sorry x.coeff)
Tactic: simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
have h : ∀ (x : R[M]) (m : M),
  Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
    ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
            (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) sorry) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
          (a : M) → S)
        m :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (hypothesis)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Injective (α := R[M]) (map f)
have this : Eq (α := (x : R[M]) → S[M]) (map f)
  (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
    (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) sorry) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
Tactic: have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
have h : ∀ (x : R[M]) (m : M),
  Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
    ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
            (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) sorry) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
          (a : M) → S)
        m :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (hypothesis)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Surjective (α := R[M]) (map f)
have this : Eq (α := (x : R[M]) → S[M]) (map f)
  (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
    (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) sorry) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
Tactic: have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Mul M
⊢ Eq (α := R[M] →ₙ+* R[M]) (mapDomainNonUnitalRingHom R (MulHom.id M)) (NonUnitalRingHom.id R[M])
have a : ∀ (x : R[M]) (m : M),
  Eq.{u_3 + 1} (α := R)
    ((((mapDomainNonUnitalRingHom R (MulHom.id M) : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
    ((((NonUnitalRingHom.id R[M] : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
f : N →ₙ* O
g : M →ₙ* N
⊢ Eq (α := R[M] →ₙ+* R[O]) (mapDomainNonUnitalRingHom R (f.comp g))
    (NonUnitalRingHom.comp (mapDomainNonUnitalRingHom R f) (mapDomainNonUnitalRingHom R g))
have a : ∀ (x : R[M]) (m : O),
  Eq.{u_3 + 1} (α := R) ((((mapDomainNonUnitalRingHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((NonUnitalRingHom.comp (mapDomainNonUnitalRingHom R f) (mapDomainNonUnitalRingHom R g) : (a : R[M]) → R[O]) x :
            R[O]) :
          (a : O) → R)
        m :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[M]
⊢ (fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M]))
      ((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N])) x) =
    x
have hfg : ∀ (m : M),
  Eq.{u_3 + 1} (α := R)
    (((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M]))
            ((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N])) x) :
          (a : M) → R)
        m :
      R)
    ((x : (a : M) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[N]
⊢ (fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N]))
      ((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M])) x) =
    x
have hfg : ∀ (m : N),
  Eq.{u_3 + 1} (α := R)
    (((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N]))
            ((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M])) x) :
          (a : N) → R)
        m :
      R)
    ((x : (a : N) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x y : R[M]
⊢ mapDomain (⇑e : (a : M) → N) (x + y) =
    HAdd.hAdd (α := R[N]) (mapDomain (⇑e : (a : M) → N) x) (mapDomain (⇑e : (a : M) → N) y)
have hfg : ∀ (m : N),
  Eq.{u_3 + 1} (α := R) ((mapDomain (⇑e : (a : M) → N) (x + y) : (a : N) → R) m : R)
    ((HAdd.hAdd (α := R[N]) (mapDomain (⇑e : (a : M) → N) x) (mapDomain (⇑e : (a : M) → N) y) : (a : N) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
⊢ Eq (α := R[M] ≃+ R[O]) (mapDomainAddEquiv R (e₁.trans e₂))
    (AddEquiv.trans (mapDomainAddEquiv R e₁) (mapDomainAddEquiv R e₂))
have h : ∀ (x : R[M]) (m : O),
  Eq.{u_3 + 1} (α := R) ((((mapDomainAddEquiv R (e₁.trans e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((AddEquiv.trans (mapDomainAddEquiv R e₁) (mapDomainAddEquiv R e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R)
        m :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : R[M]
⊢ map (↑e.symm : S →+ R) (map (↑e : R →+ S) x) = x
have hfg : ∀ (m : M),
  Eq.{u_3 + 1} (α := R) ((map (↑e.symm : S →+ R) (map (↑e : R →+ S) x) : (a : M) → R) m : R) ((x : (a : M) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : S[M]
⊢ map (↑e : R →+ S) (map (↑e.symm : S →+ R) x) = x
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := S) ((map (↑e : R →+ S) (map (↑e.symm : S →+ R) x) : (a : M) → S) m : S) ((x : (a : M) → S) m : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
⊢ Eq (α := R[M] ≃+ T[M]) (mapAddEquiv M (e₁.trans e₂)) (AddEquiv.trans (mapAddEquiv M e₁) (mapAddEquiv M e₂))
have h : ∀ (x : R[M]) (m : M),
  Eq.{u_5 + 1} (α := T) ((((mapAddEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
    ((((AddEquiv.trans (mapAddEquiv M e₁) (mapAddEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Mul M
f : R →+* S
x y : R[M]
⊢ map (↑f : R →+ S) (x * y) = HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y)
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) (x * y) : (a : M) → S) m : S)
    ((HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y) : (a : M) → S) m : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Mul M
f : R →+* S
x y : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) (x * y) : (a : M) → S) m : S)
    ((HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y) : (a : M) → S) m : S)
have hfg : Eq.{u_4 + 1} (α := S)
  ((f : (a : R) → S)
      (sum x fun (a₁ : M) (b : R) ↦
        sum y fun (a₁_1 : M) (b_1 : R) ↦ (coeff (single (a₁ * a₁_1) (b * b_1)) : (a : M) → R) m) :
    S)
  ((sum (map (↑f : R →+ S) x) fun (m₁ : M) (r₁ : S) ↦
          sum (map (↑f : R →+ S) y) fun (m₂ : M) (r₂ : S) ↦ single (m₁ * m₂) (r₁ * r₂) :
        (a : M) → S)
      m :
    S)
Tactic: simp [mul_def]