awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
⊢ Membership.mem (α := M) p (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂) : M)
have rcases : ∀ (y' : M₂) (hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p),
  Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy) : M₂) :
      M)
Tactic: rcases y with ⟨y', hy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (hypothesis)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy) : M₂) :
      M)
have hy₁ : ∃ y ∈ p, ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) y = y'
Tactic: rw [Submodule.mem_map] at hy
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy_1 : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
hy : ∃ y ∈ p, ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) y = y'
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy_1) : M₂) :
      M)
have rcases : ∀ (x : M) (hx : x ∈ p) (hxy : ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x = y'),
  Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy_1) : M₂) :
      M)
Tactic: rcases hy with ⟨x, hx, hxy⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
x : M
hx : x ∈ p
hxy : ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x = y'
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy) : M₂) :
      M)
have subst : ∀ (hy : Membership.mem (α := M₂) (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x : M₂)),
  Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
                (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x) hy) :
            M₂) :
          M₂) :
      M)
Tactic: subst hxy
Cleared hypotheses: y', hy, hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
⊢ (LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) ⋯).toFun
      ((fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
          (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) ⋯ : ↥p))
        y) =
    y
have a : (↑((LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) sorry).toFun
        ((fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
            (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) sorry : ↥p))
          y)) :
    M₂) =
  (↑y : M₂)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
p : Submodule R M
⊢ Eq (α := Submodule S M) (-restrictScalars S p) (restrictScalars S (-p))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule S M) (-restrictScalars S p) x ↔
    Membership.mem (γ := Submodule S M) (restrictScalars S (-p)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ r • m ∈ s • N
have rw : ∀ (p : Submodule R M),
  Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p} p →
    r • m ∈ p
Tactic: rw [mem_set_smul_def, mem_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
have mp : s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
N p : Submodule R M
mp : s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
have mpr : (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ s • N = ⨆ a ∈ s, a • N
have refine : Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p}
  (Set.Ici (⨆ a ∈ s, a • N))
Tactic: refine Eq.trans (congrArg sInf ?_) csInf_Ici
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p}
    (Set.Ici (⨆ a ∈ s, a • N))
have simp_rw : Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ (b : r ∈ s), ∀ a ∈ N, r • a ∈ p}
  {x : Submodule R M | ∀ (i : S) (i_1 : i ∈ s), i • N ≤ x}
Tactic: simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N = ⊥
have h : ∀ (x : M), x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N ↔ Membership.mem (γ := Submodule R M) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
⊢ x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N ↔ Membership.mem (γ := Submodule R M) ⊥ x
have h : x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N → Membership.mem (γ := Submodule R M) ⊥ x
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
h : x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N → Membership.mem (γ := Submodule R M) ⊥ x
⊢ x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N ↔ Membership.mem (γ := Submodule R M) ⊥ x
have h₁ : Membership.mem (γ := Submodule R M) ⊥ x → x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
x : M
hx : x ∈ HSMul.hSMul.{u_4, u_3, u_3} (α := Set S) ∅ N
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have hx₁ : ∀ (p : Submodule R M),
  Membership.mem (γ := Set (Submodule R M))
      {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, Membership.mem (γ := Set S) ∅ r → n ∈ N → r • n ∈ p} p →
    x ∈ p
Tactic: rw [mem_set_smul_def, Submodule.mem_sInf] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) s ⊥
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → Membership.mem (γ := Submodule R M) ⊥ n → Membership.mem (γ := Submodule R M) ⊥ (r • n)
Tactic: induction x, hx using set_smul_inductionOn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) s ⊥
smul₀ :
  ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → Membership.mem (γ := Submodule R M) ⊥ n → Membership.mem (γ := Submodule R M) ⊥ (r • n)
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have smul₁ : ∀ (r : R) ⦃m : M⦄,
  m ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
    Membership.mem (γ := Submodule R M) ⊥ m → Membership.mem (γ := Submodule R M) ⊥ (r • m)
Tactic: induction x, hx using set_smul_inductionOn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) s ⊥
smul₀ :
  ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → Membership.mem (γ := Submodule R M) ⊥ n → Membership.mem (γ := Submodule R M) ⊥ (r • n)
smul₁ :
  ∀ (r : R) ⦃m : M⦄,
    m ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      Membership.mem (γ := Submodule R M) ⊥ m → Membership.mem (γ := Submodule R M) ⊥ (r • m)
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have add : ∀ ⦃m₁ m₂ : M⦄,
  m₁ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
    m₂ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      Membership.mem (γ := Submodule R M) ⊥ m₁ →
        Membership.mem (γ := Submodule R M) ⊥ m₂ → Membership.mem (γ := Submodule R M) ⊥ (m₁ + m₂)
Tactic: induction x, hx using set_smul_inductionOn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
s : Set S
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) s ⊥
smul₀ :
  ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → Membership.mem (γ := Submodule R M) ⊥ n → Membership.mem (γ := Submodule R M) ⊥ (r • n)
smul₁ :
  ∀ (r : R) ⦃m : M⦄,
    m ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      Membership.mem (γ := Submodule R M) ⊥ m → Membership.mem (γ := Submodule R M) ⊥ (r • m)
add :
  ∀ ⦃m₁ m₂ : M⦄,
    m₁ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
      m₂ ∈ HSMul.hSMul (β := Submodule R M) s ⊥ →
        Membership.mem (γ := Submodule R M) ⊥ m₁ →
          Membership.mem (γ := Submodule R M) ⊥ m₂ → Membership.mem (γ := Submodule R M) ⊥ (m₁ + m₂)
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have zero : Membership.mem (γ := Submodule R M) ⊥ 0
Tactic: induction x, hx using set_smul_inductionOn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
⊢ HSMul.hSMul (α := Set S) {r} N = r • N
have closed_under_smul : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ r • N
Tactic: apply set_smul_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
closed_under_smul : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ r • N
⊢ HSMul.hSMul (α := Set S) {r} N = r • N
have le : r • N ≤ HSMul.hSMul (α := Set S) {r} N
Tactic: apply set_smul_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
r : S
m : M
hm : m ∈ (↑N : Set M)
⊢ Membership.mem (α := M) (HSMul.hSMul (α := Set S) {r} N) ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)
have le : ∀ (p : Submodule R M),
  Membership.mem (γ := Set (Submodule R M))
      {p : Submodule R M | ∀ ⦃r_1 : S⦄ {n : M}, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → r_1 • n ∈ p} p →
    Membership.mem (α := M) p ((DistribSMul.toLinearMap R M r : (a : M) → M) m : M)
Tactic: rw [mem_set_smul_def, Submodule.mem_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ x ∈ HSMul.hSMul (α := Set S) {r} N ↔ ∃ m ∈ N, x = r • m
have mp : x ∈ HSMul.hSMul (α := Set S) {r} N → ∃ m ∈ N, x = r • m
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
mp : x ∈ HSMul.hSMul (α := Set S) {r} N → ∃ m ∈ N, x = r • m
⊢ x ∈ HSMul.hSMul (α := Set S) {r} N ↔ ∃ m ∈ N, x = r • m
have mpr : (∃ m ∈ N, x = r • m) → x ∈ HSMul.hSMul (α := Set S) {r} N
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
t : R
n : M
mem : n ∈ HSMul.hSMul (α := Set S) {r} N
h : ∃ m ∈ N, n = r • m
⊢ ∃ m ∈ N, t • n = r • m
have mp : ∀ (n : M) (hn : n ∈ N) (mem : r • n ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, t • r • n = r • m
Tactic: rcases h with ⟨n, hn, rfl⟩
Cleared hypotheses: n, mem, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₁ m₂ : M
mem₁ : m₁ ∈ HSMul.hSMul (α := Set S) {r} N
mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N
h₁ : ∃ m ∈ N, m₁ = r • m
h₂ : ∃ m ∈ N, m₂ = r • m
⊢ ∃ m ∈ N, m₁ + m₂ = r • m
have mp : ∀ (m₁ : M) (h₁ : m₁ ∈ N) (mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, r • m₁ + m₂ = r • m
Tactic: rcases h₁ with ⟨m₁, h₁, rfl⟩
Cleared hypotheses: m₁, mem₁, h₁
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x m₂ : M
mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N
h₂ : ∃ m ∈ N, m₂ = r • m
m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ HSMul.hSMul (α := Set S) {r} N
⊢ ∃ m ∈ N, r • m₁ + m₂ = r • m
have mp : ∀ (m₂ : M) (h₂ : m₂ ∈ N) (mem₂ : r • m₂ ∈ HSMul.hSMul (α := Set S) {r} N), ∃ m ∈ N, r • m₁ + r • m₂ = r • m
Tactic: rcases h₂ with ⟨m₂, h₂, rfl⟩
Cleared hypotheses: m₂, mem₂, h₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
hx : x ∈ HSMul.hSMul (α := Set S) {r} N
⊢ ∃ m ∈ N, x = r • m
have mp : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → ∃ m ∈ N, r_1 • n = r • m
Tactic: induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
hx : x ∈ HSMul.hSMul (α := Set S) {r} N
mp : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → ∃ m ∈ N, r_1 • n = r • m
⊢ ∃ m ∈ N, x = r • m
have mp₁ : ∀ (t : R) ⦃n : M⦄ (mem : n ∈ HSMul.hSMul (α := Set S) {r} N) (h : ∃ m ∈ N, n = r • m), ∃ m ∈ N, t • n = r • m
Tactic: induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
hx : x ∈ HSMul.hSMul (α := Set S) {r} N
mp : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → ∃ m ∈ N, r_1 • n = r • m
mp₁ : ∀ (t : R) ⦃n : M⦄ (mem : n ∈ HSMul.hSMul (α := Set S) {r} N) (h : ∃ m ∈ N, n = r • m), ∃ m ∈ N, t • n = r • m
⊢ ∃ m ∈ N, x = r • m
have mp₂ : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ HSMul.hSMul (α := Set S) {r} N) (mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N)
  (h₁ : ∃ m ∈ N, m₁ = r • m) (h₂ : ∃ m ∈ N, m₂ = r • m), ∃ m ∈ N, m₁ + m₂ = r • m
Tactic: induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass R S M
r : S
x : M
hx : x ∈ HSMul.hSMul (α := Set S) {r} N
mp : ∀ ⦃r_1 : S⦄ ⦃n : M⦄, Membership.mem (γ := Set S) {r} r_1 → n ∈ N → ∃ m ∈ N, r_1 • n = r • m
mp₁ : ∀ (t : R) ⦃n : M⦄ (mem : n ∈ HSMul.hSMul (α := Set S) {r} N) (h : ∃ m ∈ N, n = r • m), ∃ m ∈ N, t • n = r • m
mp₂ :
  ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ HSMul.hSMul (α := Set S) {r} N) (mem₂ : m₂ ∈ HSMul.hSMul (α := Set S) {r} N)
    (h₁ : ∃ m ∈ N, m₁ = r • m) (h₂ : ∃ m ∈ N, m₂ = r • m), ∃ m ∈ N, m₁ + m₂ = r • m
⊢ ∃ m ∈ N, x = r • m
have mp₃ : ∃ m ∈ N, 0 = r • m
Tactic: induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
⊢ p x hx
have smul₂ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m sorry → p (r • m) sorry
Tactic: simp_all only [← Submodule.singleton_set_smul]
Cleared hypotheses: smul₁, add, zero
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
smul₂ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
⊢ p x hx
have add₁ : ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
  p x sorry → p y sorry → p (x + y) sorry
Tactic: simp_all only [← Submodule.singleton_set_smul]
Cleared hypotheses: smul₁, add, zero