awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + (n • a + x))
have h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (n • a + (a + x))
Tactic: rw [add_left_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (n • a + (a + x))
have h : a ∈ a +ᵥ (↑(closure t) : Set M)
Tactic: refine add_mem (nsmul_mem (mem_closure_of_mem ?_) _)
        (mem_closure_of_mem (vadd_mem_vadd_set hx))
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ a ∈ a +ᵥ (↑(closure t) : Set M)
have h : a + 0 ∈ a +ᵥ (↑(closure t) : Set M)
Tactic: nth_rw 2 [← add_zero a]
-- 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
⊢ IsSemilinearSet (↑(closure s) : Set M)
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ S)) : Set M)
Tactic: rcases hs with ⟨S, hS, hS', rfl⟩
Cleared hypotheses: s, 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' : ∀ t ∈ s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ s)) : Set M)
hS' : ∀ t ∈ insert a s, IsLinearSet t
⊢ IsSemilinearSet (↑(closure (⋃₀ insert a s)) : Set M)
have hS'₁ : IsLinearSet a ∧ ∀ a ∈ s, IsLinearSet 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' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (↑(closure (⋃₀ S)) : Set M)
have empty : ∀ (hS' : ∀ (t : Set M), Membership.mem (γ := Set (Set M)) ∅ t → IsLinearSet t),
  IsSemilinearSet (↑(closure (⋃₀ ∅)) : Set 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 [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)
Cleared hypotheses: hS, 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
empty :
  ∀ (hS' : ∀ (t : Set M), Membership.mem (γ := Set (Set M)) ∅ t → IsLinearSet t),
    IsSemilinearSet (↑(closure (⋃₀ ∅)) : Set M)
⊢ IsSemilinearSet (↑(closure (⋃₀ S)) : Set M)
have insert : ∀ {a : Set M} {s : Set (Set M)},
  a ∉ s →
    s.Finite →
      ∀ (ih : ∀ (hS' : ∀ t ∈ s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ s)) : Set M))
        (hS' : ∀ t ∈ insert a s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ insert a s)) : Set 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 [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)
Cleared hypotheses: hS, 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 : IsProperLinearSet s
⊢ IsLinearSet s
have rcases : ∀ (a : M) (t : Set M) (ht : t.Finite), LinearIndepOn ℕ id t → IsLinearSet (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
inst : AddCommMonoid M
s : Set M
hs : IsProperSemilinearSet s
⊢ IsSemilinearSet s
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsProperLinearSet t), IsSemilinearSet (⋃₀ 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₁ s₂ : Set M
hs₁ : IsProperSemilinearSet s₁
hs₂ : IsProperSemilinearSet s₂
⊢ IsProperSemilinearSet (s₁ ∪ s₂)
have rcases : ∀ (S₁ : Set (Set M)) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsProperLinearSet t), IsProperSemilinearSet (⋃₀ 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₂ : IsProperSemilinearSet s₂
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ S₁ ∪ s₂)
have rcases : ∀ (S₂ : Set (Set M)) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsProperLinearSet t), IsProperSemilinearSet (⋃₀ 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₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)
have rw : IsProperSemilinearSet (⋃₀ (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₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ (S₁ ∪ S₂))
have refine : ∀ (s : Set M) (hs : s ∈ S₁ ∪ S₂), IsProperLinearSet 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₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∪ S₂
⊢ IsProperLinearSet 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, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ s)
hS' : ∀ s_1 ∈ insert a s, IsProperSemilinearSet s_1
⊢ IsProperSemilinearSet (⋃₀ insert a s)
have hS'₁ : IsProperSemilinearSet a ∧ ∀ a ∈ s, IsProperSemilinearSet 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, IsProperSemilinearSet s
⊢ IsProperSemilinearSet (⋃₀ S)
have empty : ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsProperSemilinearSet s),
  IsProperSemilinearSet.{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'
-- 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, IsProperSemilinearSet s
empty :
  ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsProperSemilinearSet s),
    IsProperSemilinearSet.{u_1} (M := M) (⋃₀ ∅)
⊢ IsProperSemilinearSet (⋃₀ S)
have insert : ∀ {a : Set M} {s : Set (Set M)},
  a ∉ s →
    s.Finite →
      ∀ (ih : ∀ (hS' : ∀ s_1 ∈ s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ s))
        (hS' : ∀ s_1 ∈ insert a s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ insert a s)
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'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ s, t i)
have rw : IsProperSemilinearSet (⋃₀ (t '' s))
Tactic: rw [← sUnion_image]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet (⋃₀ (t '' s))
have apply : ∀ s_1 ∈ t '' s, IsProperSemilinearSet s_1
Tactic: apply sUnion (hs.image t)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
⊢ IsProperSemilinearSet s
have hs₁ : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)
Tactic: rw [isLinearSet_iff] 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 M
inst_1 : IsCancelAdd M
hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)
⊢ IsProperSemilinearSet s
have rcases : ∀ (a : M) (t : Finset M), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: rcases hs with ⟨a, t, 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
inst_1 : IsCancelAdd M
a : M
t : Finset M
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have h : ∀ (n : ℕ)
  (ih :
    ∀ m < n, ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
  (a : M) (t : Finset M) (hn : t.card = n), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
Cleared hypotheses: a, t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
n : ℕ
ih : ∀ m < n, ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
a : M
t : Finset M
hn : t.card = n
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have ih₁ : ∀ m < t.card, ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: subst hn
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have pos : ∀ (hindep : LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: by_cases hindep : LinearIndepOn ℕ id (t : Set M)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
pos : ∀ (hindep : LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have neg : ∀ (hindep : ¬LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: by_cases hindep : LinearIndepOn ℕ id (t : Set M)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
hindep : ¬LinearIndepOn ℕ id (↑t : Set M)
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have hindep₁ : ∃ t_1 ⊆ t, ∃ (f : M → ℕ), Eq (α := M) (∑ i ∈ t_1, f i • id i) (∑ i ∈ t \ t_1, f i • id i) ∧ ∃ i ∈ t_1, 0 < f i
Tactic: rw [not_linearIndepOn_finset_iffₒₛ] at hindep
Cleared hypotheses: hindep
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
hindep : ∃ t_1 ⊆ t, ∃ (f : M → ℕ), Eq (α := M) (∑ i ∈ t_1, f i • id i) (∑ i ∈ t \ t_1, f i • id i) ∧ ∃ i ∈ t_1, 0 < f i
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have neg : ∀ (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (heq : Eq (α := M) (∑ i ∈ t', f i • id i) (∑ i ∈ t \ t', f i • id i))
  (i : M) (hi : i ∈ t') (hfi : 0 < f i), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
Cleared hypotheses: hindep
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
heq : Eq (α := M) (∑ i ∈ t', f i • id i) (∑ i ∈ t \ t', f i • id i)
i : M
hi : i ∈ t'
hfi : 0 < f i
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have heq₁ : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
Tactic: simp only [Function.id_def] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have h : a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
  ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)
Tactic: convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
h :
  a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
    ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
have neg : IsProperSemilinearSet.{u_1} (M := M)
  (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
Tactic: convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
⊢ a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
    ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)
have h : ∀ (x : M),
  x ∈ a +ᵥ (↑(closure (↑t : Set M)) : Set M) ↔
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
x : M
⊢ (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) ↔
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
have h : (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) →
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
x : M
h :
  (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) →
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
⊢ (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) ↔
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
have h₁ : Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x →
  ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) (a +ᵥ y)
have hy₁ : ∃ (f : M → ℕ), Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = y
Tactic: rw [mem_closure_finset] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
y : M
hy : ∃ (f : M → ℕ), Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = y
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) (a +ᵥ y)
have h : ∀ (g : M → ℕ),
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: rcases hy with ⟨g, -, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have h : ∀ (n : ℕ)
  (ih' :
    ∀ m < n,
      ∀ (g : M → ℕ) (hn : g i = m),
        Membership.mem (γ := Set M)
          (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
          (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a)))
  (g : M → ℕ) (hn : g i = n),
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
n : ℕ
ih' :
  ∀ m < n,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
g : M → ℕ
hn : g i = n
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have ih'₁ : ∀ m < g i,
  ∀ (g : M → ℕ) (hn : g i = m),
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
      (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: subst hn
Cleared hypotheses: n, ih', hn
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have pos : ∀ (hfg : ∀ j ∈ t', f j ≤ g j),
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: by_cases! hfg : ∀ j ∈ t', f j ≤ g j