awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.NilpotentKer
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ
    (↑(quotTensorEquivQuotSMul (↥(I ^ n)) I) : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] ↥(I ^ n) ⧸ I • ⊤)
e_3 : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring
e_4 :
  Eq.{u_2 + 1} (α := AddCommMonoid (S ⧸ I ^ (n + 1))) AddCommGroup.toAddCommMonoid
    (Submodule.Quotient.addCommMonoid (I ^ (n + 1)))
e_5 :
  HEq (α := Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1))) (β :=
    Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1)))
h : φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)
⊢ Eq (α := Submodule R (S ⧸ I ^ (n + 1)))
    (⊤ ⊓
      LinearMap.ker
        ((↑R :
            {S M M₂ : Type u_2} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          φ.toLinearMap))
    (Submodule.map
      ((↑R :
          {S M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        ψ)
      ⊤)

Tactic:
suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
-- Module: Mathlib.RingTheory.Finiteness.NilpotentKer
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ
    (↑(quotTensorEquivQuotSMul (↥(I ^ n)) I) : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] ↥(I ^ n) ⧸ I • ⊤)
e_3 : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring
e_4 :
  Eq.{u_2 + 1} (α := AddCommMonoid (S ⧸ I ^ (n + 1))) AddCommGroup.toAddCommMonoid
    (Submodule.Quotient.addCommMonoid (I ^ (n + 1)))
e_5 :
  HEq (α := Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1))) (β :=
    Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1)))
h :
  Submodule.comap (Submodule.mkQ (I ^ (n + 1))) φ.toLinearMap.ker =
    Submodule.comap (R₂ := S) (M₂ := S ⧸ I ^ (n + 1)) (σ₁₂ := RingHom.id S) (Submodule.mkQ (I ^ (n + 1)))
      (Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n))
⊢ φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)

Tactic:
apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective

Premises used: Submodule.comap_injective_of_surjective, HPow.hPow, HAdd.hAdd, Submodule.mkQ_surjective, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.NilpotentKer
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
zero : Module.Finite.{u_1, u_2} R (S ⧸ HPow.hPow (β := ℕ) I 0)
succ : ∀ (n : ℕ) (IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)), Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)

Tactic:
induction n with
  | zero => rw [pow_zero, Ideal.one_eq_top]; infer_instance
  | succ n IH =>
    let φ : (S ⧸ I ^ (n + 1)) →ₐ[S] S ⧸ I ^ n :=
      Ideal.Quotient.factorₐ _ (Ideal.pow_le_pow_right n.le_succ)
    have hφ : Function.Surjective φ :=
      Ideal.Quotient.factor_surjective (Ideal.pow_le_pow_right n.le_succ)
    have hφ' : φ.toLinearMap ∘ₗ (I ^ (n + 1)).mkQ = (I ^ n).mkQ := rfl
    refine ⟨Submodule.fg_of_fg_map_of_fg_inf_ker (φ.toLinearMap.restrictScalars R) ?_ ?_⟩
    · simpa [LinearMap.range_eq_top_of_surjective (φ.toLinearMap.restrictScalars R) hφ] using
        Module.Finite.fg_top
    · have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
        exact .trans (S ⧸ I) _
      let ψ : (S ⧸ I) ⊗[S] ↑(I ^ n) →ₗ[S] (S ⧸ I ^ (n + 1)) := by
        refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_left (I := I) (J := I ^ n)
      convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1
      suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
      apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective
      simpa [← LinearMap.ker_comp, hφ'] using Ideal.pow_le_pow_right n.le_succ

Premises used: Module.Finite.fg_top, Ideal.one_eq_top, LinearMap.ker_comp, Nat.le_succ, Submodule.comap_injective_of_surjective, pow_zero, Ideal.pow_le_pow_right, HPow.hPow, HAdd.hAdd, Submodule.mkQ_surjective, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Type u_3
inst_3 : AddCommMonoid P
inst_4 : Module R P
sb : Submodule R M
sc : Submodule R P
hsb : sb.FG
hsc : sc.FG
tb : Set M
htb : tb.Finite ∧ span R tb = sb
tc : Set P
htc : tc.Finite ∧ span R tc = sc
rw : Submodule.prod (span R tb) (span R tc) = sb.prod sc
rw₁ : sb.prod (span R tc) = sb.prod sc
rw₂ rw₃ : sb.prod sc = sb.prod sc
⊢ span R ((⇑(LinearMap.inl R M P) : (a : M) → M × P) '' tb ∪ (⇑(LinearMap.inr R M P) : (a : P) → M × P) '' tc) =
    sb.prod sc

Tactic:
rw [LinearMap.span_inl_union_inr, htb.2, htc.2]

Premises used: LinearMap.span_inl_union_inr, And.right
-- Module: Mathlib.RingTheory.Finiteness.Prod
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
rw : Submodule.FG (R := R) (M := M × N) (Submodule.prod ⊤ ⊤)
⊢ Submodule.FG (R := R) (M := M × N) ⊤

Tactic:
rw [← Submodule.prod_top]

Premises used: Submodule.prod_top
-- Module: Mathlib.RingTheory.Finiteness.Prod
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
⊢ Submodule.FG (R := R) (M := M × N) (Submodule.prod ⊤ ⊤)

Tactic:
hM.1.prod hN.1

Premises used: Module.Finite.fg_top, Submodule.FG.prod
-- Module: Mathlib.RingTheory.Finiteness.Prod
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
⊢ Submodule.FG (R := R) (M := M × N) (Submodule.prod ⊤ ⊤)

Tactic:
exact hM.1.prod hN.1

Premises used: Module.Finite.fg_top, Submodule.FG.prod
-- Module: Mathlib.RingTheory.Finiteness.Projective
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Projective R M
⊢ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : M →ₗ[R] Fin n → R),
    Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M) ∧
      Function.Injective.{u_2 + 1, u_1 + 1} (α := M) (β := Fin n → R) (⇑g : (a : M) → Fin n → R) ∧ f ∘ₗ g = LinearMap.id

Tactic:
have ⟨n, f, surj⟩ := exists_fin' R M
  have ⟨g, hfg⟩ := Module.projective_lifting_property f .id surj
  ⟨n, f, g, surj, LinearMap.injective_of_comp_eq_id _ _ hfg, hfg⟩

Premises used: LinearMap.id, _private.0.Module.Finite.exists_comp_eq_id_of_projective.match_1, Exists, LinearMap.injective_of_comp_eq_id, LinearMap.comp, And, _private.0.Module.Finite.exists_comp_eq_id_of_projective.match_2, And.intro, Exists.intro, Module.projective_lifting_property, Function.Injective, Module.Finite.exists_fin', Eq, DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.Finiteness.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : Module.Finite A B
⊢ Module.Finite.{u_1, u_2} (A ⧸ p) (B ⧸ P)

Tactic:
Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ P)

Premises used: Module.Finite.of_restrictScalars_finite, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Finiteness.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : Module.Finite A B
⊢ Module.Finite.{u_1, u_2} (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A P)) (B ⧸ P)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Finiteness.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : Algebra.FiniteType A B
⊢ Algebra.FiniteType.{u_1, u_2} (A ⧸ p) (B ⧸ P)

Tactic:
Algebra.FiniteType.of_restrictScalars_finiteType A (A ⧸ p) (B ⧸ P)

Premises used: Algebra.FiniteType.of_restrictScalars_finiteType, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Finiteness.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : IsNoetherian A B
⊢ IsNoetherian.{u_1, u_2} (A ⧸ p) (B ⧸ P)

Tactic:
isNoetherian_of_tower A inferInstance

Premises used: inferInstance, isNoetherian_of_tower
-- Module: Mathlib.RingTheory.Finiteness.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : IsNoetherian A B
⊢ IsNoetherian.{u_1, u_2} (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))

Tactic:
isNoetherian_of_tower A <|
    isNoetherian_of_surjective (Ideal.Quotient.mkₐ A _).toLinearMap <|
      LinearMap.range_eq_top.mpr Ideal.Quotient.mk_surjective

Premises used: Iff.mpr, AlgHom.toLinearMap, isNoetherian_of_surjective, LinearMap.range_eq_top, Ideal.Quotient.mk_surjective, isNoetherian_of_tower, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
rw : Small.{u, u_2} ↥(P.subtype.coprod Q.subtype).range
⊢ Small.{u, u_2} ↥(P ⊔ Q)

Tactic:
rw [Submodule.sup_eq_range]

Premises used: Submodule.sup_eq_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P.subtype.coprod Q.subtype).range

Tactic:
small_range _

Premises used: Set.Mem, setOf, small_range, Set.range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P.subtype.coprod Q.subtype).range

Tactic:
exact small_range _

Premises used: small_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // Small.{u, u_2} ↥P }
⊢ (↑P : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // Small.{u, u_2} ↥P }
⊢ (↑P : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // Small.{u, u_2} ↥P }
⊢ (↑Q : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // Small.{u, u_2} ↥P }
⊢ (↑Q : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : { P : Submodule R M // Small.{u, u_2} ↥P }
hPR : x ≤ x_2
hQR : x_1 ≤ x_2
⊢ (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M)

Tactic:
rw [← Subtype.coe_le_coe] at hPR hQR ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : { P : Submodule R M // Small.{u, u_2} ↥P }
hPR : x ≤ x_2
hQR : x_1 ≤ x_2
hPR₁ : (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M)
⊢ (↑x_1 : Submodule R M) ≤ (↑x_2 : Submodule R M)

Tactic:
rw [← Subtype.coe_le_coe] at hPR hQR ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : { P : Submodule R M // Small.{u, u_2} ↥P }
hPR : (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M)
hQR : (↑x_1 : Submodule R M) ≤ (↑x_2 : Submodule R M)
⊢ (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⋯) :
      Submodule R M) ≤
    (↑x_2 : Submodule R M)

Tactic:
sup_le hPR hQR

Premises used: Set.Mem, sup_le
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : { P : Submodule R M // Small.{u, u_2} ↥P }
hPR : (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M)
hQR : (↑x_1 : Submodule R M) ≤ (↑x_2 : Submodule R M)
⊢ (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⋯) :
      Submodule R M) ≤
    (↑x_2 : Submodule R M)

Tactic:
exact sup_le hPR hQR

Premises used: sup_le
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
P : ι → Submodule R M
inst_3 : Small.{u, u_3} ι
inst_4 : ∀ (i : ι), Small.{u, u_2} ↥(P i)
rw :
  Small.{u, u_2}
    ↥(LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(P i)) (τ₁₂ := RingHom.id R)
        ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(P i)) : (a : (i : ι) → ↥(P i) →ₗ[R] M) → (Π₀ (i : ι), ↥(P i)) →ₗ[R] M)
          fun (i : ι) ↦ (P i).subtype))
⊢ Small.{u, u_2} ↥(iSup P)

Tactic:
rw [iSup_eq_range_dfinsupp_lsum]

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
P : ι → Submodule R M
inst_3 : Small.{u, u_3} ι
inst_4 : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2}
    ↥(LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(P i)) (τ₁₂ := RingHom.id R)
        ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(P i)) : (a : (i : ι) → ↥(P i) →ₗ[R] M) → (Π₀ (i : ι), ↥(P i)) →ₗ[R] M)
          fun (i : ι) ↦ (P i).subtype))

Tactic:
apply small_range

Premises used: small_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
P : ι → Submodule R M
inst_3 : Small.{u, u_3} ι
inst_4 : ∀ (i : ι), Small.{u, u_2} ↥(P i)
rw rw₁ rw₂ :
  Small.{u, u_2}
    ↥(LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(P i)) (τ₁₂ := RingHom.id R)
        ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(P i)) : (a : (i : ι) → ↥(P i) →ₗ[R] M) → (Π₀ (i : ι), ↥(P i)) →ₗ[R] M)
          fun (i : ι) ↦ (P i).subtype))
⊢ Small.{u, u_2} ↥(iSup P)

Tactic:
classical
  rw [iSup_eq_range_dfinsupp_lsum]
  apply small_range

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, small_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
P : Submodule R M
hP : P.FG
⊢ ∃ (n : ℕ) (s : Fin n → M), span R (Set.range s) = P

Tactic:
rw [fg_iff_exists_fin_generating_family] at hP

Premises used: Submodule.fg_iff_exists_fin_generating_family
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
P : Submodule R M
hP : ∃ (n : ℕ) (s : Fin n → M), span R (Set.range s) = P
obtain : ∀ (n : ℕ) (s : Fin n → M), Small.{u, u_2} ↥(span R (Set.range s))
⊢ Small.{u, u_2} ↥P

Tactic:
obtain ⟨n, s, rfl⟩ := hP

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
n : ℕ
s : Fin n → M
rw : Small.{u, u_2} ↥(LinearMap.range (Fintype.linearCombination R s))
⊢ Small.{u, u_2} ↥(span R (Set.range s))

Tactic:
rw [← Fintype.range_linearCombination]

Premises used: Fintype.range_linearCombination
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(LinearMap.range (Fintype.linearCombination R s))

Tactic:
apply small_range

Premises used: small_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
inst_4 : Module.Finite R M
⊢ Small.{u, u_2} ↥⊤

Tactic:
have : Small.{u} (⊤ : Submodule R M) :=
    FG.small _ (Module.finite_def.mp inferInstance)
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
inst_4 : Module.Finite R M
this : Small.{u, u_2} ↥⊤
rwa rwa₁ rwa₂ rwa₃ : Small.{u, u_2} (↑Set.univ : Type u_2)
⊢ Small.{u, u_2} M

Tactic:
rwa [← small_univ_iff]

Premises used: small_univ_iff
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
m : M
⊢ Small.{u, u_2} ↥(R ∙ m)

Tactic:
FG.small _ (fg_span_singleton _)

Premises used: Submodule.fg_span_singleton, Submodule.FG.small
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
s : Set M
inst_4 : Small.{u, u_2} (↑s : Type u_2)
this : Eq (α := Submodule R M) (span R s) (⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
rw : Small.{u, u_2} ↥(⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
s : Set M
inst_4 : Small.{u, u_2} (↑s : Type u_2)
this : Eq (α := Submodule R M) (span R s) (⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
⊢ Small.{u, u_2} ↥(⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))

Tactic:
apply small_iSup

Premises used: Submodule.small_iSup
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
s : Set M
inst_4 : Small.{u, u_2} (↑s : Type u_2)
suffices : Eq (α := Submodule R M) (span R s) (⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
suffices span R s = iSup (fun i : s ↦ span R ({(↑i : M)} : Set M)) by
    rw [this]
    apply small_iSup
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{u, u_1} R
s : Set M
inst_4 : Small.{u, u_2} (↑s : Type u_2)
⊢ Eq (α := Submodule R M) (span R s) (⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))

Tactic:
simp [← Submodule.span_iUnion]

Premises used: Submodule.span_iUnion
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
s : Set S
inst_4 : Small.{u, u_2} (↑s : Type u_2)
rw :
  Small.{u, u_2}
    ↥(AlgHom.range (A := MvPolynomial.{u_2, u_1} { x : S // x ∈ s } R) (aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))))
⊢ Small.{u, u_2} ↥(adjoin R s)

Tactic:
rw [Algebra.adjoin_eq_range]

Premises used: Algebra.adjoin_eq_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
s : Set S
inst_4 : Small.{u, u_2} (↑s : Type u_2)
⊢ Small.{u, u_2}
    ↥(AlgHom.range (A := MvPolynomial.{u_2, u_1} { x : S // x ∈ s } R) (aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))))

Tactic:
apply small_range

Premises used: small_range
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
A : Subalgebra R S
fgS : A.FG
obtain : ∀ (s : Finset S), Small.{u, u_2} ↥(adjoin R (↑s : Set S))
⊢ Small.{u, u_2} ↥A

Tactic:
obtain ⟨s, hs, rfl⟩ := fgS

Premises used: rfl