awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
rw₁ :
  HSMul.hSMul (β := S) b ((f : (a : M₁) → S) y : S) • x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) b : R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x)
have rw₂ : b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x =
  b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
Tactic: rw [RingHom.id_apply, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
⊢ Eq (α := M₁ →ₗ[R] M) (f.smulRight 0) 0
have h : ∀ (x : M₁), Eq.{u_4 + 1} (α := M) ((f.smulRight 0 : (a : M₁) → M) x : M) ((0 : (a : M₁) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
x : M
⊢ Eq (α := M₁ →ₗ[R] M) (smulRight.{u_1, u_3, u_4, u_5} (S := S) 0 x) 0
have h : ∀ (x_1 : M₁),
  Eq.{u_4 + 1} (α := M) ((smulRight.{u_1, u_3, u_4, u_5} (S := S) 0 x : (a : M₁) → M) x_1 : M)
    ((0 : (a : M₁) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
m m' : M
⊢ f.smulRight (m + m') = HAdd.hAdd (α := M₂ →ₗ[R] M) (f.smulRight m) (f.smulRight m')
have h : ∀ (x : M₂),
  Eq.{u_4 + 1} (α := M) ((f.smulRight (m + m') : (a : M₂) → M) x : M)
    ((HAdd.hAdd (α := M₂ →ₗ[R] M) (f.smulRight m) (f.smulRight m') : (a : M₂) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
⊢ f.smulRight (c • m) = HSMul.hSMul (α := R) (β := M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R) (f.smulRight m)
have h : ∀ (x : M₂),
  Eq.{u_4 + 1} (α := M) ((f.smulRight (c • m) : (a : M₂) → M) x : M)
    ((HSMul.hSMul (α := R) (β := M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R) (f.smulRight m) : (a : M₂) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
⊢ { toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] M₂ →ₗ[R] M) { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
      { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
have h : ∀ (x : M) (x_1 : M₂),
  Eq.{u_4 + 1} (α := M)
    (((({ toFun := (f + f').smulRight, map_add' := sorry, map_smul' := sorry } : (a : M) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)
    ((((HAdd.hAdd (α := M →ₗ[R] M₂ →ₗ[R] M) { toFun := f.smulRight, map_add' := sorry, map_smul' := sorry : M →ₗ[R] M₂ →ₗ[R] M }
                  { toFun := f'.smulRight, map_add' := sorry, map_smul' := sorry : M →ₗ[R] M₂ →ₗ[R] M } :
                (a : M) → M₂ →ₗ[R] M)
              x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
⊢ { toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := M →ₗ[R] M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R)
      { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
have h : ∀ (x : M) (x_1 : M₂),
  Eq.{u_4 + 1} (α := M)
    (((({ toFun := (c • f).smulRight, map_add' := sorry, map_smul' := sorry } : (a : M) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)
    ((((HSMul.hSMul (α := R) (β := M →ₗ[R] M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R)
                  { toFun := f.smulRight, map_add' := sorry, map_smul' := sorry : M →ₗ[R] M₂ →ₗ[R] M } :
                (a : M) → M₂ →ₗ[R] M)
              x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_9
M : Type u_10
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
⊢ Commute LinearMap.id f
have h : ∀ (x : M), Eq (α := M) ((LinearMap.id * f : (a : M) → M) x : M) ((f * LinearMap.id : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_9
M : Type u_10
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
⊢ Commute f LinearMap.id
have h : ∀ (x : M), Eq (α := M) ((f * LinearMap.id : (a : M) → M) x : M) ((LinearMap.id * f : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : AddCommMonoid V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
h : u.HasNoetherianRange
v : V₂ →ₗ[K] V₃
⊢ (v ∘ₗ u).HasNoetherianRange
have rw : ∀ (h : IsNoetherian.{u_1, u_4} K ↥u.range) (v : V₂ →ₗ[K] V₃), IsNoetherian.{u_1, u_6} K ↥(map v u.range)
Tactic: rw [LinearMap.HasNoetherianRange, LinearMap.range_comp] at *
Cleared hypotheses: h, v
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : AddCommMonoid V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
h : u.HasFiniteRange
v : V₂ →ₗ[K] V₃
⊢ (v ∘ₗ u).HasFiniteRange
have rw : ∀ (h : u.range.FG) (v : V₂ →ₗ[K] V₃), (map v u.range).FG
Tactic: rw [LinearMap.HasFiniteRange, LinearMap.range_comp] at *
Cleared hypotheses: h, v
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (hypothesis)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u : V →ₗ[K] V₂
h : u.HasFiniteRange
⊢ IsNoetherian.{u_1, u_4} K ↥u.range
have this : Module.Finite.{u_1, u_4} K ↥u.range
Tactic: have := Finite.of_fg h.fg_range
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
v : V₂ →ₗ[K] V₃
h : v.HasNoetherianRange
u : V →ₗ[K] V₂
⊢ (v ∘ₗ u).HasNoetherianRange
have rw : ∀ (h : IsNoetherian.{u_1, u_6} K ↥v.range) (u : V →ₗ[K] V₂), IsNoetherian.{u_1, u_6} K ↥(map v u.range)
Tactic: rw [HasNoetherianRange, LinearMap.range_comp] at *
Cleared hypotheses: h, u
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
⊢ (-f).HasNoetherianRange
have rwa : IsNoetherian.{u_1, u_4} K ↥(-f).range
Tactic: rwa [HasNoetherianRange, LinearMap.range_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
rwa : IsNoetherian.{u_1, u_4} K ↥(-f).range
⊢ (-f).HasNoetherianRange
have rwa₁ : IsNoetherian.{u_1, u_4} K ↥f.range
Tactic: rwa [HasNoetherianRange, LinearMap.range_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasFiniteRange
⊢ (-f).HasFiniteRange
have rwa : (-f).range.FG
Tactic: rwa [HasFiniteRange, LinearMap.range_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasFiniteRange
rwa : (-f).range.FG
⊢ (-f).HasFiniteRange
have rwa₁ : f.range.FG
Tactic: rwa [HasFiniteRange, LinearMap.range_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (hypothesis)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f g : V →ₗ[K] V₂
hf : f.HasNoetherianRange
hg : g.HasNoetherianRange
⊢ (f + g).HasNoetherianRange
have hf₁ : IsNoetherian.{u_1, u_4} K ↥f.range
Tactic: rw [HasNoetherianRange] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (hypothesis)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f g : V →ₗ[K] V₂
hf : f.HasNoetherianRange
hg : g.HasNoetherianRange
hf₁ : IsNoetherian.{u_1, u_4} K ↥f.range
⊢ (f + g).HasNoetherianRange
have hg₁ : IsNoetherian.{u_1, u_4} K ↥g.range
Tactic: rw [HasNoetherianRange] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
f : V →ₗ[K] V₂
⊢ Membership.mem (γ := Submodule K (V →ₗ[K] V₂)) (finiteRange K V V₂) f ↔ f.HasFiniteRange
have rw : f.HasNoetherianRange ↔ f.HasFiniteRange
Tactic: rw [mem_finiteRange_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
f : V →ₗ[K] V₂
rw : f.HasNoetherianRange ↔ f.HasFiniteRange
⊢ Membership.mem (γ := Submodule K (V →ₗ[K] V₂)) (finiteRange K V V₂) f ↔ f.HasFiniteRange
have rw₁ : f.HasFiniteRange ↔ f.HasFiniteRange
Tactic: rw [mem_finiteRange_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u - v).HasFiniteRange
have rw : (u - v).HasNoetherianRange ↔ (u - v).HasFiniteRange
Tactic: rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
rw : (u - v).HasNoetherianRange ↔ (u - v).HasFiniteRange
⊢ u ≈ v ↔ (u - v).HasFiniteRange
have rw₁ : (u - v).HasFiniteRange ↔ (u - v).HasFiniteRange
Tactic: rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
have rw : (u - v).HasNoetherianRange ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
Tactic: rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
rw : (u - v).HasNoetherianRange ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
⊢ u ≈ v ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
have rw₁ : IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker) ↔
  IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
Tactic: rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
rw : (u - v).HasNoetherianRange ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
rw₁ :
  IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker) ↔
    IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
⊢ u ≈ v ↔ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
have rw₂ : IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker) ↔ IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker)
Tactic: rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ CoFG (eqLocus u v)
have rw : u ≈ v ↔ (u - v).ker.CoFG
Tactic: rw [eqLocus_eq_ker_sub, ker_coFG_iff_hasFiniteRange, equiv_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
rw : u ≈ v ↔ (u - v).ker.CoFG
⊢ u ≈ v ↔ CoFG (eqLocus u v)
have rw₁ : u ≈ v ↔ (u - v).HasFiniteRange
Tactic: rw [eqLocus_eq_ker_sub, ker_coFG_iff_hasFiniteRange, equiv_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
rw : u ≈ v ↔ (u - v).ker.CoFG
rw₁ : u ≈ v ↔ (u - v).HasFiniteRange
⊢ u ≈ v ↔ CoFG (eqLocus u v)
have rw₂ : (u - v).HasFiniteRange ↔ (u - v).HasFiniteRange
Tactic: rw [eqLocus_eq_ker_sub, ker_coFG_iff_hasFiniteRange, equiv_iff_hasFiniteRange]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (hypothesis)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
⊢ u ≈ v
have A_le : A ≤ eqLocus u v
Tactic: have A_le : A ≤ eqLocus u v := le_eqLocus.mpr eqOn_A
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
A_le : A ≤ eqLocus u v
⊢ u ≈ v
have rw : IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
Tactic: rw [equiv_iff_isNoetherian_quotient_eqLocus]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : v ≈ v'
⊢ v ∘ₗ u ≈ v' ∘ₗ u
have rw : ∀ (h' : (v - v').HasNoetherianRange), (v ∘ₗ u - v' ∘ₗ u).HasNoetherianRange
Tactic: rw [equiv_iff_hasNoetherianRange] at *
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : u ≈ v
⊢ u' ∘ₗ u ≈ u' ∘ₗ v
have rw : ∀ (h : (u - v).HasNoetherianRange), (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange
Tactic: rw [equiv_iff_hasNoetherianRange] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' v' : V₂ →ₗ[K] V₃
h : u ≈ v
h' : u' ≈ v'
⊢ u' ∘ₗ u ≈ v' ∘ₗ v
have grw : v' ∘ₗ u ≈ v' ∘ₗ v
Tactic: grw [equiv_comp_right h', equiv_comp_left h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.FiniteRange (goal)
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' v' : V₂ →ₗ[K] V₃
h : u ≈ v
h' : u' ≈ v'
grw : v' ∘ₗ u ≈ v' ∘ₗ v
⊢ u' ∘ₗ u ≈ v' ∘ₗ v
have grw₁ : (setoid : (V →ₗ[K] V₃) → (V →ₗ[K] V₃) → Prop) (v' ∘ₗ v) (v' ∘ₗ v)
Tactic: grw [equiv_comp_right h', equiv_comp_left h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
⊢ IsHomogeneous (M.toMvPolynomial i) 1
have h : ∀ (i_1 : n),
  Membership.mem (γ := Finset n) Finset.univ i_1 →
    IsHomogeneous.{u_2, u_4} (σ := n) (R := R)
      ((monomial (Finsupp.single i_1 1) : (a : R) → MvPolynomial n R) (M i i_1)) 1
Tactic: apply MvPolynomial.IsHomogeneous.sum
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ IsHomogeneous.{u_2, u_4} (σ := n) (R := R) ((monomial (Finsupp.single j 1) : (a : R) → MvPolynomial n R) (M i j)) 1
have apply : Eq (α := ℕ) ((Finsupp.degree : (a : n →₀ ℕ) → ℕ) (Finsupp.single j 1) : ℕ) (1 : ℕ)
Tactic: apply MvPolynomial.isHomogeneous_monomial _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
⊢ Eq (α := (i : m) → MvPolynomial n R) (toMvPolynomial 0) 0
have h : ∀ (x : m) (m_1 : n →₀ ℕ), Eq.{u_4 + 1} (α := R) (coeff m_1 (toMvPolynomial 0 x)) (coeff m_1 (0 x))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
⊢ Eq (α := (i : n) → MvPolynomial n R) (toMvPolynomial 1) X
have h : ∀ (i : n), Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
⊢ Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)
have h : Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) (X i)
Tactic: rw [toMvPolynomial, Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
h : Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) (X i)
⊢ Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)
have h₁ : ∀ (b : n),
  Membership.mem (γ := Finset n) Finset.univ b →
    b ≠ i → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single b 1) : (a : R) → MvPolynomial n R) (1 i b)) 0
Tactic: rw [toMvPolynomial, Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
h : Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) (X i)
h₁ :
  ∀ (b : n),
    Membership.mem (γ := Finset n) Finset.univ b →
      b ≠ i → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single b 1) : (a : R) → MvPolynomial n R) (1 i b)) 0
⊢ Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)
have h₂ : i ∉ Finset.univ → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) 0
Tactic: rw [toMvPolynomial, Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M N : Matrix m n R
⊢ (M + N).toMvPolynomial = HAdd.hAdd (α := (i : m) → MvPolynomial n R) M.toMvPolynomial N.toMvPolynomial
have h : ∀ (i : m),
  (M + N).toMvPolynomial i =
    HAdd.hAdd (α := (i : m) → MvPolynomial n R) (β := (i : m) → MvPolynomial n R) M.toMvPolynomial N.toMvPolynomial i
Tactic: ext i : 1