awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)))
⊢ 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₂)
        ψ)
      ⊤)
have h : φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)
Tactic: suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)))
⊢ φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)
have 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))
Tactic: apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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 : ℕ
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
have zero : Module.Finite.{u_1, u_2} R (S ⧸ HPow.hPow (β := ℕ) I 0)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
have succ : ∀ (n : ℕ) (IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)), Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Prod (goal)
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
⊢ 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
have rw : Submodule.prod (span R tb) (span R tc) = sb.prod sc
Tactic: rw [LinearMap.span_inl_union_inr, htb.2, htc.2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Prod (goal)
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
⊢ 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
have rw₁ : sb.prod (span R tc) = sb.prod sc
Tactic: rw [LinearMap.span_inl_union_inr, htb.2, htc.2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Prod (goal)
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
⊢ 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
have rw₂ : sb.prod sc = sb.prod sc
Tactic: rw [LinearMap.span_inl_union_inr, htb.2, htc.2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Prod (goal)
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) ⊤
have rw : Submodule.FG (R := R) (M := M × N) (Submodule.prod ⊤ ⊤)
Tactic: rw [← Submodule.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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 ⊔ Q)
have rw : Small.{u, u_2} ↥(P.subtype.coprod Q.subtype).range
Tactic: rw [Submodule.sup_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (hypothesis)
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
⊢ Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⋯ ≤ x_2
have hPR₁ : (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M)
Tactic: rw [← Subtype.coe_le_coe] at hPR hQR ⊢
Cleared hypotheses: hPR, hQR
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (hypothesis)
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)
⊢ Subtype.mk (p := fun (P : Submodule R M) ↦ Small.{u, u_2} ↥P) ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⋯ ≤ x_2
have hQR₁ : (↑x_1 : Submodule R M) ≤ (↑x_2 : Submodule R M)
Tactic: rw [← Subtype.coe_le_coe] at hPR hQR ⊢
Cleared hypotheses: hPR, hQR
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥(iSup P)
have 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))
Tactic: rw [iSup_eq_range_dfinsupp_lsum]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥(iSup P)
have 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))
Tactic: classical
  rw [iSup_eq_range_dfinsupp_lsum]
  apply small_range
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (hypothesis)
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
⊢ Small.{u, u_2} ↥P
have hP₁ : ∃ (n : ℕ) (s : Fin n → M), span R (Set.range s) = P
Tactic: rw [fg_iff_exists_fin_generating_family] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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
⊢ Small.{u, u_2} ↥P
have obtain : ∀ (n : ℕ) (s : Fin n → M), Small.{u, u_2} ↥(span R (Set.range s))
Tactic: obtain ⟨n, s, rfl⟩ := hP
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥(span R (Set.range s))
have rw : Small.{u, u_2} ↥(LinearMap.range (Fintype.linearCombination R s))
Tactic: rw [← Fintype.range_linearCombination]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (hypothesis)
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} M
have this : Small.{u, u_2} ↥⊤
Tactic: have : Small.{u} (⊤ : Submodule R M) :=
    FG.small _ (Module.finite_def.mp inferInstance)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥⊤
⊢ Small.{u, u_2} M
have rwa : Small.{u, u_2} (↑Set.univ : Type u_2)
Tactic: rwa [← small_univ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥(span R s)
have rw : Small.{u, u_2} ↥(⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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)
⊢ Small.{u, u_2} ↥(span R s)
have suffices : Eq (α := Submodule R M) (span R s) (⨆ (i : (↑s : Type u_2)), R ∙ (↑i : M))
Tactic: suffices span R s = iSup (fun i : s ↦ span R ({(↑i : M)} : Set M)) by
    rw [this]
    apply small_iSup
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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} ↥(adjoin R s)
have 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))))
Tactic: rw [Algebra.adjoin_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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
⊢ Small.{u, u_2} ↥A
have obtain : ∀ (s : Finset S), Small.{u, u_2} ↥(adjoin R (↑s : Set S))
Tactic: obtain ⟨s, hs, rfl⟩ := fgS
Cleared hypotheses: A, fgS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (hypothesis)
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
inst_4 : FiniteType R S
⊢ Small.{u, u_2} S
have this : Small.{u, u_2} ↥⊤
Tactic: have : Small.{u} (⊤ : Subalgebra R S) :=
    Subalgebra.FG.small Algebra.FiniteType.out
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Small (goal)
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
inst_4 : FiniteType R S
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} S
have rwa : Small.{u, u_2} (↑Set.univ : Type u_2)
Tactic: rwa [← small_univ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
⊢ (↑I : Submodule R A).FG
have obtain : ∀ (T T' : Finset A) (hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A))
  (hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A))
  (one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1), (↑I : Submodule R A).FG
Tactic: obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
⊢ (↑I : Submodule R A).FG
have refine : (↑I : Submodule R A) ≤ span R (↑T : Set A)
Tactic: refine ⟨T, span_eq_of_le _ hT ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
⊢ (↑I : Submodule R A) ≤ span R (↑T : Set A)
have rw : (↑(1 * I) : Submodule R A) ≤ HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1
Tactic: rw [← one_mul I, ← mul_one (span R (T : Set A))]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
| HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1
have rw : span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
Tactic: rw [← I.inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
⊢ (↑(1 * I) : Submodule R A) ≤ HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1
have conv_rhs : (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
Tactic: conv_rhs => rw [← I.inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
have grw : (↑(1 * I) : Submodule R A) ≤
  HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
Tactic: grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
grw :
  (↑(1 * I) : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
have grw₁ : (↑1 : Submodule R A) * (↑I : Submodule R A) ≤
  HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
Tactic: grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
grw :
  (↑(1 * I) : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₁ :
  (↑1 : Submodule R A) * (↑I : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
have grw₂ : 1 * (↑I : Submodule R A) ≤
  HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
Tactic: grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]