awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 1}

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R

Tactic:
exact ⟨(presentationFinsupp A G).ofLinearEquiv e.symm, by dsimp; infer_instance⟩
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
p : Presentation.{v, w₁, v, u} A M
h : IsEmpty.{w₁ + 1} p.R
⊢ Free A M

Tactic:
p.toIsPresentation.free

Premises used: Module.Relations.Solution.IsPresentation.free, Module.Presentation.toIsPresentation
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
p : Presentation.{v, w₁, v, u} A M
h : IsEmpty.{w₁ + 1} p.R
⊢ Free A M

Tactic:
exact p.toIsPresentation.free

Premises used: Module.Relations.Solution.IsPresentation.free, Module.Presentation.toIsPresentation
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
h :
  ∀ (v : Finsupp.{u_5, u_1} presM.R B),
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            match (motive := Prod.{u_6, u_5} presB.G presM.R → Finsupp.{u_5, u_1} presM.R B) x with
            | (g, g') => HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single g' 1)))
        v ↔
      Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B)) ⊤ v
⊢ Eq (α := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        match (motive := Prod.{u_6, u_5} presB.G presM.R → Finsupp.{u_5, u_1} presM.R B) x with
        | (g, g') => HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single g' 1)))
    ⊤

Tactic:
ext v
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
h :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    v
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
      (Submodule.span A
        (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
          HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
      v ↔
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B)) ⊤ v

Tactic:
simp only [Submodule.mem_top, iff_true]

Premises used: iff_true, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
h :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    0
h₁ :
  ∀ (a : presM.R) (b : B) (f : Finsupp.{u_5, u_1} presM.R B),
    a ∉ f.support →
      b ≠ 0 →
        Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
            (Submodule.span A
              (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
                HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
            f →
          Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
            (Submodule.span A
              (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
                HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
            (Finsupp.single a b + f)
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    v

Tactic:
apply Finsupp.induction
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
b : B
w : Finsupp.{u_5, u_1} presM.R B
h :
  r ∉ w.support →
    b ≠ 0 →
      Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          w →
        Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r b + w)
⊢ r ∉ w.support →
    b ≠ 0 →
      Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          w →
        Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r b + w)

Tactic:
_
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
b : B
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
h :
  b ≠ 0 →
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        w →
      Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r b + w)
⊢ b ≠ 0 →
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        w →
      Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r b + w)

Tactic:
_
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
b : B
w : Finsupp.{u_5, u_1} presM.R B
h : r ∉ w.support
h_1 : b ≠ 0
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r b + w)

Tactic:
Submodule.add_mem _ ?_ hw

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
b : B
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
h_2 : b ≠ 0
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
h :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r b)
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r b + w)

Tactic:
refine Submodule.add_mem _ ?_ hw

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
b : B
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
h_2 : b ≠ 0
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
h :
  ∀ (β : Finsupp.{u_6, u_3} presB.G A),
    Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B) →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) β) : Finsupp.{u_5, u_1} presM.R B)
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r b)

Tactic:
obtain ⟨β, rfl⟩ := presB.surjective_π b

Premises used: Module.Presentation.toIsPresentation, Module.Relations.Solution.IsPresentation.surjective_π, rfl
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
β : Finsupp.{u_6, u_3} presB.G A
h_2 : Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B)
h :
  Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) 0) : Finsupp.{u_5, u_1} presM.R B)
h₁ :
  ∀ (a : presB.G) (b : A) (f : Finsupp.{u_6, u_3} presB.G A),
    a ∉ f.support →
      b ≠ 0 →
        Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
            (Submodule.span A
              (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
                HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
            (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
          Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
            (Submodule.span A
              (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
                HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
            (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single a b + f)) :
              Finsupp.{u_5, u_1} presM.R B)
⊢ Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) β) : Finsupp.{u_5, u_1} presM.R B)

Tactic:
apply Finsupp.induction (motive := fun β ↦ Finsupp.single r (presB.π β) ∈ _)

Premises used: Finsupp.induction
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
w : Finsupp.{u_5, u_1} presM.R B
h : r ∉ w.support
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
β : Finsupp.{u_6, u_3} presB.G A
h_1 : Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B)
⊢ Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) 0) : Finsupp.{u_5, u_1} presM.R B)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
β : Finsupp.{u_6, u_3} presB.G A
h_2 : Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B)
g : presB.G
a : A
f : Finsupp.{u_6, u_3} presB.G A
h :
  g ∉ f.support →
    a ≠ 0 →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
        Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a + f)) :
            Finsupp.{u_5, u_1} presM.R B)
⊢ g ∉ f.support →
    a ≠ 0 →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
        Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a + f)) :
            Finsupp.{u_5, u_1} presM.R B)

Tactic:
_
-- Module: Mathlib.Algebra.Module.Presentation.RestrictScalars
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
β : Finsupp.{u_6, u_3} presB.G A
h_2 : Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B)
g : presB.G
a : A
f : Finsupp.{u_6, u_3} presB.G A
h_3 : g ∉ f.support
h :
  a ≠ 0 →
    Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a + f)) : Finsupp.{u_5, u_1} presM.R B)
⊢ a ≠ 0 →
    Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
        (Submodule.span A
          (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
            HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
        (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a + f)) : Finsupp.{u_5, u_1} presM.R B)

Tactic:
_