awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
g : P.Aut
hg : g ∈ P.weylGroup
mem :
  ∀ (i : ι) (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
one :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • x) : M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have mul : ∀ (g₁ g₂ : P.Aut) (hg₁ : g₁ ∈ P.weylGroup) (hg₂ : g₂ ∈ P.weylGroup)
  (hg₁' :
    ∀ (x y : M),
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • x) :
                M →ₗ[R] R) :
              (a : M) → R)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • y) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
  (hg₂' :
    ∀ (x y : M),
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • x) :
                M →ₗ[R] R) :
              (a : M) → R)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • y) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
  (x y : M),
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) sorry • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) sorry • y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: induction hg using weylGroup.induction with
  | mem i => simp
  | one => simp
  | mul g₁ g₂ hg₁ hg₂ hg₁' hg₂' =>
    intro x y
    rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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] ↔ x - y ∈ U
have rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x - y ∈ U
Tactic: rw [SModEq.def, Submodule.Quotient.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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 : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x - y ∈ U
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U
have rw₁ : x - y ∈ U ↔ x - y ∈ U
Tactic: rw [SModEq.def, Submodule.Quotient.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ SModEq.{u_1, u_4} (R := R) ⊥ x y ↔ x = y
have rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) ⊥) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x = y
Tactic: rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) ⊥) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x = y
⊢ SModEq.{u_1, u_4} (R := R) ⊥ x y ↔ x = y
have rw₁ : Membership.mem (γ := Submodule R M) ⊥ (x - y) ↔ x = y
Tactic: rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) ⊥) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x = y
rw₁ : Membership.mem (γ := Submodule R M) ⊥ (x - y) ↔ x = y
⊢ SModEq.{u_1, u_4} (R := R) ⊥ x y ↔ x = y
have rw₂ : x - y = 0 ↔ x = y
Tactic: rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) ⊥) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x = y
rw₁ : Membership.mem (γ := Submodule R M) ⊥ (x - y) ↔ x = y
rw₂ : x - y = 0 ↔ x = y
⊢ SModEq.{u_1, u_4} (R := R) ⊥ x y ↔ x = y
have rw₃ : x = y ↔ x = y
Tactic: rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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 [SMOD U]
⊢ x ≡ y [SMOD V]
have simp : ∀ (hxy : x - y ∈ U), x - y ∈ V
Tactic: simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (hypothesis)
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]
⊢ x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
have hxy₃ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
Tactic: rw [SModEq.def] at hxy₁ hxy₂ ⊢
Cleared hypotheses: hxy₁, hxy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (hypothesis)
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₁)
⊢ x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
have hxy₄ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
Tactic: rw [SModEq.def] at hxy₁ hxy₂ ⊢
Cleared hypotheses: hxy₁, hxy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ + x₂)) (Submodule.Quotient.mk (y₁ + y₂))
have 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₂)
Tactic: simp_rw [Quotient.mk_add, hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ + x₂)) (Submodule.Quotient.mk (y₁ + y₂))
have 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₂)
Tactic: simp_rw [Quotient.mk_add, hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
have cons : x i + ∑ x_1 ∈ s, x x_1 ≡ ∑ 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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
have cons₁ : x i + ∑ x_1 ∈ s, x x_1 ≡ y i + ∑ x ∈ s, y x [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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
have cons₂ : y i + ∑ x_1 ∈ s, x x_1 ≡ y i + ∑ x ∈ s, y x [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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ Finset.cons i s h, x i ≡ ∑ i ∈ Finset.cons i s h, y i [SMOD U]
have cons₃ : y i + ∑ i ∈ s, y i ≡ y i + ∑ i ∈ s, 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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
have empty : ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ≡ y i [SMOD U]), ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, 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))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
have 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]
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))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
have empty : ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ≡ y i [SMOD U]), ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, 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))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
have 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]
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))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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
⊢ c • x ≡ c • y [SMOD U]
have 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))
Tactic: rw [SModEq.def] at hxy ⊢
Cleared hypotheses: hxy, c
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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 : ℕ
⊢ n • x ≡ n • y [SMOD U]
have 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))
Tactic: rw [SModEq.def] at hxy ⊢
Cleared hypotheses: hxy, n
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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 : ℤ
⊢ n • x ≡ n • y [SMOD U]
have 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))
Tactic: rw [SModEq.def] at hxy ⊢
Cleared hypotheses: hxy, n
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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₂
⊢ SModEq (R := A) I (x₁ * x₂) (y₁ * y₂)
have 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)
Tactic: simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
Cleared hypotheses: hxy₁, hxy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have cons : SModEq (R := A) I (x i * ∏ x_1 ∈ s, x x_1) (∏ 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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have cons₁ : SModEq (R := A) I (x i * ∏ x_1 ∈ s, x x_1) (y i * ∏ x ∈ s, y x)
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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have cons₂ : SModEq (R := A) I (y i * ∏ x_1 ∈ s, x x_1) (y i * ∏ x ∈ s, y x)
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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ 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)
have cons₃ : SModEq (R := A) I (y i * ∏ i ∈ s, y i) (y i * ∏ i ∈ s, 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))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)
have 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)
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))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
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)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)
have 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)
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))]
Cleared hypotheses: s, hxy