awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) (0 : M₂)
rw : Eq (α := M) ((id : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((g ∘ₛₗ f : (a : M) → M) m : M) (0 : M)
rw₂ : Eq.{u_5 + 1} (α := M) ((g : (a : M₂) → M) ((f : (a : M) → M₂) m : M₂) : M) (0 : M)
rw₃ : Eq.{u_5 + 1} (α := M) ((g : (a : M₂) → M) 0 : M) (0 : M)
rw₄ rw₅ : Eq.{u_5 + 1} (α := M) 0 0
⊢ m = 0

Tactic:
rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]

Premises used: LinearMap.id_apply, LinearMap.comp_apply, LinearMap.map_zero
-- 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₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
rw : p ≤ comap f ⊥ ↔ map f p = ⊥
rw₁ : p ≤ comap f ⊥ ↔ map f p ≤ ⊥
rw₂ rw₃ : p ≤ comap f ⊥ ↔ p ≤ comap f ⊥
⊢ p ≤ f.ker ↔ map f p = ⊥

Tactic:
rw [ker, eq_bot_iff, map_le_iff_le_comap]

Premises used: LinearMap.ker, Submodule.map_le_iff_le_comap, eq_bot_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₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
rw : comap f ⊥ = f.ker
⊢ (codRestrict p f hf).ker = f.ker

Tactic:
rw [ker, comap_codRestrict, Submodule.map_bot]

Premises used: LinearMap.ker, Submodule.map_bot, LinearMap.comap_codRestrict
-- 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₂
hf : ∀ (c : M), Membership.mem (α := M₂) p ((f : (a : M) → M₂) c : M₂)
⊢ comap f ⊥ = f.ker

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₂
p : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (f.domRestrict p).ker = comap p.subtype f.ker

Tactic:
ker_comp ..

Premises used: LinearMap.ker_comp, LinearMap.domRestrict
-- 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
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
rw : (codRestrict q (f.domRestrict p) ⋯).ker = comap p.subtype f.ker
rw₁ : (f.domRestrict p).ker = comap p.subtype f.ker
rw₂ rw₃ : comap p.subtype f.ker = comap p.subtype f.ker
⊢ (f.restrict hf).ker = comap p.subtype f.ker

Tactic:
rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

Premises used: LinearMap.ker_codRestrict, LinearMap.restrict_eq_codRestrict_domRestrict, LinearMap.ker_domRestrict
-- 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₂
x : M
⊢ Membership.mem (γ := Submodule R M) (ker.{u_1, u_2, u_5, u_7} (R₂ := R₂) (M₂ := M₂) (τ₁₂ := τ₁₂) 0) x

Tactic:
simp
-- 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 = ⊤ ↔ f = 0

Tactic:
⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩

Premises used: trivial, LinearMap.ext, Eq.rec, LinearMap.mem_ker, LinearMap.ker_zero, Iff.intro, Iff.mp, Eq.symm
-- 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₂
h :
  ∀ (x : ↥f.ker),
    Eq.{u_7 + 1} (α := M₂) ((f.domRestrict f.ker : (a : ↥f.ker) → M₂) x : M₂) ((0 : (a : ↥f.ker) → M₂) x : M₂)
⊢ Eq (α := LinearMap.{u_1, u_2, u_5, u_7} τ₁₂ (↥f.ker) M₂) (f.domRestrict f.ker) 0

Tactic:
ext
-- 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.domRestrict f.ker : (a : ↥f.ker) → M₂) x : M₂) ((0 : (a : ↥f.ker) → M₂) x : M₂)

Tactic:
simp
-- 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₂
h : f ≠ 0
s : Set (Submodule R M)
hs : sSup s = ⊤
contrapose! : ∀ (h : ∀ (m : Submodule R M) (_ : m ∈ s), f ∘ₛₗ m.subtype = 0), f = 0
⊢ ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0

Tactic:
contrapose! h
-- 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₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h simp_rw : ∀ b ∈ s, f ∘ₛₗ b.subtype = 0
⊢ f = 0

Tactic:
simp_rw [← ker_eq_top, eq_top_iff, ← hs, sSup_le_iff, le_ker_iff_comp_subtype_eq_zero]

Premises used: LinearMap.ker_eq_top, LinearMap.le_ker_iff_comp_subtype_eq_zero, eq_top_iff, sSup_le_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₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ (m : Submodule R M) (_ : m ∈ s), f ∘ₛₗ m.subtype = 0
⊢ ∀ b ∈ s, f ∘ₛₗ b.subtype = 0

Tactic:
h
-- 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₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ (m : Submodule R M) (_ : m ∈ s), f ∘ₛₗ m.subtype = 0
⊢ ∀ b ∈ s, f ∘ₛₗ b.subtype = 0

Tactic:
exact h
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
M : Type u_11
M₂ : Type u_12
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f : M →+ M₂
⊢ f.toIntLinearMap.ker = (AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) f.ker

Tactic:
rfl

Premises used: LinearMap.ker, AddMonoidHom.mker, AddSubmonoid.comap, Submodule.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₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw : f.ker ≤ ⊥
⊢ f.ker = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_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₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
hx : x ∈ f.ker
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx

Premises used: Submodule.mem_bot, Function.Injective.eq_iff, map_zero, LinearMap.mem_ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 →ₗ[R] M
n m : ℕ
w : n ≤ m
x : M
h : Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) n) x
obtain : ∀ (c : ℕ) (w : n ≤ n + c), Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) m) x

Tactic:
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 →ₗ[R] M
n : ℕ
x : M
h : Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) n) x
c : ℕ
w : n ≤ n + c
rw :
  ∀ (h : Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)) (c : ℕ) (w : n ≤ n + c),
    Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x

Tactic:
rw [LinearMap.mem_ker] at h

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 →ₗ[R] M
n : ℕ
x : M
h : Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
c : ℕ
w : n ≤ n + c
rw : Eq (α := M) ((f ^ (n + c) : (a : M) → M) x : M) (0 : M)
rw₁ : Eq (α := M) ((f ^ (c + n) : (a : M) → M) x : M) (0 : M)
rw₂ : Eq (α := M) ((f ^ c * f ^ n : (a : M) → M) x : M) (0 : M)
rw₃ : Eq (α := M) ((f ^ c : (a : M) → M) ((f ^ n : (a : M) → M) x : M) : M) (0 : M)
rw₄ : Eq (α := M) ((f ^ c : (a : M) → M) 0 : M) (0 : M)
rw₅ rw₆ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x

Tactic:
rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]

Premises used: pow_add, map_zero, add_comm, LinearMap.mem_ker, Module.End.mul_apply
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (x : M), x ∈ (-f).ker ↔ x ∈ f.ker
⊢ (-f).ker = f.ker

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x : M
⊢ x ∈ (-f).ker ↔ x ∈ f.ker

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker.toAddSubgroup = f.toAddMonoidHom.ker

Tactic:
rfl

Premises used: AddMonoidHom.mker, AddSubmonoid.comap, rfl, AddMonoidHom.ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
rw :
  Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) (x - y) : M₂) (0 : M₂) ↔
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
rw₁ :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂) = 0 ↔
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
rw₂ rw₃ :
  Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂) ↔
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
⊢ x - y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
rw [mem_ker, map_sub, sub_eq_zero]

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

Tactic:
rw [disjoint_ker, Set.injOn_iff_map_eq_zero]

Premises used: Set.injOn_iff_map_eq_zero, LinearMap.disjoint_ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
s : Set M
h : s ⊆ (↑p : Set M)
hd : Disjoint p f.ker
⊢ Set.InjOn.{u_5, u_7} (β := M₂) (⇑f : (a : M) → M₂) s

Tactic:
disjoint_ker_iff_injOn.mp hd |>.mono h

Premises used: LinearMap.disjoint_ker_iff_injOn, Iff.mp, Set.InjOn.mono
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker = ⊥ ↔ Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

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

Premises used: LinearMap.disjoint_ker_iff_injOn, disjoint_iff_inf_le
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
rw : (f.domRestrict S).ker = ⊥ ↔ S ⊓ f.ker = ⊥
⊢ Injective.{u_5 + 1, u_7 + 1} (α := ↥S) (β := M₂) (⇑(f.domRestrict S) : (a : ↥S) → M₂) ↔ S ⊓ f.ker = ⊥

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ (f.domRestrict S).ker = ⊥ ↔ S ⊓ f.ker = ⊥

Tactic:
⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩

Premises used: le_bot_iff, Iff.intro, 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
refine_1 : ∀ (h : (f.domRestrict S).ker = ⊥), S ⊓ f.ker ≤ ⊥
refine_2 : ∀ (h : S ⊓ f.ker = ⊥), (f.domRestrict S).ker ≤ ⊥
⊢ (f.domRestrict S).ker = ⊥ ↔ S ⊓ f.ker = ⊥

Tactic:
refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).ker = ⊥
x : M
refine_1 : ∀ (hx : x ∈ (↑S : Set M)) (h'x : x ∈ (↑f.ker : Set M)), Membership.mem (γ := Submodule R M) ⊥ x
⊢ x ∈ S ⊓ f.ker → Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
⟨hx, h'x⟩
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).ker = ⊥
x : M
hx : x ∈ (↑S : Set M)
h'x : x ∈ (↑f.ker : Set M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker

Tactic:
simpa using h'x
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).ker = ⊥
x : M
hx : x ∈ (↑S : Set M)
h'x : x ∈ (↑f.ker : Set M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker

Tactic:
have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).ker = ⊥
x : M
hx : x ∈ (↑S : Set M)
h'x : x ∈ (↑f.ker : Set M)
this : Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker
⊢ Membership.mem (γ := Submodule R ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)

Tactic:
rw [h] at this
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).ker = ⊥
x : M
hx : x ∈ (↑S : Set M)
h'x : x ∈ (↑f.ker : Set M)
this : Membership.mem (γ := Submodule R ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
simpa [mk_eq_zero] using this

Premises used: Submodule.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ f.ker = ⊥
x : M
hx : x ∈ S
h'x : Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker
⊢ x ∈ S ⊓ f.ker

Tactic:
have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ f.ker = ⊥
x : M
hx : x ∈ S
h'x : Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker
this : x ∈ S ⊓ f.ker
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
rw [h] at this
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ f.ker = ⊥
x : M
hx : x ∈ S
h'x : Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ∈ (f.domRestrict S).ker
this : Membership.mem (γ := Submodule R M) ⊥ x
⊢ Membership.mem (γ := Submodule R ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)

Tactic:
simpa [mk_eq_zero] using this

Premises used: Submodule.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
rw₂ : (f.domRestrict p).ker = ⊥ ↔ Disjoint p f.ker
rw₃ : Injective (α := ↥p) (β := M) (⇑(f.domRestrict p) : (a : ↥p) → M) ↔ Disjoint p f.ker
rw₄ : p ⊓ f.ker = ⊥ ↔ Disjoint p f.ker
rw₅ rw₆ : p ⊓ f.ker = ⊥ ↔ p ⊓ f.ker = ⊥
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker

Tactic:
rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]

Premises used: LinearMap.ker_eq_bot, disjoint_iff, LinearMap.ker_domRestrict, LinearMap.ker_restrict, LinearMap.injective_domRestrict_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 : CommSemiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ f.ker ≤ (c • f).ker

Tactic:
simpa only [ker] using Submodule.comap_le_comap_smul _ _ _

Premises used: Submodule.comap_le_comap_smul, LinearMap.ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
K : Type u_4
V : Type u_9
V₂ : Type u_10
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
a : K
h : a ≠ 0
⊢ (a • f).ker = f.ker

Tactic:
Submodule.comap_smul f _ a h

Premises used: Submodule.comap_smul, LinearMap.ker
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
K : Type u_4
V : Type u_9
V₂ : Type u_10
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ (a • f).ker = ⨅ (_ : a ≠ 0), f.ker

Tactic:
Submodule.comap_smul' f _ a

Premises used: LinearMap.ker, Submodule.comap_smul'
-- 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₂
⊢ comap f ⊥ = f.ker

Tactic:
rfl

Premises used: LinearMap.ker, rfl
-- 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
p : Submodule R M
⊢ p.subtype.ker = ⊥

Tactic:
ker_eq_bot_of_injective fun _ _ => Subtype.ext

Premises used: LinearMap.ker_eq_bot_of_injective, Subtype.ext
-- 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
p p' : Submodule R M
h : p ≤ p'
rw : (codRestrict p' p.subtype ⋯).ker = ⊥
rw₁ : p.subtype.ker = ⊥
rw₂ rw₃ : Eq.{u_5 + 1} (α := Submodule R ↥p) ⊥ ⊥
⊢ (inclusion h).ker = ⊥

Tactic:
rw [inclusion, ker_codRestrict, ker_subtype]

Premises used: Submodule.ker_subtype, LinearMap.ker_codRestrict, Submodule.inclusion