awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
i : ι
⊢ ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
have obtain : ∀ (x : M) (hxp : x ∈ p) (hx₀ : Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)),
  ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
Tactic: obtain ⟨x, hxp, hx₀⟩ := h i
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
⊢ ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
have h₁ : ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
Tactic: replace h (i : ι) : ∃ x : p, f' i x ≠ 0 := by obtain ⟨x, hxp, hx₀⟩ := h i; exact ⟨⟨x, hxp⟩, hx₀⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
h : ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
⊢ ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
have obtain : ∀ (x : M) (hxp : x ∈ p)
  (hx₀ :
    ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hxp) : K) (0 : K)),
  ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
Tactic: obtain ⟨⟨x, hxp⟩, hx₀⟩ := exists_forall_ne_zero_of_forall_exists f' h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ ∃ (f : Dual K M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f : (a : M) → K) (v i) : K) (0 : K)
have refine : ∀ (i : ι),
  ∃ (x : Dual K M),
    Ne.{u_2 + 1} (α := K)
      (((fun (i : ι) ↦ ((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M))) i :
            (a : Dual K M) → K)
          x :
        K)
      (0 : K)
Tactic: refine Dual.exists_forall_ne_zero_of_forall_exists (fun i ↦ Dual.eval K M (v i)) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
⊢ ∃ (x : Dual K M),
    Ne.{u_2 + 1} (α := K)
      (((fun (i : ι) ↦ ((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M))) i :
            (a : Dual K M) → K)
          x :
        K)
      (0 : K)
have by_contra! : ∀
  (contra :
    ∀ (x : Dual K M),
      Eq.{u_2 + 1} (α := K)
        ((((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M)) : (a : Dual K M) → K) x : K)
        (0 : K)),
  False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra :
  ∀ (x : Dual K M),
    Eq.{u_2 + 1} (α := K)
      ((((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M)) : (a : Dual K M) → K) x : K) (0 : K)
⊢ False
have contra₁ : v i = 0
Tactic: simp_rw [Dual.eval_apply, forall_dual_apply_eq_zero_iff] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊤ ↔ m = 0
have refine : ∀ (h : Eq (α := Ideal R) (torsionOf R M m) ⊤), m = 0
Tactic: refine ⟨fun h => ?_, fun h => by simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊤
⊢ m = 0
have rw : Membership.mem (γ := Ideal R) ⊤ 1
Tactic: rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊥ ↔ m ≠ 0
have refine_1 : ∀ (h : Eq (α := Ideal R) (torsionOf R M m) ⊥) (contra : m = 0), False
Tactic: refine ⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
refine_1 : ∀ (h : Eq (α := Ideal R) (torsionOf R M m) ⊥) (contra : m = 0), False
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊥ ↔ m ≠ 0
have refine_2 : ∀ (h : m ≠ 0) (r : R) (hr : Membership.mem (γ := Submodule R R) (torsionOf R M m) r), r = 0
Tactic: refine ⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊥
contra : m = 0
⊢ False
have h₁ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊥
Tactic: rw [contra, torsionOf_zero] at h
Cleared hypotheses: h, contra
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : Membership.mem (γ := Submodule R R) (torsionOf R M m) r
⊢ r = 0
have hr₁ : r = 0 ∨ m = 0
Tactic: rw [mem_torsionOf_iff, smul_eq_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0
have refine_2 : ∀ (hr : r = 0), r = 0
Tactic: tauto
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
refine_2 : ∀ (hr : r = 0), r = 0
⊢ r = 0
have refine_2₁ : ∀ (hr : m = 0), r = 0
Tactic: tauto
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Ideal R) (annihilator R M) (⨅ (x : M), torsionOf R M x)
have h : ∀ (r : R),
  Membership.mem (γ := Ideal R) (annihilator R M) r ↔ Membership.mem (γ := Ideal R) (⨅ (x : M), torsionOf R M x) r
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
hv : iSupIndep.{u_3 + 1, u_5} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
⊢ LinearIndependent R v
have refine : ∀ (i : ι) (r : R) (hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)), r = 0
Tactic: refine linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
hv : iSupIndep.{u_3 + 1, u_5} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
⊢ r = 0
have hv₁ : Disjoint (α := Submodule R M) (R ∙ v i) (⨆ (j : ι), ⨆ (_ : j ≠ i), R ∙ v j)
Tactic: replace hv := iSupIndep_def.mp hv i
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv : Disjoint (α := Submodule R M) (R ∙ v i) (⨆ (j : ι), ⨆ (_ : j ≠ i), R ∙ v j)
⊢ r = 0
have hv₁ : Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
Tactic: simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) ⊥ (r • v i)
have rw : Membership.mem (γ := Submodule R M) (R ∙ v i) (r • v i) ∧
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
    (r • v i)
Tactic: rw [← hv, Submodule.mem_inf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) (R ∙ v i) (r • v i) ∧
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
      (r • v i)
have refine : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
  (r • v i)
Tactic: refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
    (r • v i)
have h : (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) = v '' (Set.univ \ {i})
Tactic: convert! hi
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) = v '' (Set.univ \ {i})
have h : ∀ (x : M),
  Membership.mem (γ := Set M) (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) x ↔
    x ∈ v '' (Set.univ \ {i})
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ r = 0
have this : Membership.mem (γ := Submodule R M) ⊥ (r • v i)
Tactic: have : r • v i ∈ (⊥ : Submodule R M) := by
    rw [← hv, Submodule.mem_inf]
    refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
    convert! hi
    ext
    simp
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
this : Membership.mem (γ := Submodule R M) ⊥ (r • v i)
⊢ r = 0
have rw : Membership.mem (γ := Submodule R R) (torsionOf R M (v i)) r
Tactic: rw [← Submodule.mem_bot R, ← h_ne_zero i]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x →
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
      Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
have this : ∀ (a : S) (hx : a • x = 0),
  Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
Tactic: ⟨a,hx⟩
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
have this : ∀ (b : S) (hy : b • y = 0), Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
Tactic: ⟨b,hy⟩
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
have h : (b * a) • (x + y) = 0
Tactic: use b * a
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ (b * a) • (x + y) = 0
have h : (b * a) • x + (b * a) • y = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
⊢ (b * a) • (x + y) = 0
have h₁ : b • a • x + (b * a) • y = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
⊢ (b * a) • (x + y) = 0
have h₂ : b • a • x + (a * b) • y = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
⊢ (b * a) • (x + y) = 0
have h₃ : b • a • x + a • b • y = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
⊢ (b * a) • (x + y) = 0
have h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
⊢ (b * a) • (x + y) = 0
have h₅ : HSMul.hSMul (β := M) b 0 + HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
h₅ : HSMul.hSMul (β := M) b 0 + HSMul.hSMul (β := M) a 0 = 0
⊢ (b * a) • (x + y) = 0
have h₆ : 0 + HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
h₅ : HSMul.hSMul (β := M) b 0 + HSMul.hSMul (β := M) a 0 = 0
h₆ : 0 + HSMul.hSMul (β := M) a 0 = 0
⊢ (b * a) • (x + y) = 0
have h₇ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
h₅ : HSMul.hSMul (β := M) b 0 + HSMul.hSMul (β := M) a 0 = 0
h₆ : 0 + HSMul.hSMul (β := M) a 0 = 0
h₇ : HAdd.hAdd (α := M) 0 0 = 0
⊢ (b * a) • (x + y) = 0
have h₈ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
a : R
x : M
h_1 : Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x
b : S
h : b • x = 0
⊢ b • a • x = 0
have rw : a • b • x = 0
Tactic: rw [smul_comm, h, smul_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
a : R
x : M
h_1 : Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x
b : S
h : b • x = 0
rw : a • b • x = 0
⊢ b • a • x = 0
have rw₁ : HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [smul_comm, h, smul_zero]
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
a : R
x : M
h_1 : Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x
b : S
h : b • x = 0
rw : a • b • x = 0
rw₁ : HSMul.hSMul (β := M) a 0 = 0
⊢ b • a • x = 0
have rw₂ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_comm, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ IsTorsionBy R M a ↔ Membership.mem (γ := Ideal R) (annihilator R M) a
have rw : (∀ ⦃x : M⦄, a • x = 0) ↔ Membership.mem (γ := Ideal R) (annihilator R M) a
Tactic: rw [IsTorsionBy, mem_annihilator]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
rw : (∀ ⦃x : M⦄, a • x = 0) ↔ Membership.mem (γ := Ideal R) (annihilator R M) a
⊢ IsTorsionBy R M a ↔ Membership.mem (γ := Ideal R) (annihilator R M) a
have rw₁ : (∀ ⦃x : M⦄, a • x = 0) ↔ ∀ (m : M), a • m = 0
Tactic: rw [IsTorsionBy, mem_annihilator]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ (↑(annihilator R M) : Set R)
have simp_rw : (∀ ⦃x : M⦄ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
Tactic: simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
have rw : (∀ (b : (↑s : Type u_1)) (a : M), (↑b : R) • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
Tactic: rw [forall_comm, SetCoe.forall]