awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
⊢ IsSemilinearSet s
have a₁ : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  (a : ι → ℕ) (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
  (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i), IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a₁ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    (a : ι → ℕ) (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
    (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
    IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
⊢ IsSemilinearSet s
have a₂ : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty),
  IsSemilinearSet s
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a₁ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    (a : ι → ℕ) (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
    (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
    IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
a₂ a₃ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty),
    IsSemilinearSet s
⊢ IsSemilinearSet s
have a₄ : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
  (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}), IsSemilinearSet s
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a₁ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    (a : ι → ℕ) (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
    (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
    IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
a₂ a₃ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty),
    IsSemilinearSet s
a₄ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
    (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}), IsSemilinearSet s
⊢ IsSemilinearSet s
have h : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
  (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}),
  s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
have hs : IsSlice.{u_3} (M := ι → ℕ)
  {x : ι → ℕ | HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
Tactic: apply isSemilinearSet_of_isSlice
-- 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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x : ι → ℕ
hx :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    x
y z : ι → ℕ
hy :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + y)
hz :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + z)
⊢ Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + y + z)
have hs : ∀ (hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M))
  (hy :
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
      HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
  (hz :
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
      HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)),
  HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
Tactic: simp only [mem_setOf, map_add, ← add_assoc] at *
Cleared hypotheses: hx, hy, hz
-- 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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)
hy :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M)
hz :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)
| HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
    ((f : (a : ι → ℕ) → M) z : M)
have rw : HAdd.hAdd (β := M)
  (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
  ((g : (a : ι → ℕ) → M) z : M)
Tactic: rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]
-- 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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)
hy :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M)
hz :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
have conv_lhs : HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
    ((f : (a : ι → ℕ) → M) z : M) =
  HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
    ((g : (a : ι → ℕ) → M) z : M)
Tactic: conv_lhs => rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]
-- 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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)
hy :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M)
hz :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)
conv_lhs :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
have hs : HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
    ((g : (a : ι → ℕ) → M) z : M) =
  HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
    ((g : (a : ι → ℕ) → M) z : M)
Tactic: conv_lhs => rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]
-- 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
⊢ IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}
have rcases : ∀ (n : ℕ) (h : (Fin n → ℕ) →+ M) (hh : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange h) ⊤),
  IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}
Tactic: rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, h, hh⟩
-- 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange h) ⊤
⊢ IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}
have hh₁ : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
Tactic: rw [AddMonoidHom.mrange_eq_top] at hh
Cleared hypotheses: hh
-- 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}
have rw : IsSemilinearSet (M := M)
  (image (α := Fin n → ℕ) (⇑h : (a : Fin n → ℕ) → M)
    {a_1 : Fin n → ℕ |
      HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
        HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)})
Tactic: rw [← image_preimage_eq { x | a + f x = b + g x } hh, preimage_setOf_eq]
-- 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := M)
    (image (α := Fin n → ℕ) (⇑h : (a : Fin n → ℕ) → M)
      {a_1 : Fin n → ℕ |
        HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
          HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)})
have hs : IsSemilinearSet (M := Fin n → ℕ)
  {a_1 : Fin n → ℕ |
    HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
      HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)}
Tactic: apply IsSemilinearSet.image
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
⊢ IsLinearSet s ↔
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
      s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M))
have simp_rw : (∃ (a : M) (P : AddSubmonoid M),
    (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
  ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
Tactic: simp_rw [isLinearSet_iff_exists_fg_eq_vadd, fg_iff_exists_fin_addMonoidHom,
    ← AddMonoidHom.coe_mrange]
-- 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) (P : AddSubmonoid M),
      (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
have a : ∀ (a : M),
  (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
Tactic: congr! with a
-- 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
⊢ (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
have a₁ : (∃ (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 : s = a +ᵥ (↑P : Set M)),
    s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
Tactic: refine ⟨fun ⟨P, ⟨n, f, hf⟩, hs⟩ => ⟨n, f, ?_⟩, fun ⟨n, f, hs⟩ => ⟨_, ⟨n, f, rfl⟩, ?_⟩⟩
-- 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
a₁ :
  (∃ (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 : s = a +ᵥ (↑P : Set M)),
      s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
have a₂ : (∃ (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)
Tactic: refine ⟨fun ⟨P, ⟨n, f, hf⟩, hs⟩ => ⟨n, f, ?_⟩, fun ⟨n, f, hs⟩ => ⟨_, ⟨n, f, rfl⟩, ?_⟩⟩