awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module S M
U : Submodule R M
V : Submodule S M
h : U.toAddSubgroup ≤ V.toAddSubgroup
x y : M
hxy : x - y ∈ U
⊢ x - y ∈ V

Tactic:
h hxy

Premises used: Set.Mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module S M
U : Submodule R M
V : Submodule S M
h : U.toAddSubgroup ≤ V.toAddSubgroup
x y : M
hxy : x - y ∈ U
⊢ x - y ∈ V

Tactic:
exact h hxy
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
⊢ x ≡ x [SMOD U]

Tactic:
@rfl _ _

Premises used: SModEq, rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
⊢ x ≡ x [SMOD U]

Tactic:
SModEq.refl _

Premises used: SModEq.refl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
A : Type u_3
inst_2 : CommRing A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_5
inst_6 : AddCommGroup N
inst_7 : Module R N
V V₁ V₂ : Submodule R N
⊢ Std.Refl (SModEq U)

Tactic:
⟨SModEq.refl⟩

Premises used: Std.Refl.mk, SModEq.refl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
⊢ y ≡ x [SMOD U]

Tactic:
hxy.symm

Premises used: Eq.symm, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x ≡ y [SMOD U] ↔ y ≡ x [SMOD U]

Tactic:
⟨symm, symm⟩

Premises used: SModEq.symm, Iff.intro
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y z : M
hxy : x ≡ y [SMOD U]
hyz : y ≡ z [SMOD U]
⊢ x ≡ z [SMOD U]

Tactic:
hxy.trans hyz

Premises used: SModEq, Eq.trans
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)

Tactic:
rw [SModEq.def] at hxy₁ hxy₂ ⊢

Premises used: SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
hxy₃ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)

Tactic:
rw [SModEq.def] at hxy₁ hxy₂ ⊢

Premises used: SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
hxy₂ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
simp_rw :
  HAdd.hAdd (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk x₂) =
    HAdd.hAdd (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
simp_rw₁ :
  HAdd.hAdd (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk x₂) =
    HAdd.hAdd (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ + x₂)) (Submodule.Quotient.mk (y₁ + y₂))

Tactic:
simp_rw [Quotient.mk_add, hxy₁, hxy₂]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ≡ y i [SMOD U]
⊢ ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, y i [SMOD U]

Tactic:
simp [SModEq.rfl]

Premises used: SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h : i ∉ s
ih : ∀ (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]), ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h, x i_1 ≡ y i_1 [SMOD U]
cons : x i + ∑ x_1 ∈ s, x x_1 ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
cons₁ : x i + ∑ x_1 ∈ s, x x_1 ≡ y i + ∑ x ∈ s, y x [SMOD U]
cons₂ : y i + ∑ x_1 ∈ s, x x_1 ≡ y i + ∑ x ∈ s, y x [SMOD U]
cons₃ cons₄ : y i + ∑ i ∈ s, y i ≡ y i + ∑ i ∈ s, y i [SMOD U]
⊢ ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]

Tactic:
grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.mem_cons_of_mem, Finset.sum_cons, Finset.mem_cons_self
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
ι : Type u_6
s : Finset ι
x y : ι → M
hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]
empty :
  ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ≡ y i [SMOD U]), ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, y i [SMOD U]
cons :
  ∀ (i : ι) (s : Finset ι) (h : i ∉ s)
    (ih : ∀ (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]), ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U])
    (hxy : ∀ i_1 ∈ Finset.cons i s h, x i_1 ≡ y i_1 [SMOD U]),
    ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]

Tactic:
induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.sum_cons, SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
ι : Type u_6
s : Finset ι
x y : ι → M
hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]
empty :
  ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ≡ y i [SMOD U]), ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, y i [SMOD U]
cons :
  ∀ (i : ι) (s : Finset ι) (h : i ∉ s)
    (ih : ∀ (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]), ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U])
    (hxy : ∀ i_1 ∈ Finset.cons i s h, x i_1 ≡ y i_1 [SMOD U]),
    ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]

Tactic:
classical
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.sum_cons, SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
c : R
rw :
  ∀ (hxy : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)) (c : R),
    Eq (α := M ⧸ U) (Submodule.Quotient.mk (c • x)) (Submodule.Quotient.mk (c • y))
⊢ c • x ≡ c • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Premises used: SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
n : ℕ
rw :
  ∀ (hxy : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)) (n : ℕ),
    Eq (α := M ⧸ U) (Submodule.Quotient.mk (n • x)) (Submodule.Quotient.mk (n • y))
⊢ n • x ≡ n • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Premises used: SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
n : ℤ
rw :
  ∀ (hxy : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)) (n : ℤ),
    Eq (α := M ⧸ U) (Submodule.Quotient.mk (n • x)) (Submodule.Quotient.mk (n • y))
⊢ n • x ≡ n • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Premises used: SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : SModEq (R := A) I x₁ y₁
hxy₂ : SModEq (R := A) I x₂ y₂
simp :
  ∀
    (hxy₁ :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₁ : A ⧸ I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I))
    (hxy₂ :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₂ : A ⧸ I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)),
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₁ : A ⧸ I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₂ : A ⧸ I) =
      HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)
⊢ SModEq (R := A) I (x₁ * x₂) (y₁ * y₂)

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢

Premises used: SModEq.def, map_mul, Ideal.Quotient.mk_eq_mk
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ :
  Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₁ : A ⧸ I)
    ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
hxy₂ :
  Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₂ : A ⧸ I)
    ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)
rw :
  HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₂ : A ⧸ I) =
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)
rw₁ rw₂ :
  HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I) =
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)
⊢ HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x₂ : A ⧸ I) =
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₁ : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y₂ : A ⧸ I)

Tactic:
rw [hxy₁, hxy₂]
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → SModEq (R := A) I (x i) (y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ ∅, x i) (∏ i ∈ ∅, y i)

Tactic:
simp [SModEq.rfl]

Premises used: SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h : i ∉ s
ih :
  ∀ (hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)), SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)
hxy : ∀ i_1 ∈ Finset.cons i s h, SModEq (R := A) I (x i_1) (y i_1)
cons : SModEq (R := A) I (x i * ∏ x_1 ∈ s, x x_1) (∏ i ∈ Finset.cons i s h, y i)
cons₁ : SModEq (R := A) I (x i * ∏ x_1 ∈ s, x x_1) (y i * ∏ x ∈ s, y x)
cons₂ : SModEq (R := A) I (y i * ∏ x_1 ∈ s, x x_1) (y i * ∏ x ∈ s, y x)
cons₃ cons₄ : SModEq (R := A) I (y i * ∏ i ∈ s, y i) (y i * ∏ i ∈ s, y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ Finset.cons i s h, x i) (∏ i ∈ Finset.cons i s h, y i)

Tactic:
grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.mem_cons_of_mem, Finset.prod_cons, Finset.mem_cons_self
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
s : Finset ι
x y : ι → A
hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)
empty :
  ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → SModEq (R := A) I (x i) (y i)),
    SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ ∅, x i) (∏ i ∈ ∅, y i)
cons :
  ∀ (i : ι) (s : Finset ι) (h : i ∉ s)
    (ih :
      ∀ (hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)),
        SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i))
    (hxy : ∀ i_1 ∈ Finset.cons i s h, SModEq (R := A) I (x i_1) (y i_1)),
    SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ Finset.cons i s h, x i) (∏ i ∈ Finset.cons i s h, y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.prod_cons, SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
s : Finset ι
x y : ι → A
hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)
empty :
  ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → SModEq (R := A) I (x i) (y i)),
    SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ ∅, x i) (∏ i ∈ ∅, y i)
cons :
  ∀ (i : ι) (s : Finset ι) (h : i ∉ s)
    (ih :
      ∀ (hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)),
        SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i))
    (hxy : ∀ i_1 ∈ Finset.cons i s h, SModEq (R := A) I (x i_1) (y i_1)),
    SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ Finset.cons i s h, x i) (∏ i ∈ Finset.cons i s h, y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)

Tactic:
classical
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

Premises used: Finset.prod_cons, SModEq.rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : SModEq (R := A) I x y
simp :
  ∀
    (hxy :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I)),
    HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) n =
      HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n
⊢ SModEq (R := A) I (x ^ n) (y ^ n)

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢

Premises used: SModEq.def, map_pow, Ideal.Quotient.mk_eq_mk
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy :
  Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I)
    ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I)
rw rw₁ :
  HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n =
    HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n
⊢ HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) n =
    HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n

Tactic:
rw [hxy]
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
⊢ -x ≡ -y [SMOD U]

Tactic:
simpa only [SModEq.def, Quotient.mk_neg, neg_inj]

Premises used: SModEq.def, neg_inj, Submodule.Quotient.mk_neg
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
hxy₂ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
simp_rw :
  HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk x₂) =
    HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
simp_rw₁ :
  HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk x₂) =
    HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ - x₂)) (Submodule.Quotient.mk (y₁ - y₂))

Tactic:
simp_rw [Quotient.mk_sub, hxy₁, hxy₂]

Premises used: Submodule.Quotient.mk_sub
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk 0) ↔ x ∈ U
rw₁ : x - 0 ∈ U ↔ x ∈ U
rw₂ rw₃ : x ∈ U ↔ x ∈ U
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U

Tactic:
rw [SModEq.def, Submodule.Quotient.eq, sub_zero]

Premises used: Submodule.Quotient.eq, sub_zero, SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

Tactic:
simp only [SModEq.sub_mem, sub_zero]

Premises used: sub_zero, SModEq.sub_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
hxy : x ≡ y [SMOD U]
f : M →ₗ[R] N
⊢ (f : (a : M) → N) x ≡ (f : (a : M) → N) y [SMOD Submodule.map f U]

Tactic:
(Submodule.Quotient.eq _).2 <| f.map_sub x y ▸ mem_map_of_mem <| (Submodule.Quotient.eq _).1 hxy

Premises used: Submodule.Quotient.eq, Iff.mpr, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
V : Submodule R N
f : M →ₗ[R] N
hxy : (f : (a : M) → N) x ≡ (f : (a : M) → N) y [SMOD V]
⊢ x ≡ y [SMOD Submodule.comap f V]

Tactic:
(Submodule.Quotient.eq _).2 <|
    show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy

Premises used: Submodule.Quotient.eq, Iff.mpr, Eq.rec, Iff.mp, LinearMap.map_sub, Eq.symm, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_6
inst : CommRing R
I : Ideal R
x y : R
h : SModEq (R := R) I x y
f : R[X]
simp_rw :
  SModEq.{u_6, u_6} (R := R) (M := R) I (∑ x_1 ∈ f.support, f.coeff x_1 * x ^ x_1) (∑ x ∈ f.support, f.coeff x * y ^ x)
⊢ SModEq (R := R) I (Polynomial.eval x f) (Polynomial.eval y f)

Tactic:
simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]

Premises used: Polynomial.sum, Polynomial.eval_eq_sum
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_6
inst : CommRing R
I : Ideal R
x y : R
h : SModEq (R := R) I x y
f : R[X]
⊢ SModEq.{u_6, u_6} (R := R) (M := R) I (∑ x_1 ∈ f.support, f.coeff x_1 * x ^ x_1) (∑ x ∈ f.support, f.coeff x * y ^ x)

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module S M
U : Submodule R M
x y : M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
⊢ x ≡ y [SMOD Submodule.restrictScalars S U] ↔ x ≡ y [SMOD U]

Tactic:
simp [SModEq.sub_mem]

Premises used: SModEq.sub_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_6
inst : CommRing R
I : Ideal R
x y : R
⊢ SModEq (R := R) I x y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
Iff.rfl

Premises used: Submodule.Quotient.mk, Iff.rfl, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
rw : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x ≡ y [SMOD U]

Tactic:
rw [SModEq.sub_mem]

Premises used: SModEq.sub_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
refine_1 : ∀ (h : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)), x - y ∈ U
refine_2 : ∀ (h : x - y ∈ U), x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)
⊢ (↑U : Set M) ⊆ (y - x) +ᵥ (↑U : Set M)

Tactic:
rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub] at h

Premises used: vadd_vadd, neg_add_eq_sub, Set.vadd_set_subset_iff_subset_neg_vadd_set
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : (↑U : Set M) ⊆ (y - x) +ᵥ (↑U : Set M)
⊢ x - y ∈ U

Tactic:
simpa [Set.mem_vadd_set_iff_neg_vadd_mem] using h U.zero_mem

Premises used: Submodule.zero_mem, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
refine_2 : (↑U : Set M) ⊆ (y - x) +ᵥ (↑U : Set M)
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)

Tactic:
rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub]

Premises used: vadd_vadd, neg_add_eq_sub, Set.vadd_set_subset_iff_subset_neg_vadd_set
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
z : M
hz : z ∈ (↑U : Set M)
⊢ z ∈ (y - x) +ᵥ (↑U : Set M)

Tactic:
simpa [Set.mem_vadd_set_iff_neg_vadd_mem] using U.add_mem h hz

Premises used: Set.mem_vadd_set_iff_neg_vadd_mem, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x +ᵥ (↑U : Set M) = y +ᵥ (↑U : Set M) ↔ x ≡ y [SMOD U]

Tactic:
⟨fun h ↦ Submodule.vadd_set_subset_vadd_set_iff.mp h.subset,
    fun h ↦ Set.Subset.antisymm (Submodule.vadd_set_subset_vadd_set_iff.mpr h)
      (Submodule.vadd_set_subset_vadd_set_iff.mpr h.symm)⟩

Premises used: Set.Subset.antisymm, Iff.mpr, SModEq.symm, Eq.subset, Iff.intro, Iff.mp, Submodule.vadd_set_subset_vadd_set_iff
-- Module: Mathlib.LinearAlgebra.SModEq.Pointwise
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
c : R
hc : c ∈ I
rw : ∀ (hxy : x - y ∈ U) {c : R} (hc : c ∈ I), c • x - c • y ∈ I • U
⊢ c • x ≡ c • y [SMOD I • U]

Tactic:
rw [SModEq.sub_mem] at hxy ⊢

Premises used: SModEq.sub_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Pointwise
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
rw : c • (x - y) ∈ I • U
⊢ c • x - c • y ∈ I • U

Tactic:
rw [← smul_sub]

Premises used: smul_sub
-- Module: Mathlib.LinearAlgebra.SModEq.Pointwise
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • (x - y) ∈ I • U

Tactic:
smul_mem_smul hc hxy

Premises used: Set.Mem, Submodule.smul_mem_smul
-- Module: Mathlib.LinearAlgebra.SModEq.Pointwise
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • (x - y) ∈ I • U

Tactic:
exact smul_mem_smul hc hxy

Premises used: Submodule.smul_mem_smul