awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ m = 0
have rw₃ : Eq.{u_5 + 1} (α := M) ((g : (a : M₂) → M) 0 : M) (0 : M)
Tactic: rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ m = 0
have rw₄ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ p ≤ f.ker ↔ map f p = ⊥
have rw : p ≤ comap f ⊥ ↔ map f p = ⊥
Tactic: rw [ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 = ⊥
⊢ p ≤ f.ker ↔ map f p = ⊥
have rw₁ : p ≤ comap f ⊥ ↔ map f p ≤ ⊥
Tactic: rw [ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 ≤ ⊥
⊢ p ≤ f.ker ↔ map f p = ⊥
have rw₂ : p ≤ comap f ⊥ ↔ p ≤ comap f ⊥
Tactic: rw [ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂)
⊢ (codRestrict p f hf).ker = f.ker
have rw : comap f ⊥ = f.ker
Tactic: rw [ker, comap_codRestrict, Submodule.map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂)
⊢ (f.restrict hf).ker = comap p.subtype f.ker
have rw : (codRestrict q (f.domRestrict p) sorry).ker = comap p.subtype f.ker
Tactic: rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ (f.restrict hf).ker = comap p.subtype f.ker
have rw₁ : (f.domRestrict p).ker = comap p.subtype f.ker
Tactic: rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ (f.restrict hf).ker = comap p.subtype f.ker
have rw₂ : comap p.subtype f.ker = comap p.subtype f.ker
Tactic: rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂
⊢ Eq (α := LinearMap.{u_1, u_2, u_5, u_7} τ₁₂ (↥f.ker) M₂) (f.domRestrict f.ker) 0
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 = ⊤
⊢ ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0
have contrapose! : ∀ (h : ∀ (m : Submodule R M) (_ : m ∈ s), f ∘ₛₗ m.subtype = 0), f = 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂)
⊢ f.ker = ⊥
have rw : f.ker ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) m) x
have obtain : ∀ (c : ℕ) (w : n ≤ n + c), Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
Tactic: obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
Cleared hypotheses: m, w
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have 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
Tactic: rw [LinearMap.mem_ker] at h
Cleared hypotheses: h, c, w
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw : Eq (α := M) ((f ^ (n + c) : (a : M) → M) x : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw₁ : Eq (α := M) ((f ^ (c + n) : (a : M) → M) x : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw₂ : Eq (α := M) ((f ^ c * f ^ n : (a : M) → M) x : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw₃ : Eq (α := M) ((f ^ c : (a : M) → M) ((f ^ n : (a : M) → M) x : M) : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw₄ : Eq (α := M) ((f ^ c : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (f ^ n).ker) (n + c)) x
have rw₅ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 = f.ker
have h : ∀ (x : M), x ∈ (-f).ker ↔ x ∈ f.ker
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ x - y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
have 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₂)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂)
⊢ x - y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
have 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₂)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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₂)
⊢ x - y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)
have 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₂)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Disjoint p f.ker ↔ Set.InjOn.{u_5, u_7} (β := M₂) (⇑f : (a : M) → M₂) (↑p : Set M)
have 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)
Tactic: rw [disjoint_ker, Set.injOn_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Disjoint p f.ker ↔ Set.InjOn.{u_5, u_7} (β := M₂) (⇑f : (a : M) → M₂) (↑p : Set M)
have 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
Tactic: rw [disjoint_ker, Set.injOn_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Injective.{u_5 + 1, u_7 + 1} (α := ↥S) (β := M₂) (⇑(f.domRestrict S) : (a : ↥S) → M₂) ↔ S ⊓ f.ker = ⊥
have rw : (f.domRestrict S).ker = ⊥ ↔ S ⊓ f.ker = ⊥
Tactic: rw [← LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 = ⊥
have refine_1 : ∀ (h : (f.domRestrict S).ker = ⊥), S ⊓ f.ker ≤ ⊥
Tactic: refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 ≤ ⊥
⊢ (f.domRestrict S).ker = ⊥ ↔ S ⊓ f.ker = ⊥
have refine_2 : ∀ (h : S ⊓ f.ker = ⊥), (f.domRestrict S).ker ≤ ⊥
Tactic: refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ x ∈ S ⊓ f.ker → Membership.mem (γ := Submodule R M) ⊥ x
have refine_1 : ∀ (hx : x ∈ (↑S : Set M)) (h'x : x ∈ (↑f.ker : Set M)), Membership.mem (γ := Submodule R M) ⊥ x
Tactic: ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (hypothesis)
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 M) ⊥ x
have this₁ : Membership.mem (γ := Submodule R ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (hypothesis)
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
⊢ Membership.mem (γ := Submodule R ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)
have this : x ∈ S ⊓ f.ker
Tactic: have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (hypothesis)
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 ↥S) ⊥ (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx)
have this₁ : Membership.mem (γ := Submodule R M) ⊥ x
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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)
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]