awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
h :
  ∀ (x : M) (x_1 : M₂),
    Eq.{u_4 + 1} (α := M)
      (((({ toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } : (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' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M } :
                  (a : M) → M₂ →ₗ[R] M)
                x :
              M₂ →ₗ[R] M) :
            (a : M₂) → M)
          x_1 :
        M)
⊢ { 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 }

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
x : M
x_1 : M₂
⊢ Eq.{u_4 + 1} (α := M)
    (((({ toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } : (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' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M } :
                (a : M) → M₂ →ₗ[R] M)
              x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)

Tactic:
apply mul_smul

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M₂ →ₗ[R] R
x : M
⊢ Eq (α := M₂ →ₗ[R] M)
    ((((smulRightₗ : (a : M₂ →ₗ[R] R) → M →ₗ[R] M₂ →ₗ[R] M) f : M →ₗ[R] M₂ →ₗ[R] M) : (a : M) → M₂ →ₗ[R] M) x :
      M₂ →ₗ[R] M)
    (f.smulRight x : M₂ →ₗ[R] M)

Tactic:
rfl

Premises used: LinearMap.smulRight, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M₂ →ₗ[R] R
x : M
y : M₂
⊢ (((((smulRightₗ : (a : M₂ →ₗ[R] R) → M →ₗ[R] M₂ →ₗ[R] M) f : M →ₗ[R] M₂ →ₗ[R] M) : (a : M) → M₂ →ₗ[R] M) x :
          M₂ →ₗ[R] M) :
        (a : M₂) → M)
      y =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((f : (a : M₂) → R) y : R) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
h : ∀ (x : M), Eq (α := M) ((LinearMap.id * f : (a : M) → M) x : M) ((f * LinearMap.id : (a : M) → M) x : M)
⊢ Commute LinearMap.id f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
x : M
⊢ Eq (α := M) ((LinearMap.id * f : (a : M) → M) x : M) ((f * LinearMap.id : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
h : ∀ (x : M), Eq (α := M) ((f * LinearMap.id : (a : M) → M) x : M) ((LinearMap.id * f : (a : M) → M) x : M)
⊢ Commute f LinearMap.id

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
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
x : M
⊢ Eq (α := M) ((f * LinearMap.id : (a : M) → M) x : M) ((LinearMap.id * f : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
⊢ f.HasNoetherianRange ↔ IsNoetherian.{u_1, u_4} K ↥f.range

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.HasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
⊢ f.HasFiniteRange ↔ f.range.FG

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.HasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
u : V →ₗ[K] V₂
h : u.HasNoetherianRange
⊢ u.HasFiniteRange

Tactic:
have := h.isNoetherian_range; FG.of_finite

Premises used: LinearMap.HasFiniteRange, Submodule.FG.of_finite, LinearMap.HasNoetherianRange.isNoetherian_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
⊢ HasNoetherianRange.{u_1, u_2, u_4} (K := K) (V := V) (V₂ := V₂) 0

Tactic:
simp [HasNoetherianRange, isNoetherian_submodule, Submodule.fg_bot]

Premises used: isNoetherian_submodule, LinearMap.HasNoetherianRange, Submodule.fg_bot
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
⊢ HasFiniteRange.{u_1, u_2, u_4} (K := K) (V := V) (V₂ := V₂) 0

Tactic:
HasNoetherianRange.zero.hasFiniteRange

Premises used: LinearMap.HasNoetherianRange.hasFiniteRange, LinearMap.HasNoetherianRange.zero
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₃
rw : ∀ (h : IsNoetherian.{u_1, u_4} K ↥u.range) (v : V₂ →ₗ[K] V₃), IsNoetherian.{u_1, u_6} K ↥(map v u.range)
⊢ (v ∘ₗ u).HasNoetherianRange

Tactic:
rw [LinearMap.HasNoetherianRange, LinearMap.range_comp] at *

Premises used: LinearMap.HasNoetherianRange, LinearMap.range_comp
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 : IsNoetherian.{u_1, u_4} K ↥u.range
v : V₂ →ₗ[K] V₃
⊢ IsNoetherian.{u_1, u_6} K ↥(map v u.range)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₃
rw : ∀ (h : u.range.FG) (v : V₂ →ₗ[K] V₃), (map v u.range).FG
⊢ (v ∘ₗ u).HasFiniteRange

Tactic:
rw [LinearMap.HasFiniteRange, LinearMap.range_comp] at *

Premises used: LinearMap.range_comp, LinearMap.HasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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.range.FG
v : V₂ →ₗ[K] V₃
⊢ (map v u.range).FG

Tactic:
Submodule.FG.map v h

Premises used: Submodule.FG.map
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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.range.FG
v : V₂ →ₗ[K] V₃
⊢ (map v u.range).FG

Tactic:
exact Submodule.FG.map v h

Premises used: Submodule.FG.map
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : IsNoetherian K V
f : V →ₗ[K] V₂
⊢ f.HasNoetherianRange

Tactic:
hasNoetherianRange_iff_range.mpr inferInstance

Premises used: Iff.mpr, inferInstance, LinearMap.hasNoetherianRange_iff_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : Module.Finite K V
f : V →ₗ[K] V₂
⊢ f.HasFiniteRange

Tactic:
simp [HasFiniteRange]

Premises used: LinearMap.HasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : IsNoetherian K V₂
f : V →ₗ[K] V₂
⊢ f.HasNoetherianRange

Tactic:
hasNoetherianRange_iff_range.mpr inferInstance

Premises used: Iff.mpr, inferInstance, LinearMap.hasNoetherianRange_iff_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : Semiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
inst_5 : IsNoetherian K V₂
f : V →ₗ[K] V₂
⊢ f.HasFiniteRange

Tactic:
HasNoetherianRange.of_isNoetherian_rng.hasFiniteRange

Premises used: LinearMap.HasNoetherianRange.hasFiniteRange, LinearMap.HasNoetherianRange.of_isNoetherian_rng
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
⊢ Module.Finite.{u_1, u_4} K ↥u.range

Tactic:
have := Finite.of_fg h.fg_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
this : Module.Finite.{u_1, u_4} K ↥u.range
⊢ IsNoetherian.{u_1, u_4} K ↥u.range

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
⊢ u.HasNoetherianRange ↔ u.HasFiniteRange

Tactic:
⟨HasNoetherianRange.hasFiniteRange, HasFiniteRange.hasNoetherianRange⟩

Premises used: LinearMap.HasNoetherianRange.hasFiniteRange, LinearMap.HasFiniteRange.hasNoetherianRange, Iff.intro
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
rw : ∀ (h : IsNoetherian.{u_1, u_6} K ↥v.range) (u : V →ₗ[K] V₂), IsNoetherian.{u_1, u_6} K ↥(map v u.range)
⊢ (v ∘ₗ u).HasNoetherianRange

Tactic:
rw [HasNoetherianRange, LinearMap.range_comp] at *

Premises used: LinearMap.HasNoetherianRange, LinearMap.range_comp
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 : IsNoetherian.{u_1, u_6} K ↥v.range
u : V →ₗ[K] V₂
⊢ IsNoetherian.{u_1, u_6} K ↥(map v u.range)

Tactic:
isNoetherian_of_le map_le_range

Premises used: isNoetherian_of_le, LinearMap.map_le_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 : IsNoetherian.{u_1, u_6} K ↥v.range
u : V →ₗ[K] V₂
⊢ IsNoetherian.{u_1, u_6} K ↥(map v u.range)

Tactic:
exact isNoetherian_of_le map_le_range

Premises used: isNoetherian_of_le, LinearMap.map_le_range
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₃
inst_7 : IsNoetherianRing K
v : V₂ →ₗ[K] V₃
h : v.HasFiniteRange
u : V →ₗ[K] V₂
⊢ (v ∘ₗ u).HasFiniteRange

Tactic:
h.hasNoetherianRange.comp_right _ |>.hasFiniteRange

Premises used: LinearMap.HasNoetherianRange.hasFiniteRange, LinearMap.HasFiniteRange.hasNoetherianRange, LinearMap.HasNoetherianRange.comp_right
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
rwa₁ rwa₂ rwa₃ rwa₄ : IsNoetherian.{u_1, u_4} K ↥f.range
⊢ (-f).HasNoetherianRange

Tactic:
rwa [HasNoetherianRange, LinearMap.range_neg]

Premises used: LinearMap.range_neg, LinearMap.HasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
rwa₁ rwa₂ rwa₃ rwa₄ : f.range.FG
⊢ (-f).HasFiniteRange

Tactic:
rwa [HasFiniteRange, LinearMap.range_neg]

Premises used: LinearMap.range_neg, LinearMap.HasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
⊢ IsNoetherian.{u_1, u_4} K ↥f.range

Tactic:
rw [HasNoetherianRange] at *

Premises used: LinearMap.HasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
⊢ IsNoetherian.{u_1, u_4} K ↥g.range

Tactic:
rw [HasNoetherianRange] at *

Premises used: LinearMap.HasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 : IsNoetherian.{u_1, u_4} K ↥f.range
hg : IsNoetherian.{u_1, u_4} K ↥g.range
⊢ IsNoetherian.{u_1, u_4} K ↥(f + g).range

Tactic:
isNoetherian_of_le (range_add_le f g)

Premises used: isNoetherian_of_le, LinearMap.range_add_le
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 : IsNoetherian.{u_1, u_4} K ↥f.range
hg : IsNoetherian.{u_1, u_4} K ↥g.range
⊢ IsNoetherian.{u_1, u_4} K ↥(f + g).range

Tactic:
exact isNoetherian_of_le (range_add_le f g)

Premises used: isNoetherian_of_le, LinearMap.range_add_le
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
f g : V →ₗ[K] V₂
hf : f.HasFiniteRange
hg : g.HasFiniteRange
⊢ (f + g).HasFiniteRange

Tactic:
hf.hasNoetherianRange.add hg.hasNoetherianRange |>.hasFiniteRange

Premises used: LinearMap.HasNoetherianRange.hasFiniteRange, LinearMap.HasFiniteRange.hasNoetherianRange, LinearMap.HasNoetherianRange.add
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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

Tactic:
sub_eq_add_neg f g ▸ hf.add hg.neg

Premises used: sub_eq_add_neg, Eq.rec, LinearMap.HasNoetherianRange.neg, LinearMap.HasNoetherianRange.add, Eq.symm
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
f g : V →ₗ[K] V₂
hf : f.HasFiniteRange
hg : g.HasFiniteRange
⊢ (f - g).HasFiniteRange

Tactic:
sub_eq_add_neg f g ▸ hf.add hg.neg

Premises used: LinearMap.HasFiniteRange.add, sub_eq_add_neg, Eq.rec, LinearMap.HasFiniteRange.neg, Eq.symm
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
⊢ f.HasNoetherianRange ↔ IsNoetherian.{u_1, u_2} K (V ⧸ f.ker)

Tactic:
f.quotKerEquivRange.isNoetherian_iff.symm

Premises used: LinearEquiv.isNoetherian_iff, LinearMap.HasNoetherianRange, LinearMap.quotKerEquivRange, Iff.symm
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
⊢ f.ker.CoFG ↔ f.HasFiniteRange

Tactic:
range_fg_iff_ker_cofg.symm

Premises used: Submodule.range_fg_iff_ker_cofg, LinearMap.HasFiniteRange, Iff.symm
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
c : K
⊢ (c • f).HasNoetherianRange

Tactic:
hf.comp_left (lsmul K V₂ c)

Premises used: LinearMap.lsmul, LinearMap.HasNoetherianRange.comp_left, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
f : V →ₗ[K] V₂
hf : f.HasFiniteRange
c : K
⊢ (c • f).HasFiniteRange

Tactic:
hf.comp_left (lsmul K V₂ c)

Premises used: LinearMap.lsmul, LinearMap.HasFiniteRange.comp_left, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V' : Type u_3
V₂ : Type u_4
V₂' : Type u_5
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₃
a b : V →ₗ[K] V₂
hu : Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} a
hv : Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} b
⊢ Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} (a + b)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V' : Type u_3
V₂ : Type u_4
V₂' : Type u_5
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₃
⊢ Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V' : Type u_3
V₂ : Type u_4
V₂' : Type u_5
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₃
c : K
hu : V →ₗ[K] V₂
⊢ Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} hu →
    Membership.mem (γ := Set (V →ₗ[K] V₂)) {u : V →ₗ[K] V₂ | u.HasNoetherianRange} (c • hu)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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₂
f : V →ₗ[K] V₂
⊢ Membership.mem (γ := Submodule K (V →ₗ[K] V₂)) (finiteRange K V V₂) f ↔ f.HasNoetherianRange

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, LinearMap.HasNoetherianRange, setOf
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
rw₁ rw₂ : f.HasFiniteRange ↔ f.HasFiniteRange
⊢ Membership.mem (γ := Submodule K (V →ₗ[K] V₂)) (finiteRange K V V₂) f ↔ f.HasFiniteRange

Tactic:
rw [mem_finiteRange_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]

Premises used: LinearMap.mem_finiteRange_iff_hasNoetherianRange, LinearMap.hasNoetherianRange_iff_hasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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 ↔ (u - v).HasNoetherianRange

Tactic:
Submodule.quotientRel_def _

Premises used: Submodule.quotientRel_def, Set.Mem, LinearMap.HasNoetherianRange, setOf
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
rw₁ rw₂ : (u - v).HasFiniteRange ↔ (u - v).HasFiniteRange
⊢ u ≈ v ↔ (u - v).HasFiniteRange

Tactic:
rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]

Premises used: LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange, LinearMap.hasNoetherianRange_iff_hasFiniteRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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))
rw₂ rw₃ : IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker) ↔ IsNoetherian.{u_1, u_2} K (V ⧸ (u - v).ker)
⊢ u ≈ v ↔ 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]

Premises used: LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange, LinearMap.hasNoetherianRange_iff_quotient_ker, LinearMap.eqLocus_eq_ker_sub
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
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
rw₂ rw₃ : (u - v).HasFiniteRange ↔ (u - v).HasFiniteRange
⊢ u ≈ v ↔ CoFG (eqLocus u v)

Tactic:
rw [eqLocus_eq_ker_sub, ker_coFG_iff_hasFiniteRange, equiv_iff_hasFiniteRange]

Premises used: LinearMap.eqLocus_eq_ker_sub, LinearMap.FiniteRangeSetoid.equiv_iff_hasFiniteRange, LinearMap.ker_coFG_iff_hasFiniteRange