awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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
⊢ 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
have 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}
                    (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
                    (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
              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}
                    (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
                    (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single a b + f)
Tactic: apply Finsupp.induction
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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)
have 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}
            (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
            (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
      HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
  (Finsupp.single r b)
Tactic: refine Submodule.add_mem _ ?_ hw
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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)
have 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)
Tactic: obtain ⟨β, rfl⟩ := presB.surjective_π b
Cleared hypotheses: b, h_1
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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) β) : Finsupp.{u_5, u_1} presM.R B)
have 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}
            (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
            (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
      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: apply Finsupp.induction (motive := fun β ↦ Finsupp.single r (presB.π β) ∈ _)
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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)
g : presB.G
a : A
f : Finsupp.{u_6, u_3} presB.G A
h_2 : g ∉ f.support
h_3 : a ≠ 0
hf :
  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)
have 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)))
  (HAdd.hAdd (α := Finsupp.{u_5, u_1} presM.R B) (β := Finsupp.{u_5, u_1} presM.R B)
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a)) : Finsupp.{u_5, u_1} presM.R B)
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B))
Tactic: rw [map_add, Finsupp.single_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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)
g : presB.G
a : A
f : Finsupp.{u_6, u_3} presB.G A
h_2 : g ∉ f.support
h_3 : a ≠ 0
hf :
  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 (γ := 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)))
    (HAdd.hAdd (α := Finsupp.{u_5, u_1} presM.R B) (β := Finsupp.{u_5, u_1} presM.R B)
      (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single g a)) : Finsupp.{u_5, u_1} presM.R B)
      (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B))
have 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}
            (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
            (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
      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)) : Finsupp.{u_5, u_1} presM.R B)
Tactic: refine Submodule.add_mem _ ?_ hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
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)
g : presB.G
a : A
f : Finsupp.{u_6, u_3} presB.G A
h_2 : g ∉ f.support
h_3 : a ≠ 0
hf :
  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)) : Finsupp.{u_5, u_1} presM.R B)
have 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)))
  (a • HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single r 1))
Tactic: rw [← Finsupp.smul_single_one, ← Finsupp.smul_single_one,
            map_smul, Relations.Solution.π_single, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tautological (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module A N
s : Relations.Solution (tautologicalRelations A M) N
m₁ m₂ : M
⊢ s.var (m₁ + m₂) = s.var m₁ + s.var m₂
have symm : s.var m₁ + s.var m₂ = s.var (m₁ + m₂)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tautological (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module A N
s : Relations.Solution (tautologicalRelations A M) N
m₁ m₂ : M
⊢ s.var m₁ + s.var m₂ = s.var (m₁ + m₂)
have rw : s.var m₁ + s.var m₂ - s.var (m₁ + m₂) = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tautological (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module A N
s : Relations.Solution (tautologicalRelations A M) N
a : A
m : M
⊢ s.var (a • m) = HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m)
have symm : HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) = s.var (a • m)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tautological (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module A N
s : Relations.Solution (tautologicalRelations A M) N
a : A
m : M
⊢ HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) = s.var (a • m)
have rw : HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) - s.var (a • m) = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tautological (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module A N
f f' : M →ₗ[A] N
h : Relations.Solution.postcomp (tautologicalSolution A M) f = Relations.Solution.postcomp (tautologicalSolution A M) f'
⊢ f = f'
have h₁ : ∀ (m : M), Eq.{w + 1} (α := N) ((f : (a : M) → N) m : N) ((f' : (a : M) → N) m : N)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : (relations₁.tensor relations₂).G) ↦
            match (motive := (relations₁.tensor relations₂).G → M₁ ⊗[A] M₂) x with
            | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂ :
          (a : (relations₁.tensor relations₂).G →₀ A) → M₁ ⊗[A] M₂)
        ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
have inl : Eq (α := M₁ ⊗[A] M₂)
  ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
          solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
        (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
      (Finsupp.embDomain (Function.Embedding.sectL relations₁.G g₂) (relations₁.relation r₁)) :
    M₁ ⊗[A] M₂)
  (0 : M₁ ⊗[A] M₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
            solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
          (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (Finsupp.embDomain (Function.Embedding.sectL relations₁.G g₂) (relations₁.relation r₁)) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
have inl : Eq (α := M₁ ⊗[A] M₂)
  ((Finsupp.linearCombination A
          ((fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦ solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2) ∘
            (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → relations₁.G × relations₂.G)) :
        (a : relations₁.G →₀ A) → M₁ ⊗[A] M₂)
      (relations₁.relation r₁) :
    M₁ ⊗[A] M₂)
  (0 : M₁ ⊗[A] M₂)
Tactic: rw [Finsupp.linearCombination_embDomain]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : (relations₁.tensor relations₂).G) ↦
            match (motive := (relations₁.tensor relations₂).G → M₁ ⊗[A] M₂) x with
            | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂ :
          (a : (relations₁.tensor relations₂).G →₀ A) → M₁ ⊗[A] M₂)
        ((relations₁.tensor relations₂).relation (Sum.inr (g₁, r₂))) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
have inr : Eq (α := M₁ ⊗[A] M₂)
  ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
          solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
        (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
      (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
    M₁ ⊗[A] M₂)
  (0 : M₁ ⊗[A] M₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
            solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
          (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
have inr : Eq (α := M₁ ⊗[A] M₂)
  ((Finsupp.linearCombination A
          ((fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦ solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2) ∘
            (⇑(Function.Embedding.sectR g₁ relations₂.G) : (a : relations₂.G) → relations₁.G × relations₂.G)) :
        (a : relations₂.G →₀ A) → M₁ ⊗[A] M₂)
      (relations₂.relation r₂) :
    M₁ ⊗[A] M₂)
  (0 : M₁ ⊗[A] M₂)
Tactic: rw [Finsupp.linearCombination_embDomain]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂) : (a : relations₂.G →₀ A) → N)
        (relations₂.relation r₂) :
      N)
    (0 : N)
have erw : Eq.{w + 1} (α := N)
  ((Finsupp.linearCombination A s.var : (a : relations₁.G × relations₂.G →₀ A) → N)
      (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
    N)
  (0 : N)
Tactic: erw [← Finsupp.linearCombination_embDomain A
              (Function.Embedding.sectR g₁ relations₂.G)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Tensor (goal)
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
⊢ Eq (α := relations₂.Solution N)
    (solution₂.postcomp
      ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
            h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
          (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
        (relations₁.relation r₁)))
    (solution₂.postcomp 0)
have var : ∀ (g₂ : relations₂.G),
  Eq.{w + 1} (α := N)
    (var
      (solution₂.postcomp
        ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := sorry } :
            (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
          (relations₁.relation r₁)))
      g₂)
    (var (solution₂.postcomp 0) g₂)
Tactic: ext g₂