awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
⊢ (↑s' : Set M) ⊆ (↑(span R s) : Set M)

Tactic:
le_trans hs's subset_span

Premises used: Submodule.subset_span, le_trans
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
⊢ (↑s' : Set M) ⊆ (↑(span R s) : Set M)

Tactic:
exact le_trans hs's subset_span

Premises used: Submodule.subset_span, le_trans
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s' : Finset M
left : (↑s' : Set M) ⊆ s
h : Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ FG (span R s)

Tactic:
⟨s', h.symm⟩

Premises used: Submodule.FG, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s' : Finset M
left : (↑s' : Set M) ⊆ s
h : Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ FG (span R s)

Tactic:
exact ⟨s', h.symm⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_6
M : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Module.Finite R M ↔ Submodule.FG.{u_6, u_7} (R := R) (M := M) ⊤

Tactic:
⟨(·.fg_top), .of_fg_top⟩

Premises used: Module.Finite.fg_top, Module.Finite.of_fg_top, Iff.intro
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
M : Type u_6
inst : AddCommMonoid M
⊢ Module.Finite ℕ M ↔ AddMonoid.FG M

Tactic:
⟨fun h => AddMonoid.fg_def.mpr <| (fg_iff_addSubmonoid_fg ⊤).mp h.fg_top,
    fun h => of_fg_top <| (fg_iff_addSubmonoid_fg ⊤).mpr (AddMonoid.fg_def.mp h)⟩

Premises used: Iff.mpr, Module.Finite.fg_top, Module.Finite.of_fg_top, AddMonoid.fg_def, Submodule.fg_iff_addSubmonoid_fg, Iff.intro, Iff.mp, Top.top
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
G : Type u_6
inst : AddCommGroup G
⊢ Module.Finite ℤ G ↔ AddGroup.FG G

Tactic:
⟨fun h => AddGroup.fg_def.mpr <| (fg_iff_addSubgroup_fg ⊤).mp h.fg_top,
    fun h => of_fg_top <| (fg_iff_addSubgroup_fg ⊤).mpr (AddGroup.fg_def.mp h)⟩

Premises used: Iff.mpr, Module.Finite.fg_top, AddGroup.fg_def, Submodule.fg_iff_addSubgroup_fg, Module.Finite.of_fg_top, Iff.intro, Iff.mp, Top.top
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
⊢ ∃ (n : ℕ) (s : Fin n → M), Eq (α := Submodule R M) (span R (range s)) ⊤

Tactic:
fg_iff_exists_fin_generating_family.mp fg_top

Premises used: Module.Finite.fg_top, Submodule.fg_iff_exists_fin_generating_family, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M_1 : Type u_4
N : Type u_5
M : Type u_6
inst : AddCommMonoid M
inst_1 : FG M
⊢ Module.Finite ℕ M

Tactic:
Module.Finite.iff_addMonoid_fg.mpr ‹_›

Premises used: Iff.mpr, Module.Finite.iff_addMonoid_fg
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
inst : AddCommGroup G
inst_1 : FG G
⊢ Module.Finite ℤ G

Tactic:
Module.Finite.iff_addGroup_fg.mpr <| AddGroup.fg_iff_addMonoid_fg.mpr ‹_›

Premises used: Iff.mpr, AddGroup.fg_iff_addMonoid_fg, Module.Finite.iff_addGroup_fg
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : Module.Finite A B ↔ Module.Finite A B
rw₁ rw₂ : Module.Finite A B ↔ Module.Finite A B
⊢ Finite (algebraMap A B) ↔ Module.Finite A B

Tactic:
rw [Finite, toAlgebra_algebraMap]

Premises used: RingHom.Finite, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.Finiteness.Descent
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

Tactic:
obtain ⟨n, s, hs⟩ := Module.Finite.exists_fin (R := T) (M := T ⊗[R] M)

Premises used: Module.Finite.exists_fin
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤
choose :
  ∀ (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

Tactic:
choose k t m h using fun i : Fin n ↦ TensorProduct.exists_sum_tmul_eq (s i)

Premises used: TensorProduct.exists_sum_tmul_eq
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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
apply :
  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)
⊢ Module.Finite R M

Tactic:
apply of_surjective f₀

Premises used: Module.Finite.of_surjective
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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
rw :
  ∀ (y : Fin n),
    s y ∈
      (↑(LinearMap.range (R := T) (M := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (τ₁₂ := RingHom.id T)
            (((AlgebraTensorModule.lTensor T T :
                  (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
                (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
              f₀)) :
        Set (T ⊗[R] M))
⊢ Function.Surjective (α := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (β := T ⊗[R] M)
    (⇑(((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀ :
          T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
      (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)

Tactic:
rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]

Premises used: eq_top_iff, LinearMap.range_eq_top, Set.range_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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
i : Fin n
h₁ :
  ((((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀ :
          T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
        (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)
      (∑ j : Fin (k i),
        t i j ⊗ₜ[R]
          (Pi.basisFun R ((i : Fin n) × Fin (k i)) : (a : (i : Fin n) × Fin (k i)) → (i : Fin n) × Fin (k i) → R)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin (k i)) i j)) =
    s i
⊢ s i ∈
    (↑(LinearMap.range (R := T) (M := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (τ₁₂ := RingHom.id T)
          (((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀)) :
      Set (T ⊗[R] M))

Tactic:
use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩

Premises used: Pi.basisFun, Fin, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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
i : Fin n
⊢ ((((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀ :
          T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
        (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)
      (∑ j : Fin (k i),
        t i j ⊗ₜ[R]
          (Pi.basisFun R ((i : Fin n) × Fin (k i)) : (a : (i : Fin n) × Fin (k i)) → (i : Fin n) × Fin (k i) → R)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin (k i)) i j)) =
    s i

Tactic:
simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]

Premises used: Pi.basisFun_apply, Pi.basisFun_equivFun
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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 (α := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (β := T ⊗[R] M)
    (⇑(((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀ :
          T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
      (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)

Tactic:
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]
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
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
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
this :
  Function.Surjective (α := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (β := T ⊗[R] M)
    (⇑(((AlgebraTensorModule.lTensor T T :
                (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R] T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
              (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
            f₀ :
          T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
      (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)
rwa rwa₁ rwa₂ rwa₃ :
  Function.Surjective (α := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (β := T ⊗[R] M)
    (⇑(LinearMap.lTensor T f₀) : (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)
⊢ 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:
rwa [← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T]

Premises used: Module.FaithfullyFlat.lTensor_surjective_iff_surjective
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
rw : Module.Finite R ↥I
⊢ Submodule.FG I

Tactic:
rw [← Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
⊢ Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
⊢ Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)

Tactic:
have hf : Function.Injective f := by simp [f]
-- Module: Mathlib.RingTheory.Finiteness.Descent
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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Finiteness.Descent
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
refine_2 : f.range ≤ Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I = f.range

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Finiteness.Descent
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 : I ≤ comap (F := R →+* S) (algebraMap R S) f.range
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I ≤ f.range

Tactic:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Finiteness.Descent
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
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)
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) f.range) x

Tactic:
use 1 ⊗ₜ ⟨x, hx⟩
-- Module: Mathlib.RingTheory.Finiteness.Descent
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
⊢ 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:
simp [f, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Finiteness.Descent
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)
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Finiteness.Descent
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 y : S ⊗[R] ↥I
h :
  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)
h_1 :
  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:
simp_all [Ideal.add_mem]

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Finiteness.Descent
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
⊢ (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)

Tactic:
simp [f]