awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
inst : CommRing R
T : Type u_3
inst_1 : CommRing T
inst_2 : Algebra R T
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : FaithfullyFlat R T
inst_6 : Module.Finite T (T ⊗[R] M)
obtain :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤),
    Module.Finite R M
⊢ Module.Finite R M
have obtain₁ : ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
  (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
  (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j), Module.Finite R M
Tactic: classical
  obtain ⟨n, s, hs⟩ := Module.Finite.exists_fin (R := T) (M := T ⊗[R] M)
  choose k t m h using fun i : Fin n ↦ TensorProduct.exists_sum_tmul_eq (s i)
  let f₀ : ((Σ i, Fin (k i)) → R) →ₗ[R] M := (Pi.basisFun R _).constr R fun ⟨i, j⟩ ↦ m i j
  apply of_surjective f₀
  have : Function.Surjective (AlgebraTensorModule.lTensor T T f₀) := by
    rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
    intro i
    use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩
    simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]
  rwa [← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
inst : CommRing R
T : Type u_3
inst_1 : CommRing T
inst_2 : Algebra R T
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : FaithfullyFlat R T
inst_6 : Module.Finite T (T ⊗[R] M)
obtain :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤),
    Module.Finite R M
obtain₁ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j), Module.Finite R M
obtain₂ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j), Module.Finite R M
⊢ Module.Finite R M
have obtain₃ : ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
  (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
  (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j),
  let f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
    (Basis.constr (Pi.basisFun R ((i : Fin n) × Fin (k i))) R :
        (a : (i : Fin n) × Fin (k i) → M) → ((i : Fin n) × Fin (k i) → R) →ₗ[R] M)
      fun (x : (i : Fin n) × Fin (k i)) ↦
      match (motive := (i : Fin n) × Fin (k i) → M) x with
      | ⟨i, j⟩ => m i j;
  Function.Surjective.{u_1 + 1, u_4 + 1} (α := (i : Fin n) × Fin (k i) → R) (β := M)
    (⇑f₀ : (a : (i : Fin n) × Fin (k i) → R) → M)
Tactic: classical
  obtain ⟨n, s, hs⟩ := Module.Finite.exists_fin (R := T) (M := T ⊗[R] M)
  choose k t m h using fun i : Fin n ↦ TensorProduct.exists_sum_tmul_eq (s i)
  let f₀ : ((Σ i, Fin (k i)) → R) →ₗ[R] M := (Pi.basisFun R _).constr R fun ⟨i, j⟩ ↦ m i j
  apply of_surjective f₀
  have : Function.Surjective (AlgebraTensorModule.lTensor T T f₀) := by
    rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
    intro i
    use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩
    simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]
  rwa [← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ Submodule.FG I
have rw : Module.Finite R ↥I
Tactic: rw [← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
⊢ Module.Finite R ↥I
have hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
Tactic: have hf : Function.Injective f := by simp [f]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
have refine_1 : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ f.range
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
refine_1 : Ideal.map (F := R →+* S) (algebraMap R S) I ≤ f.range
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
have refine_2 : f.range ≤ Ideal.map (F := R →+* S) (algebraMap R S) I
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I ≤ f.range
have refine_1 : I ≤ comap (F := R →+* S) (algebraMap R S) f.range
Tactic: rw [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
x : R
hx : x ∈ I
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) f.range) x
have h : Eq.{u_2 + 1} (α := S) ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] Subtype.mk (p := fun (x : R) ↦ x ∈ I) x hx) : S)
  ((algebraMap R S : (a : R) → S) x : S)
Tactic: use 1 ⊗ₜ ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) : S)
have this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
Tactic: have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) : S)
have refine_2 : Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
  (HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S))
have refine_2 : Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
  ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
Tactic: apply Ideal.mul_mem_left
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
x : S ⊗[R] ↥I
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) x : S)
have refine_2 : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
  ((f : (a : S ⊗[R] ↥I) → S) 0 : S)
Tactic: induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
x : S ⊗[R] ↥I
refine_2 :
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) 0 : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) x : S)
have refine_2₁ : ∀ (x y : S ⊗[R] ↥I),
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
      ((f : (a : S ⊗[R] ↥I) → S) x : S) →
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((f : (a : S ⊗[R] ↥I) → S) y : S) →
      Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((f : (a : S ⊗[R] ↥I) → S) (x + y) : S)
Tactic: induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
x : S ⊗[R] ↥I
refine_2 :
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) 0 : S)
refine_2₁ :
  ∀ (x y : S ⊗[R] ↥I),
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((f : (a : S ⊗[R] ↥I) → S) x : S) →
      Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
          ((f : (a : S ⊗[R] ↥I) → S) y : S) →
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
          ((f : (a : S ⊗[R] ↥I) → S) (x + y) : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) x : S)
have refine_2₂ : ∀ (s : S) (x : ↥I),
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) : S)
Tactic: induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
⊢ Module.Finite R ↥I
have this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
Tactic: have : I.map (algebraMap R S) = LinearMap.range f := by
    refine le_antisymm ?_ ?_
    · rw [Ideal.map_le_iff_le_comap]
      intro x hx
      use 1 ⊗ₜ ⟨x, hx⟩
      simp [f, Algebra.smul_def]
    · rintro - ⟨x, rfl⟩
      induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
⊢ Module.Finite S (S ⊗[R] ↥I)
have rwa : Module.Finite S ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
rwa : Module.Finite S ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ Module.Finite S (S ⊗[R] ↥I)
have rwa₁ : Submodule.FG.{u_2, u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
⊢ Module.Finite R ↥I
have this₁ : Module.Finite S (S ⊗[R] ↥I)
Tactic: have : Module.Finite S (S ⊗[R] ↥I) := by
    rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FiniteType T (T ⊗[R] S)
⊢ FiniteType R S
have obtain : ∀ (s : Finset (T ⊗[R] S)) (hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤), FiniteType R S
Tactic: obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := T) (A := T ⊗[R] S)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
⊢ FiniteType R S
have this : ∀ (x : ↥s), ∃ (k : ℕ) (m : Fin k → T) (n : Fin k → S), (↑x : T ⊗[R] S) = ∑ j : Fin k, m j ⊗ₜ[R] n j
Tactic: have (x : s) := TensorProduct.exists_sum_tmul_eq x.1
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
this : ∀ (x : ↥s), ∃ (k : ℕ) (m : Fin k → T) (n : Fin k → S), (↑x : T ⊗[R] S) = ∑ j : Fin k, m j ⊗ₜ[R] n j
⊢ FiniteType R S
have choose : ∀ (k : (x : ↥s) → ℕ) (t : (x : ↥s) → Fin (k x) → T) (m : (x : ↥s) → Fin (k x) → S)
  (h : ∀ (x : ↥s), (↑x : T ⊗[R] S) = ∑ j : Fin (k x), t x j ⊗ₜ[R] m x j), FiniteType R S
Tactic: choose k t m h using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
k : (x : ↥s) → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), (↑x : T ⊗[R] S) = ∑ j : Fin (k x), t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun (x : (x : ↥s) × Fin (k x)) ↦
    match (motive := (x : ↥s) × Fin (k x) → S) x with
    | ⟨x, i⟩ => m x i
⊢ FiniteType R S
have apply : Function.Surjective (α := MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := S)
  (⇑f : (a : MvPolynomial ((x : ↥s) × Fin (k x)) R) → S)
Tactic: apply Algebra.FiniteType.of_surjective f