awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
c₁ c₂ : R
x : M₂
rcases :
  ∀ (x : M),
    HSMul.hSMul (β := M₂) (c₁ + c₂) ((f : (a : M) → M₂) x : M₂) =
      HSMul.hSMul (β := M₂) c₁ ((f : (a : M) → M₂) x : M₂) + HSMul.hSMul (β := M₂) c₂ ((f : (a : M) → M₂) x : M₂)
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x

Tactic:
rcases hf x with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
c₁ c₂ : R
x : M
⊢ HSMul.hSMul (β := M₂) (c₁ + c₂) ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) c₁ ((f : (a : M) → M₂) x : M₂) + HSMul.hSMul (β := M₂) c₂ ((f : (a : M) → M₂) x : M₂)

Tactic:
simp only [add_smul, ← smul, ← f.map_add]

Premises used: add_smul, AddMonoidHom.map_add
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M₂
rcases : ∀ (x : M), HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 x = 0

Tactic:
rcases hf x with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M →+ M₂
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
smul : ∀ (c : R) (x : M), (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)
x : M
rw : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = (f : (a : M) → M₂) 0
rw₁ :
  Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x) : M₂)
    ((f : (a : M) → M₂) 0 : M₂)
rw₂ rw₃ : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) 0 : M₂) ((f : (a : M) → M₂) 0 : M₂)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((f : (a : M) → M₂) x : M₂) = 0

Tactic:
rw [← f.map_zero, ← smul, zero_smul]

Premises used: AddMonoidHom.map_zero, zero_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
zero_eq_one : Eq.{u_1 + 1} (α := R) 0 1
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ x = 0

Tactic:
rw [← one_smul R x, ← zero_eq_one, zero_smul]

Premises used: one_smul, zero_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
M : Type u_3
inst : AddCommMonoid M
R : Type u_5
inst_1 : Ring R
inst_2 : Module R M
r : R
m : M
rw : (r + (1 - r)) • m = m
rw₁ : HSMul.hSMul.{u_5, u_3, u_3} (α := R) 1 m = m
rw₂ rw₃ : m = m
⊢ r • m + (1 - r) • m = m

Tactic:
rw [← add_smul, add_sub_cancel, one_smul]

Premises used: one_smul, add_smul, add_sub_cancel
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
rw : a • x + b • y = b • y + a • x
rw₁ rw₂ : b • y + a • x = b • y + a • x
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)

Tactic:
rw [sub_add_add_cancel, add_comm]

Premises used: add_comm, sub_add_add_cancel
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
a b : R
h : a + b = 1
rw : b • y - b • x + (a • x + b • x) = b • y - b • x + x
rw₁ rw₂ : b • y - b • x + x = b • y - b • x + x
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
rw [smul_sub, Convex.combo_self h]

Premises used: Convex.combo_self, smul_sub
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_5
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
smul : ∀ (x : R) (x_1 : M), SMul.smul x x_1 = SMul.smul x x_1
⊢ P = Q

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_5
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x : R
x_1 : M
⊢ SMul.smul x x_1 = SMul.smul x x_1

Tactic:
w _ _
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_5
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x : R
x_1 : M
⊢ SMul.smul x x_1 = SMul.smul x x_1

Tactic:
exact w _ _
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : (-r + r) • x = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ -r • x + r • x = 0

Tactic:
rw [← add_smul, neg_add_cancel, zero_smul]

Premises used: zero_smul, neg_add_cancel, add_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
rw : -(r • -x) = r • x
rw₁ : - -(r • x) = r • x
rw₂ rw₃ : r • x = r • x
⊢ -r • -x = r • x

Tactic:
rw [neg_smul, smul_neg, neg_neg]

Premises used: neg_smul, neg_neg, smul_neg
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) x = -x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y

Tactic:
simp [add_smul, sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_5
M : Type u_6
inst : MonoidWithZero R
inst_1 : Subsingleton R
inst_2 : Zero M
inst_3 : MulActionWithZero R M
⊢ Subsingleton M

Tactic:
MulActionWithZero.subsingleton R M

Premises used: MulActionWithZero.subsingleton
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_5
M : Type u_6
inst : MonoidWithZero R
inst_1 : Nontrivial M
inst_2 : Zero M
inst_3 : MulActionWithZero R M
⊢ Nontrivial R

Tactic:
MulActionWithZero.nontrivial R M

Premises used: MulActionWithZero.nontrivial
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R) ↔ f ≠ 0

Tactic:
⟨ne_zero_of_surjective, fun hf z ↦ ?_⟩

Premises used: Iff.intro, LinearMap.ne_zero_of_surjective
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
refine : ∀ (hf : f ≠ 0) (z : R), ∃ (a : M), (f : (a : M) → R) a = z
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R) ↔ f ≠ 0

Tactic:
refine ⟨ne_zero_of_surjective, fun hf z ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
⊢ ∃ (y : M), Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)

Tactic:
simpa [Ne, LinearMap.ext_iff] using hf

Premises used: LinearMap.ext_iff, Ne
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
obtain : ∀ (y : M) (hy : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)), ∃ (a : M), (f : (a : M) → R) a = z
⊢ ∃ (a : M), (f : (a : M) → R) a = z

Tactic:
obtain ⟨y, hy⟩ : ∃ y, f y ≠ 0 := by simpa [Ne, LinearMap.ext_iff] using hf
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
y : M
hy : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)
⊢ (f : (a : M) → R) (HMul.hMul (β := R) z (((f : (a : M) → R) y)⁻¹ : R) • y) = z

Tactic:
simp [hy]
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : DivisionSemiring R
inst_2 : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
y : M
hy : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)
⊢ ∃ (a : M), (f : (a : M) → R) a = z

Tactic:
exact ⟨(z * (f y)⁻¹) • y, by simp [hy]⟩
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
simp_rw : (∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z) ↔ ∃ (a : R), a • x = z
⊢ Membership.mem (γ := Submodule R M₁) (range (f.smulRight x)) z ↔ Membership.mem (γ := Submodule R M₁) (R ∙ x) z

Tactic:
simp_rw [mem_range, smulRight_apply, Submodule.mem_span_singleton]

Premises used: LinearMap.smulRight_apply, Submodule.mem_span_singleton, LinearMap.mem_range
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
⊢ (∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z) ↔ ∃ (a : R), a • x = z

Tactic:
⟨fun ⟨w, hw⟩ ↦ ⟨f w, hw ▸ rfl⟩, fun ⟨w, hw⟩ ↦ ?_⟩

Premises used: _private.0.LinearMap.range_smulRight_apply_of_surjective.match_2, Exists, Eq.rec, _private.0.LinearMap.range_smulRight_apply_of_surjective.match_3, Iff.intro, Exists.intro, HSMul.hSMul, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
refine :
  (∃ (a : R), a • x = z) →
    ∀ (w : R) (hw : w • x = z), ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
⊢ (∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z) ↔ ∃ (a : R), a • x = z

Tactic:
refine ⟨fun ⟨w, hw⟩ ↦ ⟨f w, hw ▸ rfl⟩, fun ⟨w, hw⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
h : ∃ (a : R), a • x = z
w : R
hw : w • x = z
obtain :
  ∀ (y : M) (hw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z),
    ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
⊢ ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z

Tactic:
obtain ⟨y, rfl⟩ := hf w

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
h : ∃ (a : R), a • x = z
y : M
hw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
⊢ ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z

Tactic:
⟨y, hw⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R) (⇑f : (a : M) → R)
x z : M₁
h : ∃ (a : R), a • x = z
y : M
hw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z
⊢ ∃ (y : M), HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : M) → R) y : R) x = z

Tactic:
exact ⟨y, hw⟩
-- Module: Mathlib.Algebra.Module.LinearMap.DivisionRing
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₁
inst_2 : DivisionSemiring R
inst_3 : Module R M
inst_4 : Module R M₁
f : M →ₗ[R] R
hf : f ≠ 0
x : M₁
⊢ Eq (α := Submodule R M₁) (range (f.smulRight x)) (R ∙ x)

Tactic:
range_smulRight_apply_of_surjective (f.surjective hf) x

Premises used: LinearMap.range_smulRight_apply_of_surjective, LinearMap.surjective
-- Module: Mathlib.Algebra.Module.RingHom
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
M₂ : Type u_4
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
r s : R_1
x_1 : M_1
R : Type u_5
S : Type u_6
M : Type u_7
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Semiring S
inst_7 : SMul S M
f : R →+* S
hf : Surjective.{u_5 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) c : S) x = c • x
a b : R
x : M
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) • x =
    HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) a : S) x +
      HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) b : S) x

Tactic:
simp only [← f.map_add, hsmul, add_smul]

Premises used: add_smul, RingHom.map_add
-- Module: Mathlib.Algebra.Module.RingHom
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
M₂ : Type u_4
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
r s : R_1
x_1 : M_1
R : Type u_5
S : Type u_6
M : Type u_7
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Semiring S
inst_7 : SMul S M
f : R →+* S
hf : Surjective.{u_5 + 1, u_6 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) c : S) x = c • x
x : M
rw : HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((f : (a : R) → S) 0 : S) x = 0
rw₁ : HSMul.hSMul.{u_5, u_7, u_7} (α := R) 0 x = 0
rw₂ rw₃ : Eq.{u_7 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_6, u_7, u_7} (α := S) 0 x = 0

Tactic:
rw [← f.map_zero, hsmul, zero_smul]

Premises used: zero_smul, RingHom.map_zero
-- Module: Mathlib.Algebra.Module.RingHom
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r_1 s_1 : R
x_1 : M
inst_3 : Semiring S
f : S →+* R
r s : S
x : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : S) → R) (r + s) : R) x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : S) → R) r : R) x +
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((f : (a : S) → R) s : R) x

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
y : S
⊢ x • y = HMul.hMul (α := S) ((f : (a : R) → S) x : S) y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
y : M
⊢ y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)

Tactic:
mem_bot R₂

Premises used: Set.Mem, Submodule.mem_bot, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := Submodule R M) (ker id) ⊥

Tactic:
rfl

Premises used: Set.Mem, LinearMap.ker, setOf, Submodule.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x : ↥f.ker
⊢ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) (↑x : M) : M₂) (0 : M₂)

Tactic:
mem_ker.1 x.2

Premises used: LinearMap.mem_ker, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker.toAddSubmonoid = AddMonoidHom.mker f

Tactic:
rfl

Premises used: AddMonoidHom.mker, AddSubmonoid.comap, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
rw :
  (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔
    ∀ (a : M) (b : a ∈ N),
      Eq.{u_7 + 1} (α := M₂) ((f ∘ₛₗ N.subtype : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)
        ((0 : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)
⊢ N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0

Tactic:
rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]

Premises used: SetLike.le_def, Subtype.forall, LinearMap.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔
    ∀ (a : M) (b : a ∈ N),
      Eq.{u_7 + 1} (α := M₂) ((f ∘ₛₗ N.subtype : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)
        ((0 : (a : ↥N) → M₂) (Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f ∘ₛₗ f.ker.subtype = 0

Tactic:
LinearMap.ext fun x => mem_ker.1 x.2

Premises used: LinearMap.ext, LinearMap.mem_ker, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ (g ∘ₛₗ f).ker = comap f g.ker

Tactic:
rfl

Premises used: Set.Mem, LinearMap.ker, setOf, Submodule.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
rw : f.ker ≤ comap f g.ker
⊢ f.ker ≤ (g ∘ₛₗ f).ker

Tactic:
rw [ker_comp]

Premises used: LinearMap.ker_comp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ comap f g.ker

Tactic:
comap_mono bot_le

Premises used: Submodule.comap_mono, Set.Mem, bot_le
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ comap f g.ker

Tactic:
exact comap_mono bot_le

Premises used: Submodule.comap_mono, bot_le
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker

Tactic:
sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩

Premises used: Iff.mpr, sup_le_iff, And.intro, LinearMap.ker_le_ker_comp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
refine : f.ker ≤ (f ∘ₗ g).ker
⊢ f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker

Tactic:
refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩

Premises used: Iff.mpr, sup_le_iff, And.intro, LinearMap.ker_le_ker_comp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
rw : f.ker ≤ (g ∘ₗ f).ker
⊢ f.ker ≤ (f ∘ₗ g).ker

Tactic:
rw [← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, Commute.eq
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (g ∘ₗ f).ker

Tactic:
ker_le_ker_comp f g

Premises used: LinearMap.ker_le_ker_comp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (g ∘ₗ f).ker

Tactic:
exact ker_le_ker_comp f g

Premises used: LinearMap.ker_le_ker_comp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
x : M
hx : x ∈ f.ker
⊢ x ∈ comap f p

Tactic:
simp [mem_ker.mp hx]

Premises used: LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ Disjoint p f.ker ↔ ∀ x ∈ p, Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂) → x = 0

Tactic:
simp [disjoint_def]

Premises used: Submodule.disjoint_def
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker = ⊥ ↔ ∀ (m : M), Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) (0 : M₂) → m = 0

Tactic:
simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤)

Premises used: LinearMap.disjoint_ker, disjoint_iff_inf_le