awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin 0),
      Eq (α := R)
        (((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin 0) → R)
            a :
          R)
        ((0.1 : (a : Fin 0) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin 0 →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 0 → R) → Fin 0 →₀ R) fun (x : Fin 0) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ ∀ (i : ι),
    Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))
      (Submodule.Quotient.mk (HSMul.hSMul (β := R) x 1)) 0

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin (m + 1)),
      Eq (α := R)
        (((HSMul.hSMul (β :=
                  (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                      fun (x : Fin (m + 1)) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin (m + 1)) → R)
            a :
          R)
        ((0.1 : (a : Fin (m + 1)) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                    fun (x : Fin (m + 1)) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ x = 0

Tactic:
simpa using h.1 0

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin (m + 1)),
      Eq (α := R)
        (((HSMul.hSMul (β :=
                  (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                      fun (x : Fin (m + 1)) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin (m + 1)) → R)
            a :
          R)
        ((0.1 : (a : Fin (m + 1)) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                    fun (x : Fin (m + 1)) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
succ : Membership.mem (γ := Submodule R R) (annihilator R M) 0
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) x

Tactic:
rw [show x = 0 by simpa using h.1 0]
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin (m + 1)),
      Eq (α := R)
        (((HSMul.hSMul (β :=
                  (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                      fun (x : Fin (m + 1)) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin (m + 1)) → R)
            a :
          R)
        ((0.1 : (a : Fin (m + 1)) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                    fun (x : Fin (m + 1)) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin (m + 1)),
      Eq (α := R)
        (((HSMul.hSMul (β :=
                  (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                      fun (x : Fin (m + 1)) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin (m + 1)) → R)
            a :
          R)
        ((0.1 : (a : Fin (m + 1)) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                    fun (x : Fin (m + 1)) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_3
y : PUnit
r : R
⊢ r • y = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
⊢ IsCentralScalar R PUnit

Tactic:
⟨fun _ _ => rfl⟩

Premises used: IsCentralScalar.mk, rfl
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
⊢ SMulCommClass R S PUnit

Tactic:
⟨fun _ _ _ => rfl⟩

Premises used: SMulCommClass.mk, rfl
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
⊢ IsScalarTower R S PUnit

Tactic:
⟨fun _ _ _ => rfl⟩

Premises used: IsScalarTower.mk, rfl
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Zero R
⊢ ∀ (a : R), HSMul.hSMul (β := PUnit) a 0 = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Zero R
⊢ ∀ (m : PUnit.{u_3 + 1}), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 m = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (x y : R) (b : PUnit.{u_3 + 1}), (x * y) • b = x • y • b

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (b : PUnit.{u_3 + 1}), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = b

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (a : R), HSMul.hSMul (β := PUnit) a 0 = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (a : R) (x y : PUnit.{u_3 + 1}), a • (x + y) = a • x + a • y

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (r : R), HSMul.hSMul (β := PUnit) r 1 = 1

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
⊢ ∀ (r : R) (x y : PUnit.{u_3 + 1}), r • (x * y) = r • x * r • y

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
⊢ ∀ (r s : R) (x : PUnit.{u_3 + 1}), (r + s) • x = r • x + s • x

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
⊢ ∀ (x : PUnit.{u_3 + 1}), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
r : PUnit
a : R
⊢ r • a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
⊢ ∀ (m : PUnit.{u_3 + 1}) (n : R) (a : S), m • n • a = n • m • a

Tactic:
simp
-- Module: Mathlib.Algebra.Module.PUnit
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
⊢ ∀ (x : PUnit.{u_3 + 1}) (y : R) (z : S), (x • y) • z = x • y • z

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Pi
Goal:
I : Type u
f : I → Type v
α : Type u_1
inst : (i : I) → SMul.{u_1, v} α (f i)
k : α
hk : ∀ (i : I), IsSMulRegular.{u_1, v} (f i) k
⊢ IsSMulRegular ((i : I) → f i) k

Tactic:
fun _ _ h =>
  funext fun i => hk i (congr_fun h i :)

Premises used: funext, IsSMulRegular, Function.Injective, congr_fun
-- Module: Mathlib.Algebra.Module.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
r_1 s : (i : I) → f i
x : (i : I) → g i
h : ∀ (x_1 : I), ((r_1 + s) • x) x_1 = (r_1 • x + s • x) x_1
⊢ (r_1 + s) • x = r_1 • x + s • x

Tactic:
ext1
-- Module: Mathlib.Algebra.Module.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
r_1 s : (i : I) → f i
x : (i : I) → g i
x_1 : I
⊢ ((r_1 + s) • x) x_1 = (r_1 • x + s • x) x_1

Tactic:
apply add_smul

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
x : (i : I) → g i
h : ∀ (x_1 : I), HSMul.hSMul (α := (i : I) → f i) 0 x x_1 = 0 x_1
⊢ HSMul.hSMul (α := (i : I) → f i) 0 x = 0

Tactic:
ext1
-- Module: Mathlib.Algebra.Module.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
x : (i : I) → g i
x_1 : I
h h₁ : Eq.{u_1 + 1} (α := g x_1) (0 x_1) (0 x_1)
⊢ HSMul.hSMul (α := (i : I) → f i) 0 x x_1 = 0 x_1

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Module.PointwisePi
Goal:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : (i : ι) → SMul.{u_1, u_3} K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
⊢ r • s.pi (α := R) t ⊆ s.pi (α := R) (r • t)

Tactic:
piMap_image_pi_subset _

Premises used: Pi.map, Set.piMap_image_pi_subset
-- Module: Mathlib.Algebra.Module.PointwisePi
Goal:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : (i : ι) → SMul.{u_1, u_3} K (R i)
r : K
t : (i : ι) → Set (R i)
⊢ r • pi (α := R) univ t = pi (α := R) univ (r • t)

Tactic:
piMap_image_univ_pi _ _

Premises used: Set.piMap_image_univ_pi, Pi.map
-- Module: Mathlib.Algebra.Module.PointwisePi
Goal:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : Group K
inst_1 : (i : ι) → MulAction.{u_1, u_3} K (R i)
r : K
S : Set ι
t : (i : ι) → Set (R i)
⊢ r • S.pi (α := R) t = S.pi (α := R) (r • t)

Tactic:
piMap_image_pi (fun _ _ => MulAction.surjective _) _

Premises used: Pi.map, Set.piMap_image_pi, MulAction.surjective
-- Module: Mathlib.Algebra.Module.PointwisePi
Goal:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : GroupWithZero K
inst_1 : (i : ι) → MulAction.{u_1, u_3} K (R i)
r : K
S : Set ι
t : (i : ι) → Set (R i)
hr : r ≠ 0
⊢ r • S.pi (α := R) t = S.pi (α := R) (r • t)

Tactic:
smul_pi (Units.mk0 r hr) S t

Premises used: Units.mk0, smul_pi
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
f f' : relations.Quotient →ₗ[A] M
h :
  ∀ (g : relations.G),
    Eq.{v + 1} (α := M)
      ((f : (a : relations.Quotient) → M)
          ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
            relations.Quotient) :
        M)
      ((f' : (a : relations.Quotient) → M)
          ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
            relations.Quotient) :
        M)
⊢ f = f'

Tactic:
Submodule.linearMap_qext _ (Finsupp.lhom_ext' (fun g ↦ LinearMap.ext_ring (h g)))

Premises used: Module.Relations.Quotient, Finsupp.lhom_ext', Submodule.linearMap_qext, LinearMap.ext_ring
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ Function.Surjective (α := Finsupp.{w₀, u} relations.G A) (β := relations.Quotient)
    (⇑relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient)

Tactic:
Submodule.mkQ_surjective _

Premises used: Module.Relations.Quotient, Submodule.mkQ_surjective
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ relations.toQuotient.ker = Submodule.span A (Set.range relations.relation)

Tactic:
Submodule.ker_mkQ _

Premises used: Module.Relations.Quotient, Module.Relations.toQuotient, Submodule.ker_mkQ
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
r : relations.R
rw :
  Membership.mem (γ := Submodule A (Finsupp.{w₀, u} relations.G A)) (Submodule.span A (Set.range relations.relation))
    (relations.relation r)
⊢ Eq (α :=
    HasQuotient.Quotient (Finsupp.{w₀, u} relations.G A) (B := Submodule A (Finsupp.{w₀, u} relations.G A))
      (Submodule.span A (Set.range relations.relation)))
    ((Submodule.mkQ (Submodule.span A (Set.range relations.relation)) :
          (a : relations.G →₀ A) → (relations.G →₀ A) ⧸ Submodule.span A (Set.range relations.relation))
        (relations.relation r) :
      HasQuotient.Quotient (Finsupp.{w₀, u} relations.G A) (B := Submodule A (Finsupp.{w₀, u} relations.G A))
        (Submodule.span A (Set.range relations.relation)))
    (0 : relations.Quotient)

Tactic:
rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Premises used: Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
r : relations.R
⊢ relations.relation r ∈ Set.range relations.relation

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
r : relations.R
⊢ Membership.mem (γ := Submodule A (Finsupp.{w₀, u} relations.G A)) (Submodule.span A (Set.range relations.relation))
    (relations.relation r)

Tactic:
exact Submodule.subset_span (by simp)

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
r : relations.R
⊢ (relations.map : (a : relations.R →₀ A) → relations.G →₀ A) (Finsupp.single r 1) = relations.relation r

Tactic:
simp [map]

Premises used: Module.Relations.map
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ relations.map.range = Submodule.span A (Set.range relations.relation)

Tactic:
Finsupp.range_linearCombination _

Premises used: Finsupp.range_linearCombination, Module.Relations.map
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ relations.toQuotient ∘ₗ relations.map = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
x : Finsupp.{w₁, u} relations.R A
⊢ Eq (α := relations.Quotient)
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient)
        ((relations.map : (a : relations.R →₀ A) → relations.G →₀ A) x) :
      relations.Quotient)
    (0 : relations.Quotient)

Tactic:
DFunLike.congr_fun relations.toQuotient_map x

Premises used: DFunLike.congr_fun, Submodule.Quotient.mk, Module.Relations.toQuotient_map
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
g : relations.G
⊢ (solution.π : (a : relations.G →₀ A) → M) (Finsupp.single g 1) = solution.var g

Tactic:
simp [π]

Premises used: Module.Relations.Solution.π
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
r : relations.R
⊢ Eq.{v + 1} (α := M) ((solution.π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)

Tactic:
solution.linearCombination_var_relation r

Premises used: Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
⊢ solution.π ∘ₗ relations.map = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
x : Finsupp.{w₁, u} relations.R A
change : Eq.{v + 1} (α := M) ((solution.π ∘ₗ relations.map : (a : relations.R →₀ A) → M) x : M) (0 : M)
⊢ Eq.{v + 1} (α := M)
    ((solution.π : (a : relations.G →₀ A) → M)
        ((relations.map : (a : relations.R →₀ A) → relations.G →₀ A) x : Finsupp.{w₀, u} relations.G A) :
      M)
    (0 : M)

Tactic:
change solution.π.comp relations.map x = 0

Premises used: LinearMap.comp, Module.Relations.map, Module.Relations.Solution.π, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
x : Finsupp.{w₁, u} relations.R A
rw : Eq.{v + 1} (α := M) ((0 : (a : relations.R →₀ A) → M) x : M) (0 : M)
rw₁ rw₂ : Eq.{v + 1} (α := M) 0 0
⊢ Eq.{v + 1} (α := M) ((solution.π ∘ₗ relations.map : (a : relations.R →₀ A) → M) x : M) (0 : M)

Tactic:
rw [π_comp_map, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, Module.Relations.Solution.π_comp_map
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
⊢ solution.π.range = Submodule.span A (Set.range solution.var)

Tactic:
Finsupp.range_linearCombination _

Premises used: Finsupp.range_linearCombination, Module.Relations.Solution.π
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
rw : Set.range relations.relation ⊆ (↑solution.π.ker : Set (relations.G →₀ A))
⊢ Submodule.span A (Set.range relations.relation) ≤ solution.π.ker

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
r : relations.R
⊢ relations.relation r ∈ (↑solution.π.ker : Set (relations.G →₀ A))

Tactic:
simp only [SetLike.mem_coe, LinearMap.mem_ker, π_relation]

Premises used: LinearMap.mem_ker, SetLike.mem_coe, Module.Relations.Solution.π_relation