awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
letI letI₁ letI₂ : FiniteType R S
letI₃ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    FiniteType R S
out :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
out₁ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (H : ∀ (r : ↥s), Subalgebra.FG (R := Localization.Away (↑r : R)) (A := Localization.Away (↑r : R) ⊗[R] S) ⊤),
    Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
⊢ FiniteType R S
have out₂ : let f : R →+* S := algebraMap R S;
∀
  (this :
    (r : ↥s) →
      Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
  (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
  (s₂ :
    ∀ (r : ↥s),
      Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
        (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
  Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
Tactic: classical
  letI := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra
  set f := algebraMap R S
  constructor
  replace H := fun r => (h r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
  rw [eq_top_iff]
  rintro x -
  apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
    _ hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
      (algebraMap S _ x) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
⊢ s.FG
have haveI : ∀ (this : DecidableEq R), s.FG
Tactic: haveI := Classical.decEq R
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this : DecidableEq R
⊢ s.FG
have haveI : ∀ (this : DecidableEq M), s.FG
Tactic: haveI := Classical.decEq M
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this_1 : DecidableEq R
this : DecidableEq M
⊢ s.FG
have haveI : ∀ (this : DecidableEq P), s.FG
Tactic: haveI := Classical.decEq P
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
⊢ s.FG
have obtain : ∀ (t1 : Finset P) (ht1 : span R (↑t1 : Set P) = map f s), s.FG
Tactic: obtain ⟨t1, ht1⟩ := hs1
Cleared hypotheses: hs1
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs2 : (s ⊓ f.ker).FG
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
⊢ s.FG
have obtain : ∀ (t2 : Finset M) (ht2 : span R (↑t2 : Set M) = s ⊓ f.ker), s.FG
Tactic: obtain ⟨t2, ht2⟩ := hs2
Cleared hypotheses: hs2
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
y : P
hy : y ∈ t1
⊢ y ∈ map f s
have rw : Membership.mem (γ := Submodule R P) (span R (↑t1 : Set P)) y
Tactic: rw [← ht1]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
y : P
hy : y ∈ t1
⊢ ∃ x ∈ s, (f : (a : M) → P) x = y
have this₁ : y ∈ map f s
Tactic: have : y ∈ s.map f := by
      rw [← ht1]
      exact subset_span hy
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
y : P
hy : y ∈ t1
this : y ∈ map f s
⊢ ∃ x ∈ s, (f : (a : M) → P) x = y
have rcases : ∀ (x : M) (hx1 : x ∈ s) (hx2 : (f : (a : M) → P) x = y), ∃ x ∈ s, (f : (a : M) → P) x = y
Tactic: rcases mem_map.1 this with ⟨x, hx1, hx2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
⊢ s.FG
have this₁ : ∀ y ∈ t1, ∃ x ∈ s, (f : (a : M) → P) x = y
Tactic: have : ∀ y ∈ t1, ∃ x ∈ s, f x = y := by
    intro y hy
    have : y ∈ s.map f := by
      rw [← ht1]
      exact subset_span hy
    rcases mem_map.1 this with ⟨x, hx1, hx2⟩
    exact ⟨x, hx1, hx2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
this : ∀ y ∈ t1, ∃ x ∈ s, (f : (a : M) → P) x = y
⊢ ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
have choose : ∀ (g : (y : P) → y ∈ t1 → M) (hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s)
  (hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y),
  ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
Tactic: choose g hg1 hg2 using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y
⊢ ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
have exists : ∀ y ∈ t1,
  (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s ∧
    (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
Tactic: exists fun y => if H : y ∈ t1 then g y H else 0
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y
y : P
H : y ∈ t1
⊢ (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s ∧
    (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
have left : (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y
y : P
H : y ∈ t1
left : (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s
⊢ (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s ∧
    (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
have right : (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y
y : P
H : y ∈ t1
⊢ (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s
have left : g y H ∈ s
Tactic: simp only [dif_pos H]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), (f : (a : M) → P) (g y a) = y
y : P
H : y ∈ t1
⊢ (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
have right : (f : (a : M) → P) (g y H) = y
Tactic: simp only [dif_pos H]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
this : ∀ y ∈ t1, ∃ x ∈ s, (f : (a : M) → P) x = y
⊢ s.FG
have this₁ : ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
Tactic: have : ∃ g : P → M, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y := by
    choose g hg1 hg2 using this
    exists fun y => if H : y ∈ t1 then g y H else 0
    intro y H
    constructor
    · simp only [dif_pos H]
      apply hg1
    · simp only [dif_pos H]
      apply hg2
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
this_4 : ∀ y ∈ t1, ∃ x ∈ s, (f : (a : M) → P) x = y
this : ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
⊢ s.FG
have obtain : ∀ (g : P → M) (hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y), s.FG
Tactic: obtain ⟨g, hg⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
⊢ s.FG
have exists : span R (↑(Finset.image g t1 ∪ t2) : Set M) = s
Tactic: exists t1.image g ∪ t2
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
⊢ span R (↑(Finset.image g t1 ∪ t2) : Set M) = s
have rw : span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) = s
Tactic: rw [Finset.coe_union, span_union, Finset.coe_image]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) = s
have a : span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) ≤ s
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
a : span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) ≤ s
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) = s
have a₁ : s ≤ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) ≤ s
have a : (↑t1 : Set P) ⊆ g ⁻¹' (↑s : Set M)
Tactic: refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
a : (↑t1 : Set P) ⊆ g ⁻¹' (↑s : Set M)
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) ≤ s
have a₁ : (↑t2 : Set M) ⊆ (↑s : Set M)
Tactic: refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ (↑t2 : Set M)
⊢ x ∈ (↑s : Set M)
have this₁ : Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M)) x
Tactic: have : x ∈ span R t2 := subset_span hx
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ (↑t2 : Set M)
this : Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M)) x
⊢ x ∈ (↑s : Set M)
have this₁ : x ∈ s ⊓ f.ker
Tactic: rw [ht2] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
have this₁ : Membership.mem (α := P) (map f s) ((f : (a : M) → P) x : P)
Tactic: have : f x ∈ s.map f := by
    rw [mem_map]
    exact ⟨x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
this : Membership.mem (α := P) (map f s) ((f : (a : M) → P) x : P)
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
have this₁ : ∃ (l : P →₀ R),
  Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l ∧
    Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
Tactic: rw [← ht1, ← Set.image_id (t1 : Set P), Finsupp.mem_span_image_iff_linearCombination] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
this :
  ∃ (l : P →₀ R),
    Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l ∧
      Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
have a : ∀ (l : P →₀ R) (hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l)
  (hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)),
  Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
Tactic: rcases this with ⟨l, hl1, hl2⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
have a : Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)))
  (AddHom.toFun (M := M →₀ R) (LinearMap.toAddHom (linearCombination R id))
    ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l))
Tactic: refine
    mem_sup.2
      ⟨(linearCombination R id).toFun ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        x - linearCombination R id ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        add_sub_cancel _ _⟩