awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG
have empty : ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
  (sInf (↑∅ : Set (Submodule R M))).CoFG
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
empty :
  ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
    (sInf (↑∅ : Set (Submodule R M))).CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG
have insert : ∀ (w : Submodule R M) (s : Finset (Submodule R M)) (hws : w ∉ s)
  (hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG) (hs : ∀ S ∈ insert w s, S.CoFG),
  (sInf (↑(insert w s) : Set (Submodule R M))).CoFG
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Set (Submodule R M)
hs : s.Finite
hcofg : ∀ S ∈ s, S.CoFG
⊢ (sInf s).CoFG
have rw : ∀ (hcofg : ∀ S ∈ (↑(hs.toFinset (s := s)) : Set (Submodule R M)), S.CoFG),
  (sInf (↑(hs.toFinset (s := s)) : Set (Submodule R M))).CoFG
Tactic: rw [← hs.coe_toFinset] at hcofg ⊢
Cleared hypotheses: hcofg
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ (S : Set M), S.Finite ∧ span R S = N
have refine : (∃ (S : Set M), S.Finite ∧ span R S = N) → N.FG
Tactic: refine ⟨fun ⟨t, h⟩ => ⟨_, t.finite_toSet, h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t' : Set M
h : t'.Finite
⊢ FG (span R t')
have this : ∃ (s' : Finset M), (↑s' : Set M) = t'
Tactic: have := h.exists_finset_coe
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t' : Set M
h : t'.Finite
this : ∃ (s' : Finset M), (↑s' : Set M) = t'
⊢ FG (span R t')
have tauto : ∀ (w : Finset M), (↑w : Set M) = t' → FG (span R t')
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
have rw : (∃ (S : Set M), S.Finite ∧ span R S = N) ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
Tactic: rw [fg_def]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ (∃ (S : Set M), S.Finite ∧ span R S = N) ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
have mp : (∃ (S : Set M), S.Finite ∧ span R S = N) → ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
mp : (∃ (S : Set M), S.Finite ∧ span R S = N) → ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
⊢ (∃ (S : Set M), S.Finite ∧ span R S = N) ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
have mpr : (∃ (n : ℕ) (s : Fin n → M), span R (range s) = N) → ∃ (S : Set M), S.Finite ∧ span R S = N
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
Sfin : S.Finite
hS : span R S = N
⊢ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
have mp : ∀ (n : ℕ) (f : Fin n ↪ M) (Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M)))
  (hS : span R (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N), ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
Tactic: obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
Cleared hypotheses: S, Sfin, hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
⊢ N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
have mp : N.FG → ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
mp : N.FG → ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
⊢ N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
have mpr : (∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N) → N.FG
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
⊢ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
have mp : ∀ (n : ℕ) (f : Fin n → M) (h : span A (range f) = N), ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
Tactic: obtain ⟨n, f, h⟩ := fg_iff_exists_fin_generating_family.mp hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
have mp : span A (range (f ∘ ULift.down)) = N
Tactic: refine ⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ span A (range (f ∘ ULift.down)) = N
have h₁ : range (f ∘ ULift.down) = range f
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ range (f ∘ ULift.down) = range f
have h₁ : ∀ (x : M), x ∈ range (f ∘ ULift.down) ↔ x ∈ range f
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
G : Type w
w : Finite G
g : G → M
hg : span A (range g) = N
⊢ N.FG
have mpr : ∀ (this : Fintype (↑(range g) : Type v)), N.FG
Tactic: have := Fintype.ofFinite (range g)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ FG (span R s) ↔ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp : FG (span R s) → ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
mp : FG (span R s) → ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ FG (span R s) ↔ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mpr : (∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))) → FG (span R s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp : ∀ (s' : Finset M) (hs's : (↑s' : Set M) ⊆ s) (hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)),
  ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
Tactic: obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp : Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
Tactic: refine ⟨s', hs's, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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)
⊢ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp : LE.le (α := Submodule R M) (span R s) (span R (↑s' : Set M))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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)
mp : LE.le (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp₁ : LE.le (α := Submodule R M) (span R (↑s' : Set M)) (span R s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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)
⊢ LE.le (α := Submodule R M) (span R s) (span R (↑s' : Set M))
have mp : LE.le (α := Submodule R M) (span R (↑s'' : Set M)) (span R (↑s' : Set M))
Tactic: rwa [← hs'', span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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)
⊢ LE.le (α := Submodule R M) (span R (↑s' : Set M)) (span R s)
have mp : (↑s' : Set M) ⊆ (↑(span R s) : Set M)
Tactic: rw [span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ Finite (algebraMap A B) ↔ Module.Finite A B
have rw : Module.Finite A B ↔ Module.Finite A B
Tactic: rw [Finite, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Defs (goal)
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
⊢ Finite (algebraMap A B) ↔ Module.Finite A B
have rw₁ : Module.Finite A B ↔ Module.Finite A B
Tactic: rw [Finite, toAlgebra_algebraMap]
-- 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)
⊢ 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)) ⊤),
  Module.Finite R M
Tactic: obtain ⟨n, s, hs⟩ := Module.Finite.exists_fin (R := T) (M := T ⊗[R] M)
-- 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)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤
⊢ Module.Finite R M
have 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
Tactic: choose k t m h using fun i : Fin n ↦ TensorProduct.exists_sum_tmul_eq (s i)
-- 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)
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
⊢ Module.Finite R M
have 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)
Tactic: apply of_surjective f₀
-- 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)
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)
have 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))
Tactic: rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
-- 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)
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
⊢ 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))
have 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
Tactic: use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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.{u_1 + 1, u_4 + 1} (α := (i : Fin n) × Fin (k i) → R) (β := M)
    (⇑f₀ : (a : (i : Fin n) × Fin (k i) → R) → M)
have 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)
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]
-- 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)
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)
⊢ 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)
have 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)
Tactic: 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)
⊢ 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)) ⊤),
  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]