Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case neg.hu₁
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ u' + u ∈ f a

pp: case neg.hu₂
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ u' + u ≠ 0

pp: case neg.hxy
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ a + x + (w' + (u' + u)) ∈ s

Tactic:
· exact add_mem hu'₁ hu₁

Goal state after:
case neg.hu₂
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ u' + u ≠ 0

case neg.hxy
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ a + x + (w' + (u' + u)) ∈ s