awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)
P : AddSubmonoid M
n : ℕ
f : (Fin n → ℕ) →+ M
hf : AddMonoidHom.mrange f = P
hs a₁ : s = a +ᵥ (↑P : Set M)
⊢ s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
have a₂ : a +ᵥ (↑P : Set M) = a +ᵥ (↑P : Set M)
Tactic: rw [hf, hs]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
have a₁ : a +ᵥ (↑(AddMonoidHom.mrange f) : Set M) = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
⊢ IsLinearSet s ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
have rw : (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
    s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
  ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
Tactic: rw [isLinearSet_iff_exists_fin_addMonoidHom]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
⊢ (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
have refine_1 : ∀ (v : ι → ℕ) (n : ℕ),
  (∃ (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) →
    ∀ (f : (Fin n → ℕ) →+ ι → ℕ)
      (hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))),
      s =
        {x : ι → ℕ |
          ∃ (x_1 : Fin n → ℕ),
            v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}
Tactic: refine exists₂_congr fun v n => ⟨fun ⟨f, hf⟩ => ⟨f.toNatLinearMap.toMatrix', ?_⟩, fun ⟨A, hA⟩ =>
    ⟨A.mulVecLin, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
refine_1 :
  ∀ (v : ι → ℕ) (n : ℕ),
    (∃ (f : (Fin n → ℕ) →+ ι → ℕ),
        s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) →
      ∀ (f : (Fin n → ℕ) →+ ι → ℕ)
        (hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))),
        s =
          {x : ι → ℕ |
            ∃ (x_1 : Fin n → ℕ),
              v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 =
                x}
⊢ (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
have refine_2 : ∀ (v : ι → ℕ) (n : ℕ),
  (∃ (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}) →
    ∀ (A : Matrix ι (Fin n) ℕ) (hA : s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}),
      s =
        HVAdd.hVAdd (β := Set (ι → ℕ)) v
          (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))
Tactic: refine exists₂_congr fun v n => ⟨fun ⟨f, hf⟩ => ⟨f.toNatLinearMap.toMatrix', ?_⟩, fun ⟨A, hA⟩ =>
    ⟨A.mulVecLin, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h :
  ∃ (f : (Fin n → ℕ) →+ ι → ℕ),
    s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
⊢ s =
    {x : ι → ℕ |
      ∃ (x_1 : Fin n → ℕ),
        v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}
have refine_1 : ∀ (x : ι → ℕ),
  x ∈ s ↔
    Membership.mem (γ := Set (ι → ℕ))
      {x : ι → ℕ |
        ∃ (x_1 : Fin n → ℕ),
          v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h : ∃ (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
⊢ s =
    HVAdd.hVAdd (β := Set (ι → ℕ)) v
      (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))
have refine_2 : ∀ (x : ι → ℕ),
  x ∈ s ↔
    x ∈
      HVAdd.hVAdd (β := Set (ι → ℕ)) v
        (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
s : Set M
hs : IsLinearSet s
f : F
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)
have rw : ∀
  (hs :
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
      s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M)))
  (f : F), IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)
Tactic: rw [isLinearSet_iff_exists_fin_addMonoidHom] at hs
Cleared hypotheses: hs, f
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
s : Set M
hs :
  ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
    s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M))
f : F
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)
have rcases : ∀ (a : M) (n : ℕ) (g : (Fin n → ℕ) →+ M),
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    ((⇑f : (a : ι → ℕ) → M) ⁻¹' HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)))
Tactic: rcases hs with ⟨a, n, g, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      Membership.mem (α := M) (HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)))
        ((f : (a : ι → ℕ) → M) x : M)}
have simp : IsSemilinearSet.{u_3} (M := ι → ℕ)
  {x : ι → ℕ | ∃ (a_1 : Fin n → ℕ), HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) a_1 : M) = (f : (a : ι → ℕ) → M) x}
Tactic: simp only [mem_vadd_set, mem_range, vadd_eq_add, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      ∃ (a_1 : Fin n → ℕ), HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) a_1 : M) = (f : (a : ι → ℕ) → M) x}
have a₁ : IsSemilinearSet.{u_3} (M := ι ⊕ Fin n → ℕ)
  {x : ι ⊕ Fin n → ℕ |
    HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) (x ∘ Sum.inr) : M) = (f : (a : ι → ℕ) → M) (x ∘ Sum.inl)}
Tactic: apply IsSemilinearSet.proj'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ Fin n → ℕ)
    {x : ι ⊕ Fin n → ℕ |
      HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) (x ∘ Sum.inr) : M) = (f : (a : ι → ℕ) → M) (x ∘ Sum.inl)}
have h : ∀ (x : ι ⊕ Fin n → ℕ),
  (f : (a : ι → ℕ) → M) (x ∘ Sum.inl) =
    HAdd.hAdd (α := M) (β := M) (0 : M)
      ((AddMonoidHom.comp (↑f : (ι → ℕ) →+ M)
              (LinearMap.toAddMonoidHom (modM₁ := Pi.Function.module (ι ⊕ Fin n) ℕ ℕ) (LinearMap.funLeft ℕ ℕ Sum.inl)) :
            (a : ι ⊕ Fin n → ℕ) → M)
          x :
        M)
Tactic: convert!
    isSemilinearSet_setOf_eq a 0 (g.comp (LinearMap.funLeft ℕ ℕ Sum.inr).toAddMonoidHom)
      ((f : (ι → ℕ) →+ M).comp (LinearMap.funLeft ℕ ℕ Sum.inl).toAddMonoidHom)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
s : Set M
hs : IsSemilinearSet s
f : F
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
  IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' ⋃₀ S)
Tactic: rcases hs with ⟨S, hS, hS', rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' ⋃₀ S)
have simp_rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ i ∈ S, (⇑f : (a : ι → ℕ) → M) ⁻¹' i)
Tactic: simp_rw [sUnion_eq_biUnion, preimage_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
⊢ IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)
have rcases : ∀ (n : ℕ) (g : (Fin n → ℕ) →+ M) (hg : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange g) ⊤),
  IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)
Tactic: rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, g, hg⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange g) ⊤
⊢ IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)
have hg₁ : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
Tactic: rw [AddMonoidHom.mrange_eq_top] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)
have rw : IsSemilinearSet (M := M)
  (Set.image (α := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)
    (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s)))
Tactic: rw [← image_preimage_eq (f ⁻¹' s) hg]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := M)
    (Set.image (α := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)
      (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s)))
have hs₁ : IsSemilinearSet (M := Fin n → ℕ) (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s))
Tactic: apply image
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := Fin n → ℕ) (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s))
have hs₁ : IsSemilinearSet (M := Fin n → ℕ) ((⇑(AddMonoidHom.comp (↑f : M →+ N) g) : (a : Fin n → ℕ) → N) ⁻¹' s)
Tactic: rw [← preimage_comp, ← AddMonoidHom.coe_coe, ← AddMonoidHom.coe_comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsLinearSet s
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsLinearSet s' ∧ s = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have rcases : ∀ (a : M) (t : Set M) (ht : t.Finite),
  ∃ (P : AddSubmonoid M) (s' : Set ↥P),
    P.FG ∧ IsLinearSet s' ∧ a +ᵥ (↑(closure t) : Set M) = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
Tactic: rcases hs with ⟨a, t, ht, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P),
    P.FG ∧ IsLinearSet s' ∧ a +ᵥ (↑(closure t) : Set M) = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have refine : a +ᵥ (↑(closure t) : Set M) =
  Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ''
    HVAdd.hVAdd (α := ↥(closure (insert a t)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a sorry)
      (↑(closure
            (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ⁻¹' t)) :
        Set ↥(closure (insert a t)))
Tactic: refine ⟨_, _, (fg_iff _).2 ⟨insert a t, rfl, ht.insert a⟩,
    ⟨⟨_, mem_closure_of_mem (mem_insert a t)⟩, _, ht.preimage Subtype.val_injective.injOn, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ (↑(closure t) : Set M) =
    Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ''
      HVAdd.hVAdd (α := ↥(closure (insert a t)))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯)
        (↑(closure
              (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ⁻¹' t)) :
          Set ↥(closure (insert a t)))
have rw : a +ᵥ (↑(closure t) : Set M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a sorry) : M) +ᵥ
    (↑(closure
          (Set.image (α := ↥(closure (insert a t)))
            (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
            ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))) :
      Set M)
Tactic: rw [← coe_subtype, image_vadd_distrib, subtype_apply, ← coe_map, AddMonoidHom.map_mclosure]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ (↑(closure t) : Set M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯) : M) +ᵥ
      (↑(closure
            (Set.image (α := ↥(closure (insert a t)))
              (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
              ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))) :
        Set M)
have e_a : t =
  Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
    ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t)
Tactic: congr
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ t =
    Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
      ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t)
have e_a : ∀ (x : M),
  x ∈ t ↔
    Membership.mem (γ := Set M)
      (Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
        ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
  ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
Tactic: rcases hs with ⟨S, hS, hS', rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have choose! : ∀ (P : (s : Set M) → AddSubmonoid M) (t : (s : Set M) → Set ↥(P s)) (hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG)
  (ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s))
  (ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s),
  ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
Tactic: choose! P t hP ht ht' using fun s hs => (hS' s hs).exists_fg_eq_subtypeVal
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have this : Finite.{u_1 + 1} (↑S : Type u_1)
Tactic: haveI : Finite S := hS
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
this : Finite.{u_1 + 1} (↑S : Type u_1)
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
have refine : ⋃₀ S =
  Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
    (⋃ (s : (↑S : Type u_1)),
      Set.image (α := ↥(P (↑s : Set M)))
        (⇑(AddSubmonoid.inclusion sorry : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
          (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
        (t (↑s : Set M)))
Tactic: refine ⟨⨆ s : S, P s, ⋃ (s : S), AddSubmonoid.inclusion (le_iSup _ s) '' t s.1,
    .iSup _ fun s => hP s s.2, .iUnion fun s => (ht s s.2).isSemilinearSet.image _, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
this : Finite.{u_1 + 1} (↑S : Type u_1)
⊢ ⋃₀ S =
    Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M)))
have simp_rw : Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
  (Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
    (⋃ (s : (↑S : Type u_1)),
      Set.image (α := ↥(P (↑s : Set M)))
        (⇑(AddSubmonoid.inclusion sorry : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
          (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
        (t (↑s : Set M))))
Tactic: simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]