awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_4 : 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)
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))
⊢ 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:
rw [map_add, Finsupp.single_add]

Premises used: map_add, Finsupp.single_add
-- 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)
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))

Tactic:
Submodule.add_mem _ ?_ hf

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
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_4 : 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)
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) (Finsupp.single g a)) : 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))

Tactic:
refine Submodule.add_mem _ ?_ hf

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
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_4 : 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)
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))
⊢ 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)

Tactic:
rw [← Finsupp.smul_single_one, ← Finsupp.smul_single_one,
            map_smul, Relations.Solution.π_single, smul_assoc]

Premises used: smul_assoc, Finsupp.smul_single_one, Module.Relations.Solution.π_single, map_smul
-- 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)
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)))
    (a • HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single r 1))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span ⟨⟨g, r⟩, rfl⟩)

Premises used: Set.Mem, Prod.mk, Exists.intro, Submodule.subset_span, rfl, Submodule.smul_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
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)))
    (a • HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single r 1))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨⟨g, r⟩, rfl⟩)
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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
symm : s.var m₁ + s.var m₂ = s.var (m₁ + m₂)
⊢ s.var (m₁ + m₂) = s.var m₁ + s.var m₂

Tactic:
symm
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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
rw : s.var m₁ + s.var m₂ - s.var (m₁ + m₂) = 0
⊢ s.var m₁ + s.var m₂ = s.var (m₁ + m₂)

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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₂) = 0

Tactic:
simpa using s.linearCombination_var_relation (.add m₁ m₂)

Premises used: Module.Presentation.tautological.R.add, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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
symm : HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) = s.var (a • m)
⊢ s.var (a • m) = HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m)

Tactic:
symm
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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
rw : HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) - s.var (a • m) = 0
⊢ HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (s.var m) = s.var (a • m)

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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) = 0

Tactic:
simpa using s.linearCombination_var_relation (.smul a m)

Premises used: Module.Presentation.tautological.R.smul, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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 : M →ₗ[A] N
m₁ m₂ : M
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A (⇑f : (a : M) → N) : (a : (tautologicalRelations A M).G →₀ A) → N)
        (Relations.relation (tautologicalRelations A M) (tautological.R.add m₁ m₂)) :
      N)
    (0 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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 : M →ₗ[A] N
a : A
m : M
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A (⇑f : (a : M) → N) : (a : (tautologicalRelations A M).G →₀ A) → N)
        (Relations.relation (tautologicalRelations A M) (tautological.R.smul a m)) :
      N)
    (0 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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'
h₁ : ∀ (m : M), Eq.{w + 1} (α := N) ((f : (a : M) → N) m : N) ((f' : (a : M) → N) m : N)
⊢ f = f'

Tactic:
ext m
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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'
m : M
⊢ Eq.{w + 1} (α := N) ((f : (a : M) → N) m : N) ((f' : (a : M) → N) m : N)

Tactic:
Relations.Solution.congr_var h m

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
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'
m : M
⊢ Eq.{w + 1} (α := N) ((f : (a : M) → N) m : N) ((f' : (a : M) → N) m : N)

Tactic:
exact Relations.Solution.congr_var h m

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Tautological
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
⊢ Relations.Solution.IsPresentation (relations := tautologicalRelations A M) (tautologicalSolution A M)

Tactic:
(tautologicalSolutionIsPresentationCore A M).isPresentation

Premises used: Module.Presentation.tautologicalSolutionIsPresentationCore, Module.Relations.Solution.IsPresentationCore.isPresentation
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
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₂)
⊢ 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₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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
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₂)
⊢ 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:
rw [Finsupp.linearCombination_embDomain]

Premises used: Finsupp.linearCombination_embDomain
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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) ∘
              (⇑(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:
(solution₁.postcomp (curry (TensorProduct.comm A M₂ M₁).toLinearMap
        (solution₂.var g₂))).linearCombination_var_relation r₁

Premises used: TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, List.foldl, LinearEquiv.toLinearMap, TensorProduct.tmul, TensorProduct.curry, Module.Relations.Solution.postcomp, DFunLike.coe, AddCon.toQuotient, FreeAddMonoid.sumAux, Module.Relations.Solution.linearCombination_var_relation, Module.Relations.Solution.var
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
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) ∘
              (⇑(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:
exact (solution₁.postcomp (curry (TensorProduct.comm A M₂ M₁).toLinearMap
        (solution₂.var g₂))).linearCombination_var_relation r₁

Premises used: TensorProduct.comm, LinearEquiv.toLinearMap, TensorProduct.curry, Module.Relations.Solution.postcomp, DFunLike.coe, Module.Relations.Solution.linearCombination_var_relation, Module.Relations.Solution.var