awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    {a : ι ⊕ ι → ℕ |
      ∃ (z : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
          ∃ (z' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
              a ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + z}
have a : IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
  {x : (ι ⊕ ι) ⊕ ι → ℕ |
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (x ∘ Sum.inr) ∧
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (x ∘ Sum.inl) ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + (x ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr}
Tactic: apply IsSemilinearSet.proj'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    ({a : (ι ⊕ ι) ⊕ ι → ℕ |
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (a ∘ Sum.inr)} ∩
      {a : (ι ⊕ ι) ⊕ ι → ℕ |
        ∃ (z' : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
            (a ∘ Sum.inl) ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr})
have a : IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
  {a : (ι ⊕ ι) ⊕ ι → ℕ |
    ∃ (z' : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
        (a ∘ Sum.inl) ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (LinearMap.funLeft ℕ ℕ Sum.inr)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ |
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (a ∘ Sum.inl) ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr}
have a : IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
  {x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (x ∘ Sum.inr) ∧
      ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x ∘ Sum.inl) ∘ Sum.inr}
Tactic: apply IsSemilinearSet.proj'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    ({a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (a ∘ Sum.inr)} ∩
      {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
          hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr})
have a : IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
  {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
    ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
      hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (LinearMap.funLeft ℕ ℕ Sum.inr)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
have a : ∀ (this : Fintype ι),
  IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
have h : ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
  ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
    HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols (fromCols 1 0) 0) 1 *ᵥ x)
Tactic: convert!
      Nat.isSemilinearSet_setOf_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) 0 (hs.base + i.1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 0) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 1) 1) 0) using 4
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
h :
  ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
    ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
      HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols (fromCols 1 0) 0) 1 *ᵥ x)
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
have h₁ : ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
  hs.base (s := s) + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x ∘ Sum.inl) ∘ Sum.inr =
    hs.base (s := s) + (↑i : ι → ℕ) + fromCols (fromCols (fromCols 0 1) 1) 0 *ᵥ x
Tactic: convert!
      Nat.isSemilinearSet_setOf_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) 0 (hs.base + i.1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 0) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 1) 1) 0) using 4
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ IsSemilinearSet sᶜ
have h : sᶜ = hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
Tactic: convert!
    hs.isSemilinearSet_setOfFractNe.union <|
      hs.isSemilinearSet_setOfFloorNeg.union <| hs.isSemilinearSet_setOfFloorPos using 1
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ sᶜ = hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
have h : ∀ (x : ι → ℕ), x ∈ sᶜ ↔ x ∈ hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x : ι → ℕ
⊢ x ∈ sᶜ ↔ x ∈ hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
have h : ¬(hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)) ↔
  hs.fract (s := s) x ≠ hs.base (s := s) ∨
    (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ∨
      hs.fract (s := s) x = hs.base (s := s) ∧
        ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x i
Tactic: simp only [mem_compl_iff, hs.mem_iff_fract_eq_and_floor_nonneg, IsProperLinearSet.setOfFractNe,
    IsProperLinearSet.setOfFloorNeg, IsProperLinearSet.setOfFloorPos, mem_union, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSemilinearSet s
⊢ IsSemilinearSet sᶜ
have rcases : ∀ (S : Set (Set (ι → ℕ))) (hS : S.Finite) (hS' : ∀ t ∈ S, IsProperLinearSet t) (hs : IsSemilinearSet (⋃₀ S)),
  IsSemilinearSet (⋃₀ S)ᶜ
Tactic: rcases hs.isProperSemilinearSet with ⟨S, hS, hS', rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋃₀ S)ᶜ
have simp_rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋂ i ∈ S, iᶜ)
Tactic: simp_rw [sUnion_eq_biUnion, compl_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ \ s₂)
have rcases : ∀ (P : AddSubmonoid M) (s₁' s₂' : Set ↥P) (hP : P.FG) (hs₁' : IsSemilinearSet s₁')
  (hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')) (hs₂' : IsSemilinearSet s₂')
  (hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')),
  IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' \ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
Tactic: rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩
Cleared hypotheses: s₁, s₂, hs₁, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' \ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
have rw : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' \ s₂'))
Tactic: rw [← image_diff Subtype.val_injective]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' \ s₂'))
have apply : IsSemilinearSet (s₁' \ s₂')
Tactic: apply image (f := P.subtype)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (s₁' \ s₂')
have hP₁ : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
Tactic: rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP
Cleared hypotheses: hP, hs₁', hs₁, hs₂', hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (s₁' \ s₂')
have rcases : ∀ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P) (hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤),
  IsSemilinearSet (s₁' \ s₂')
Tactic: rcases hP with ⟨n, f, hf⟩
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
⊢ IsSemilinearSet (s₁' \ s₂')
have hf₁ : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
Tactic: rw [AddMonoidHom.mrange_eq_top] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (s₁' \ s₂')
have rw : IsSemilinearSet (M := ↥P)
  (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
    ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))
Tactic: rw [← image_preimage_eq (s₁' \ s₂') hf, preimage_diff]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (M := ↥P)
    (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
      ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))
have hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
Tactic: apply image
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
have hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')
Tactic: apply Nat.isSemilinearSet_diff
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
have hs₃ : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
Tactic: apply Nat.isSemilinearSet_diff
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : AddMonoid.FG M
hs : IsSemilinearSet s
⊢ IsSemilinearSet sᶜ
have rw : IsSemilinearSet (univ \ s)
Tactic: rw [compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
⊢ IsLinearSet (↑P : Set M)
have rw : ∃ (a : M) (P_1 : AddSubmonoid M), P_1.FG ∧ (↑P : Set M) = a +ᵥ (↑P_1 : Set M)
Tactic: rw [isLinearSet_iff_exists_fg_eq_vadd]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
hs : IsLinearSet s
⊢ IsLinearSet (a +ᵥ s)
have rcases : ∀ (b : M) (t : Set M) (ht : t.Finite), IsLinearSet (a +ᵥ b +ᵥ (↑(closure t) : Set M))
Tactic: rcases hs with ⟨b, t, ht, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
⊢ a +ᵥ b +ᵥ (↑(closure t) : Set M) = (a + b) +ᵥ (↑(closure t) : Set M)
have rw : (a + b) +ᵥ (↑(closure t) : Set M) = (a + b) +ᵥ (↑(closure t) : Set M)
Tactic: rw [vadd_vadd]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
⊢ IsLinearSet (s₁ + s₂)
have rcases : ∀ (a : M) (t₁ : Set M) (ht₁ : t₁.Finite), IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + s₂)
Tactic: rcases hs₁ with ⟨a, t₁, ht₁, rfl⟩
Cleared hypotheses: s₁, hs₁
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₂ : Set M
hs₂ : IsLinearSet s₂
a : M
t₁ : Set M
ht₁ : t₁.Finite
⊢ IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + s₂)
have rcases : ∀ (b : M) (t₂ : Set M) (ht₂ : t₂.Finite), IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + (b +ᵥ (↑(closure t₂) : Set M)))
Tactic: rcases hs₂ with ⟨b, t₂, ht₂, rfl⟩
Cleared hypotheses: s₂, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
s : Set M
hs : IsLinearSet s
f : F
⊢ IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
have rcases : ∀ (a : M) (t : Set M) (ht : t.Finite), IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)))
Tactic: rcases hs with ⟨a, t, ht, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
a : M
t : Set M
ht : t.Finite
⊢ IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)))
have refine : (⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)) =
  HVAdd.hVAdd (α := N) ((f : (a : M) → N) a : N) (↑(closure ((⇑f : (a : M) → N) '' t)) : Set N)
Tactic: refine ⟨f a, f '' t, ht.image f, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∪ s₂)
have rcases : ∀ (S₁ : Set (Set M)) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∪ s₂)
Tactic: rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
Cleared hypotheses: s₁, hs₁
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₂ : Set M
hs₂ : IsSemilinearSet s₂
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ ∪ s₂)
have rcases : ∀ (S₂ : Set (Set M)) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)
Tactic: rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
Cleared hypotheses: s₂, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)
have rw : IsSemilinearSet (⋃₀ (S₁ ∪ S₂))
Tactic: rw [← sUnion_union]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ (S₁ ∪ S₂))
have refine : ∀ (s : Set M) (hs : s ∈ S₁ ∪ S₂), IsLinearSet s
Tactic: refine ⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
s : Set M
hs : s ∈ S₁ ∪ S₂
⊢ IsLinearSet s
have hs₁ : s ∈ S₁ ∨ s ∈ S₂
Tactic: rw [mem_union] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ s_1 ∈ s, IsSemilinearSet s_1), IsSemilinearSet (⋃₀ s)
hS' : ∀ s_1 ∈ insert a s, IsSemilinearSet s_1
⊢ IsSemilinearSet (⋃₀ insert a s)
have hS'₁ : IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet a
Tactic: simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ s ∈ S, IsSemilinearSet s
⊢ IsSemilinearSet (⋃₀ S)
have empty : ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s),
  IsSemilinearSet.{u_1} (M := M) (⋃₀ ∅)
Tactic: induction S, hS using Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.union (ih hS'.2)
Cleared hypotheses: hS, hS'