awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
h : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i) + pOrder hM (s i)) • s i = 0
h₁ : (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) * p ^ pOrder hM (s i)) • s i = 0
h₂ : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) • p ^ pOrder hM (s i) • s i = 0
h₃ : HSMul.hSMul (β := M) (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i))) 0 = 0
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have h₄ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
⊢ Eq (α := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
    (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
      Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
    (Submodule.span R
        (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))) :
      Submodule R (HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)))
have h : ∀ (x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)),
  Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
        Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      x ↔
    Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (Submodule.span R
        (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)
⊢ Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
        Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      x ↔
    Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (Submodule.span R
        (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))))
      x
have h : a • x = 0 ↔
  ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      x
Tactic: rw [mem_torsionBy_iff, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)
⊢ a • x = 0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        x
have h : ∀ (x : R),
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
Tactic: obtain ⟨x, rfl⟩ := mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0 →
  ∃ (a_2 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_2
        ((mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 →
    ∃ (a_2 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_2
          ((mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) x
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h₁ : (∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x) →
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h₁ : ∃ (a_1 : R), a_1 • (a * b) = a • x
Tactic: rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h : ∃ (a_1 : R), a_1 • (a * b) = a • x
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h₁ : ∀ (c : R) (h : c • (a * b) = a • x),
  ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
Tactic: obtain ⟨c, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c • (a * b) = a • x
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h₁ : c * b = x
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
      mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
have h₁ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
  (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
Tactic: use c
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
have h₁ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
  (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
Tactic: rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
have h₂ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk b) =
  (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
Tactic: rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₂ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk b) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
have h₃ : Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c • b))
  ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
Tactic: rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₂ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk b) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₃ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c • b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
have h₄ : Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c * b))
  ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
Tactic: rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₂ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk b) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₃ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c • b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
h₄ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c * b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
have h₅ : Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b))
  ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b) : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
  ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b) : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
Tactic: rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₁ : ∀ (c : R)
  (h :
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x),
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
Tactic: obtain ⟨c, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₁ : a •
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
  0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
h₁ :
  a •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₂ : c •
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
  0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
h₁ :
  a •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₂ :
  c •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₃ : c • HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a (Submodule.Quotient.mk b) = 0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
h₁ :
  a •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₂ :
  c •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₃ : c • HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a (Submodule.Quotient.mk b) = 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₄ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk (a • b)) = 0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
h₁ :
  a •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₂ :
  c •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₃ : c • HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a (Submodule.Quotient.mk b) = 0
h₄ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk (a • b)) = 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
have h₅ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c 0 = 0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]