awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₁ :
        R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₁ :
        R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₁ :
        R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₆ : Eq (α := R[M]) (single (m₁ * m₂) (HMul.hMul (α := R) 1 1)) (single (m₁ * m₂) 1)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₁ :
        R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
rw₆ : Eq (α := R[M]) (single (m₁ * m₂) (HMul.hMul (α := R) 1 1)) (single (m₁ * m₂) 1)
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₇ : Eq (α := R[M]) (single (m₁ * m₂) 1) (single (m₁ * m₂) 1)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
f g : R[M]
ihf :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f + g
have hadd : ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        g
Tactic: rcases ihf with ⟨P, rfl⟩
Cleared hypotheses: f, ihf
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
g : R[M]
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        g
have hadd : ∀ (Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M]) (β := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            Q :
          R[M])
Tactic: rcases ihg with ⟨Q, rfl⟩
Cleared hypotheses: g, ihg
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
r : R
f : R[M]
ih :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      r • f
have hsmul : ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HSMul.hSMul (β := R[M]) r
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
Tactic: rcases ih with ⟨P, rfl⟩
Cleared hypotheses: f, ih
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
f : R[M]
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
have hM : ∀ (m : M),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : M) → R[M]) m : R[M])
Tactic: induction f using induction_on with
  | hM m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
  | hadd f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | hsmul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
f : R[M]
hM :
  ∀ (m : M),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      Eq (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            a :
          R[M])
        ((of R M : (a : M) → R[M]) m : R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
have hadd : ∀ (f g : R[M])
  (ihf :
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        f)
  (ihg :
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        g),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f + g
Tactic: induction f using induction_on with
  | hM m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
  | hadd f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | hsmul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ OrzechProperty R
have refine : ∀ {M : Type u_1} (x : AddCommMonoid M) (x_1 : Module R M),
  Module.Finite R M →
    ∀ {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)),
      Function.Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
Tactic: refine ⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
⊢ Function.Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
have refine : ∀ (n : ↥N) (hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)), n = 0
Tactic: refine LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
⊢ n = 0
have obtain : ∀ (k : ℕ) (mj : Fin k → M) (hmj : Eq (α := Submodule R M) (span R (Set.range mj)) ⊤), n = 0
Tactic: obtain ⟨k, mj, hmj⟩ := exists_fin (R := R) (M := M)