awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
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))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
h₂ :
  Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
      Submodule R S)
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
        Submodule R S)
      ((↑r : R) ^ n • x)

Tactic:
use n₂ + n₁
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
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))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
      Submodule R S)
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Algebra.adjoin, le_iSup, SetLike.coe
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
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))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
      Submodule R S)
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂

Premises used: Algebra.adjoin, le_iSup, SetLike.coe
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
haveI : ∀ (this : DecidableEq R), s.FG
⊢ s.FG

Tactic:
haveI := Classical.decEq R
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
haveI : ∀ (this : DecidableEq M), s.FG
⊢ s.FG

Tactic:
haveI := Classical.decEq M
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
haveI : ∀ (this : DecidableEq P), s.FG
⊢ s.FG

Tactic:
haveI := Classical.decEq P
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
obtain : ∀ (t1 : Finset P) (ht1 : span R (↑t1 : Set P) = map f s), s.FG
⊢ s.FG

Tactic:
obtain ⟨t1, ht1⟩ := hs1
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
obtain : ∀ (t2 : Finset M) (ht2 : span R (↑t2 : Set M) = s ⊓ f.ker), s.FG
⊢ s.FG

Tactic:
obtain ⟨t2, ht2⟩ := hs2
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
rw : Membership.mem (γ := Submodule R P) (span R (↑t1 : Set P)) y
⊢ y ∈ map f s

Tactic:
rw [← ht1]
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ Membership.mem (γ := Submodule R P) (span R (↑t1 : Set P)) y

Tactic:
subset_span hy

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ Membership.mem (γ := Submodule R P) (span R (↑t1 : Set P)) y

Tactic:
exact subset_span hy

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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

Tactic:
have : y ∈ s.map f := by
      rw [← ht1]
      exact subset_span hy
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
rcases : ∀ (x : M) (hx1 : x ∈ s) (hx2 : (f : (a : M) → P) x = y), ∃ x ∈ s, (f : (a : M) → P) x = y
⊢ ∃ x ∈ s, (f : (a : M) → P) x = y

Tactic:
rcases mem_map.1 this with ⟨x, hx1, hx2⟩

Premises used: Submodule.mem_map, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 : M
hx1 : x ∈ s
hx2 : (f : (a : M) → P) x = y
⊢ ∃ x ∈ s, (f : (a : M) → P) x = y

Tactic:
⟨x, hx1, hx2⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 : M
hx1 : x ∈ s
hx2 : (f : (a : M) → P) x = y
⊢ ∃ x ∈ s, (f : (a : M) → P) x = y

Tactic:
exact ⟨x, hx1, hx2⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 ∈ 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⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
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
⊢ ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y

Tactic:
choose g hg1 hg2 using this
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
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
⊢ ∃ (g : P → M), ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y

Tactic:
exists fun y => if H : y ∈ t1 then g y H else 0

Premises used: Membership.mem, dite, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
right : (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y
⊢ (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:
constructor
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 : g y H ∈ s
⊢ (fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y ∈ s

Tactic:
simp only [dif_pos H]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ g y H ∈ s

Tactic:
apply hg1
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
right : (f : (a : M) → P) (g y H) = y
⊢ (f : (a : M) → P) ((fun (y : P) ↦ (if H : y ∈ t1 then g y H else 0 : M)) y) = y

Tactic:
simp only [dif_pos H]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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) (g y H) = y

Tactic:
apply hg2
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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

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
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
obtain : ∀ (g : P → M) (hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y), s.FG
⊢ s.FG

Tactic:
obtain ⟨g, hg⟩ := this
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
exists : span R (↑(Finset.image g t1 ∪ t2) : Set M) = s
⊢ s.FG

Tactic:
exists t1.image g ∪ t2

Premises used: Finset.image
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
rw : span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) = s
⊢ span R (↑(Finset.image g t1 ∪ t2) : Set M) = s

Tactic:
rw [Finset.coe_union, span_union, Finset.coe_image]

Premises used: Finset.coe_image, Submodule.span_union, Finset.coe_union
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
a₁ : s ≤ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) = s

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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

Tactic:
sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)

Premises used: Iff.mpr, sup_le, Set.image_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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)
a₁ : (↑t2 : Set M) ⊆ (↑s : Set M)
⊢ span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M) ≤ s

Tactic:
refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)

Premises used: Iff.mpr, sup_le, Set.image_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
y : P
hy : y ∈ (↑t1 : Set P)
⊢ y ∈ g ⁻¹' (↑s : Set M)

Tactic:
(hg y hy).1

Premises used: Set.Mem, setOf, Set.preimage, And.left
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
y : P
hy : y ∈ (↑t1 : Set P)
⊢ y ∈ g ⁻¹' (↑s : Set M)

Tactic:
exact (hg y hy).1

Premises used: And.left