awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
c : R
g : α → M
hc : c ≠ 0
⊢ support (c • g) = support g

Tactic:
ext fun _ ↦ smul_ne_zero_iff_right hc

Premises used: Set.ext, smul_ne_zero_iff_right
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
f : α → R
g : α → M
⊢ support (f • g) = support f ∩ support g

Tactic:
ext fun _ => smul_ne_zero_iff

Premises used: Set.ext, smul_ne_zero_iff
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
a : R
f : α → M
⊢ support (a • f) ⊆ support f

Tactic:
support_smul_subset_right (fun _ ↦ a) f

Premises used: Function.support_smul_subset_right
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
dsimp : (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0
⊢ s.indicator (fun (a : α) ↦ r a • f a) a = r a • s.indicator f a

Tactic:
dsimp only [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
pos : a ∈ s → r a • f a = r a • f a
neg : ¬a ∈ s → 0 = HSMul.hSMul (β := M) (r a) 0
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h : a ∈ s
⊢ r a • f a = r a • f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h : ¬a ∈ s
⊢ 0 = HSMul.hSMul (β := M) (r a) 0

Tactic:
(smul_zero (r a)).symm

Premises used: smul_zero, Eq.symm
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h : a ∈ s
⊢ r a • f a = r a • f a

Tactic:
exacts [rfl, (smul_zero (r a)).symm]

Premises used: smul_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
⊢ Eq (α := (x : α) → M) (s.indicator fun (a : α) ↦ r a • f a) fun (a : α) ↦ r a • s.indicator f a

Tactic:
funext <| indicator_smul_apply s r f

Premises used: funext, Set.indicator_smul_apply
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : R
f : α → M
a : α
⊢ s.indicator (fun (x : α) ↦ r • f x) a = r • s.indicator f a

Tactic:
indicator_smul_apply s (fun _ ↦ r) f a

Premises used: Set.indicator_smul_apply
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : R
f : α → M
⊢ Eq (α := (x : α) → M) (s.indicator fun (x : α) ↦ r • f x) fun (x : α) ↦ r • s.indicator f x

Tactic:
funext <| indicator_const_smul_apply s r f

Premises used: funext, Set.indicator_const_smul_apply
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
dsimp : (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a
⊢ s.indicator (fun (a : α) ↦ r a • f a) a = s.indicator r a • f a

Tactic:
dsimp only [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
pos : a ∈ s → r a • f a = r a • f a
neg : ¬a ∈ s → 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (f a)
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h : a ∈ s
⊢ r a • f a = r a • f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h : ¬a ∈ s
⊢ 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (f a)

Tactic:
(zero_smul _ (f a)).symm

Premises used: zero_smul, Eq.symm
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h : a ∈ s
⊢ r a • f a = r a • f a

Tactic:
exacts [rfl, (zero_smul _ (f a)).symm]

Premises used: zero_smul, Eq.symm, rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
⊢ Eq (α := (x : α) → M) (s.indicator fun (a : α) ↦ r a • f a) fun (a : α) ↦ s.indicator r a • f a

Tactic:
funext <| indicator_smul_apply_left _ _ _

Premises used: Set.indicator_smul_apply_left, funext
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
m : M
a : α
⊢ s.indicator (fun (x : α) ↦ r x • m) a = s.indicator r a • m

Tactic:
indicator_smul_apply_left _ _ _ _

Premises used: Set.indicator_smul_apply_left
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
m : M
⊢ Eq (α := (x : α) → M) (s.indicator fun (x : α) ↦ r x • m) fun (x : α) ↦ s.indicator r x • m

Tactic:
funext <| indicator_smul_const_apply _ _ _

Premises used: Set.indicator_smul_const_apply, funext
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
inst : MulZeroOneClass R
s : Set α
r : R
a : α
simp_rw :
  Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r (1 x)) a) (s.indicator (fun (x : α) ↦ r) a)
simp_rw₁ :
  Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r 1) a) (s.indicator (fun (x : α) ↦ r) a)
simp_rw₂ : Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ r * 1) a) (s.indicator (fun (x : α) ↦ r) a)
⊢ HSMul.hSMul (β := R) r (s.indicator 1 a) = s.indicator (fun (x : α) ↦ r) a

Tactic:
simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

Premises used: Pi.one_apply, Set.indicator_const_smul_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
l : List R
x : M
⊢ l.sum • x = sum (map (fun (r : R) ↦ r • x) l)

Tactic:
map_list_sum ((smulAddHom R M).flip x) l

Premises used: map_list_sum, AddMonoidHom.flip, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
l : Multiset R
x : M
⊢ l.sum • x = sum (map (fun (r : R) ↦ r • x) l)

Tactic:
((smulAddHom R M).flip x).map_multiset_sum l

Premises used: AddMonoidHom.flip, smulAddHom, AddMonoidHom.map_multiset_sum, DFunLike.coe
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Multiset M
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := R) (sum 0) t.sum =
    sum (map (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Multiset R) 0 t))

Tactic:
simp
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Multiset M
a : R
s : Multiset R
ih : s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))
⊢ (a ::ₘ s).sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) ((a ::ₘ s) ×ˢ t))

Tactic:
simp [add_smul, ih, ← Multiset.smul_sum]

Premises used: Multiset.smul_sum, add_smul
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Multiset R
t : Multiset M
empty :
  HSMul.hSMul.{u_5, u_6, u_6} (α := R) (sum 0) t.sum =
    sum (map (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Multiset R) 0 t))
cons :
  ∀ (a : R) (s : Multiset R) (ih : s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))),
    (a ::ₘ s).sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) ((a ::ₘ s) ×ˢ t))
⊢ s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simp [add_smul, ih, ← Multiset.smul_sum]

Premises used: Multiset.smul_sum, Multiset.cons, add_smul
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → R
s : Finset ι
x : M
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := R) (∑ i ∈ s, f i) x = ∑ i ∈ s, f i • x

Tactic:
map_sum ((smulAddHom R M).flip x) f s

Premises used: map_sum, AddMonoidHom.flip, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
t : Finset β
f : α → R
g : β → M
simp_rw : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul (β := M) (f i) (∑ j ∈ t, g j)) (∑ i ∈ s, ∑ j ∈ t, f i • g j)
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := R) (β := M) (∑ i ∈ s, f i) (∑ j ∈ t, g j) = ∑ i ∈ s, ∑ j ∈ t, f i • g j

Tactic:
simp_rw [sum_smul, ← smul_sum]

Premises used: Finset.sum_smul, Finset.smul_sum
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype α
inst_4 : Fintype β
f : α → R
g : β → M
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := R) (β := M) (∑ i : α, f i) (∑ j : β, g j) = ∑ i : α, ∑ j : β, f i • g j

Tactic:
Finset.sum_smul_sum _ _

Premises used: Finset.sum_smul_sum
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
α : Type u_3
R : Type u_5
inst : NonAssocSemiring R
s : Finset α
rw : (↑(#s) : R) = HSMul.hSMul (β := R) (#s) 1
rw₁ rw₂ : Eq.{u_5 + 1} (α := R) (↑(#s) : R) (↑(#s) : R)
⊢ Eq.{u_5 + 1} (α := R) (↑(#s) : R) (∑ x ∈ s, 1)

Tactic:
rw [Finset.sum_const, Nat.smul_one_eq_cast]

Premises used: Nat.smul_one_eq_cast, Finset.sum_const
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
rw :
  ∑ b ∈ image (fun (g : (a : ι) → κ) ↦ g i) (piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s),
      Finset.card (α := (a : ι) → κ) ({a ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s | a i = b}) • f b =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
⊢ ∑ g ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, f (g i) =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)

Tactic:
rw [Finset.sum_comp]

Premises used: Finset.sum_comp
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun (g : (a : ι) → κ) ↦ g i) (piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s),
      Finset.card (α := (a : ι) → κ) ({a ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s | a i = b}) • f b =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)

Tactic:
simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

Premises used: Finset.sum_ite_mem, Finset.inter_self, zero_smul, Finset.smul_sum, ite_smul, Fintype.card_filter_piFinset_const, Fintype.eval_image_piFinset_const
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
rw rw₁ rw₂ :
  ∑ b ∈ image (fun (g : (a : ι) → κ) ↦ g i) (piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s),
      Finset.card (α := (a : ι) → κ) ({a ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s | a i = b}) • f b =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
⊢ ∑ g ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, f (g i) =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)

Tactic:
classical
  rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

Premises used: Finset.sum_ite_mem, Finset.inter_self, Finset.sum_comp, zero_smul, Finset.smul_sum, ite_smul, Fintype.eval_image_piFinset_const
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R α
f : ι → α
r : R
i₀ : ι
h₀ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) univ b →
      b ≠ i₀ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r b : R) (f b) = 0
h₁ : i₀ ∉ univ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i₀ : R) (f i₀) = 0
⊢ ∑ i : ι, HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i : R) (f i) = r • f i₀

Tactic:
rw [Finset.sum_eq_single i₀, Pi.single_eq_same]

Premises used: Finset.sum_eq_single, Pi.single_eq_same
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ (b : ι),
    Membership.mem (γ := Finset ι) univ b →
      b ≠ i₀ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r b : R) (f b) = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.BigOperators
Goal:
ι : Type u_1
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i₀ : R) (f i₀) = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
h : m ∈ (↑p : Set M)
⊢ HSMul.hSMul (α := A ⊗[R] B) 0 m ∈ (↑p : Set M)

Tactic:
simp only [zero_smul, SetLike.mem_coe, zero_mem]

Premises used: zero_smul, SetLike.mem_coe, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
a : A
b : B
hm : m ∈ (↑p : Set M)
⊢ HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m ∈ (↑p : Set M)

Tactic:
simpa only [TensorProduct.Algebra.smul_def] using hA a (hB b hm)

Premises used: TensorProduct.Algebra.smul_def
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : m ∈ (↑p : Set M) → z • m ∈ (↑p : Set M)
hw : m ∈ (↑p : Set M) → w • m ∈ (↑p : Set M)
hm : m ∈ (↑p : Set M)
⊢ (z + w) • m ∈ (↑p : Set M)

Tactic:
simpa only [add_smul] using p.add_mem (hz hm) (hw hm)

Premises used: AddSubmonoid.add_mem, add_smul
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) m
⊢ a • m ∈ p

Tactic:
this.symm ▸ p.smul_mem _ hm

Premises used: Eq.rec, Eq.symm, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) m
⊢ a • m ∈ p

Tactic:
exact this.symm ▸ p.smul_mem _ hm
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
suffices : a • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) m
⊢ a • m ∈ p

Tactic:
suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) m

Tactic:
simp [TensorProduct.Algebra.smul_def]

Premises used: TensorProduct.Algebra.smul_def
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = HSMul.hSMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) m
⊢ b • m ∈ p

Tactic:
this.symm ▸ p.smul_mem _ hm

Premises used: Eq.rec, Eq.symm, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = HSMul.hSMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) m
⊢ b • m ∈ p

Tactic:
exact this.symm ▸ p.smul_mem _ hm
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
suffices : b • m = HSMul.hSMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) m
⊢ b • m ∈ p

Tactic:
suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm
-- Module: Mathlib.Algebra.Module.Bimodule
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m = HSMul.hSMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) m

Tactic:
simp [TensorProduct.Algebra.smul_def]

Premises used: TensorProduct.Algebra.smul_def
-- Module: Mathlib.Algebra.Module.Card
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
⊢ ∃ (x : E), x ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Card
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
obtain : ∀ (x : E) (hx : x ≠ 0), lift.{v, u} #R ≤ lift.{u, v} #E
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Card
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
x : E
hx : x ≠ 0
⊢ Injective.{u + 1, v + 1} (β := E) fun (k : R) ↦ k • x

Tactic:
have : Injective (fun k ↦ k • x) := smul_left_injective R hx
-- Module: Mathlib.Algebra.Module.Card
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
x : E
hx : x ≠ 0
this : Injective.{u + 1, v + 1} (β := E) fun (k : R) ↦ k • x
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
lift_mk_le_lift_mk_of_injective this

Premises used: Cardinal.lift_mk_le_lift_mk_of_injective
-- Module: Mathlib.Algebra.Module.Card
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
x : E
hx : x ≠ 0
this : Injective.{u + 1, v + 1} (β := E) fun (k : R) ↦ k • x
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
exact lift_mk_le_lift_mk_of_injective this

Premises used: Cardinal.lift_mk_le_lift_mk_of_injective
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
x x_1 : CharacterModule A
h :
  Eq.{max (uA + 1) 1} (α := (a : A) → AddCircle (𝕜 := ℚ) 1)
    ((fun (c : CharacterModule A) ↦ (↑c : ZeroHom A (AddCircle 1)).toFun) x)
    ((fun (c : CharacterModule A) ↦ (↑c : ZeroHom A (AddCircle 1)).toFun) x_1)
⊢ x = x_1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
c c' : CharacterModule A
h :
  ∀ (x : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
      ((c' : (a : A) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
⊢ c = c'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
inst_2 : Module R A
c : CharacterModule A
r : R
a : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((r • c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1)
    ((c : (a : A) → AddCircle 1) (r • a) : AddCircle (𝕜 := ℚ) 1)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl