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
S : Set (Set M)
hS : S.Finite
hS' : ∀ s ∈ S, IsSemilinearSet s
empty :
  ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s),
    IsSemilinearSet.{u_1} (M := M) (⋃₀ ∅)
⊢ IsSemilinearSet (⋃₀ S)
have insert : ∀ {a : Set M} {s : Set (Set M)},
  a ∉ s →
    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)
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
inst_1 : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ IsSemilinearSet (⋃₀ range s)
have apply : ∀ s_1 ∈ range s, IsSemilinearSet s_1
Tactic: apply sUnion (finite_range s)
-- 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, IsSemilinearSet (t i)
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ i ∈ s, t i)
have rw : IsSemilinearSet (⋃₀ (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, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋃₀ (t '' s))
have apply : ∀ s_1 ∈ t '' s, IsSemilinearSet s_1
Tactic: apply sUnion (hs.image t)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ IsSemilinearSet s
have rw : IsSemilinearSet.{u_1} (M := M) (⋃ x ∈ s, {x})
Tactic: rw [← biUnion_of_singleton s]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ x ∈ s, {x})
have apply : ∀ i ∈ s, IsSemilinearSet (M := M) {i}
Tactic: apply biUnion hs
-- 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 : IsSemilinearSet s
⊢ IsSemilinearSet (a +ᵥ s)
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsSemilinearSet (a +ᵥ ⋃₀ 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
a : M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (a +ᵥ ⋃₀ S)
have rw : IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S, a +ᵥ s)
Tactic: rw [vadd_set_sUnion]
-- 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 simp_rw : IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S₁, ⋃ t ∈ S₂, s + t)
Tactic: simp_rw [sUnion_add, add_sUnion]
-- 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 : IsSemilinearSet s
f : F
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
  IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' ⋃₀ 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
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
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' ⋃₀ S)
have simp_rw : IsSemilinearSet.{u_2} (M := N) (⋃ i ∈ S, (⇑f : (a : M) → N) '' i)
Tactic: simp_rw [sUnion_eq_biUnion, image_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) ↔ IsSemilinearSet s
have mp : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) → IsSemilinearSet s
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
mp : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) → IsSemilinearSet s
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) ↔ IsSemilinearSet s
have mpr : IsSemilinearSet s → IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
⊢ IsSemilinearSet s
have h₁ : s = image.{u_2, u_1} (α := N) (⇑(AddEquiv.symm (↑f : M ≃+ N)) : (a : N) → M) ((⇑f : (a : M) → N) '' s)
Tactic: convert! h.image (f : M ≃+ N).symm
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
⊢ IsSemilinearSet (M := ι → M) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
have h : Eq (α := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
  ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s)
Tactic: convert! hs.image (LinearMap.funLeft ℕ M Sum.inl)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
⊢ Eq (α := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s)
have h : ∀ (x : ι → M),
  Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x ↔
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
⊢ Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x ↔
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
have h : Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x →
  Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
h :
  Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x →
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
⊢ Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x ↔
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
have h₁ : Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x →
  Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
y : ι ⊕ κ → M
hy : y ∈ s
⊢ Membership.mem (α := ι → M) (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y : ι → M)
have h : Sum.elim ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y) (y ∘ Sum.inr) ∈ s
Tactic: refine ⟨y ∘ Sum.inr, ?_⟩
-- 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
⊢ IsSemilinearSet (↑(closure s) : Set M)
have rcases : ∀ (a : M) (t : Set M) (ht : t.Finite), IsSemilinearSet (↑(closure (a +ᵥ (↑(closure t) : Set M))) : 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
a : M
t : Set M
ht : t.Finite
⊢ IsSemilinearSet (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M)
have h : (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) = {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
Tactic: convert! (IsSemilinearSet.singleton 0).union (isSemilinearSet ⟨a, { a } ∪ t, by simp [ht], rfl⟩)
-- 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
⊢ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) = {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
have h : ∀ (x : M), x ∈ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) ↔ x ∈ {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
Tactic: ext x
-- 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
x : M
⊢ x ∈ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) ↔ x ∈ {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
have h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x ↔
  x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
Tactic: simp only [SetLike.mem_coe, singleton_union, mem_insert_iff, mem_vadd_set, vadd_eq_add]
-- 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
x : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x ↔
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x →
  x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
Tactic: constructor
-- 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
x : M
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x →
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x ↔
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h₁ : (x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x) →
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : 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
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : x ∈ a +ᵥ (↑(closure t) : Set M)
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h : ∀ (x : M) (hx : x ∈ (↑(closure t) : Set M)),
  Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ a +ᵥ x) x) 0 ∨
    ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = (fun (x : M) ↦ a +ᵥ x) x
Tactic: rcases hx with ⟨x, hx, rfl⟩
Cleared hypotheses: x, 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
x_1 x y : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₁ : x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
⊢ x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = x + y
have h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
  0 + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = 0 + y
Tactic: rcases ih₁ with rfl | ⟨x, hx, rfl⟩
Cleared hypotheses: x, hx, ih₁
-- 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
x_1 x y : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₁ : x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
    0 + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = 0 + y
⊢ x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = x + y
have h₁ : ∀ (x : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x),
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x) →
    a + x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + y
Tactic: rcases ih₁ with rfl | ⟨x, hx, rfl⟩
Cleared hypotheses: x, hx, ih₁
-- 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
x_1 y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
⊢ a + x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + y
have h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
  a + x + 0 = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = a + x + 0
Tactic: rcases ih₂ with rfl | ⟨y, hy, rfl⟩
Cleared hypotheses: y, hy, ih₂
-- 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
x_1 y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
    a + x + 0 = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = a + x + 0
⊢ a + x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + y
have h₁ : ∀ (y : M) (hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y),
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y) →
    a + x + (a + y) = 0 ∨
      ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + (a + y)
Tactic: rcases ih₂ with rfl | ⟨y, hy, rfl⟩
Cleared hypotheses: y, hy, ih₂
-- 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
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y
hy_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y)
⊢ a + x + (a + y) = 0 ∨
    ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + (a + y)
have h : a + (a + (x + y)) = a + x + (a + y)
Tactic: refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
-- 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
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y
hy_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y)
⊢ a + (a + (x + y)) = a + x + (a + y)
have h : a + a + x + y = a + x + a + y
Tactic: simp_rw [← add_assoc, add_right_comm a a x]
-- 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
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h : ∀ (x : M) (hx : x ∈ a +ᵥ (↑(closure t) : Set M)),
  x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
Tactic: induction hx using closure_induction with
    | mem x hx =>
      rcases hx with ⟨x, hx, rfl⟩
      exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩
    | zero => exact Or.inl rfl
    | add x y _ _ ih₁ ih₂ =>
      rcases ih₁ with rfl | ⟨x, hx, rfl⟩
      · simpa
      · rcases ih₂ with rfl | ⟨y, hy, rfl⟩
        · exact Or.inr ⟨x, hx, by simp⟩
        · refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
          simp_rw [← add_assoc, add_right_comm a a x]
Cleared hypotheses: 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
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
h :
  ∀ (x : M) (hx : x ∈ a +ᵥ (↑(closure t) : Set M)),
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h₁ : Eq.{u_1 + 1} (α := M) 0 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = 0
Tactic: induction hx using closure_induction with
    | mem x hx =>
      rcases hx with ⟨x, hx, rfl⟩
      exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩
    | zero => exact Or.inl rfl
    | add x y _ _ ih₁ ih₂ =>
      rcases ih₁ with rfl | ⟨x, hx, rfl⟩
      · simpa
      · rcases ih₂ with rfl | ⟨y, hy, rfl⟩
        · exact Or.inr ⟨x, hx, by simp⟩
        · refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
          simp_rw [← add_assoc, add_right_comm a a x]
Cleared hypotheses: 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
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
h :
  ∀ (x : M) (hx : x ∈ a +ᵥ (↑(closure t) : Set M)),
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
h₁ : Eq.{u_1 + 1} (α := M) 0 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = 0
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
have h₂ : ∀ (x y : M),
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x →
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y →
      ∀ (ih₁ : x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x)
        (ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y),
        x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = x + y
Tactic: induction hx using closure_induction with
    | mem x hx =>
      rcases hx with ⟨x, hx, rfl⟩
      exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩
    | zero => exact Or.inl rfl
    | add x y _ _ ih₁ ih₂ =>
      rcases ih₁ with rfl | ⟨x, hx, rfl⟩
      · simpa
      · rcases ih₂ with rfl | ⟨y, hy, rfl⟩
        · exact Or.inr ⟨x, hx, by simp⟩
        · refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
          simp_rw [← add_assoc, add_right_comm a a x]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
have hx₁ : ∃ (y : M), (∃ (n : ℕ), n • a = y) ∧ ∃ (z : M), Membership.mem (γ := AddSubmonoid M) (closure t) z ∧ y + z = x
Tactic: simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx
Cleared hypotheses: 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
x : M
hx : ∃ (y : M), (∃ (n : ℕ), n • a = y) ∧ ∃ (z : M), Membership.mem (γ := AddSubmonoid M) (closure t) z ∧ y + z = x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
have h : ∀ (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))
Tactic: rcases hx with ⟨_, ⟨n, rfl⟩, ⟨x, hx, rfl⟩⟩
Cleared hypotheses: x, hx