case intro.intro
ι : Type ?u.8005
α : Type ?u.8008
M : Type ?u.8011
N : Type ?u.8014
P : Type ?u.8017
M₀ : Type ?u.8020
G : Type ?u.8023
R : Type ?u.8026
l : List ℤ
h : prod l = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
ι : Type ?u.8005
α : Type ?u.8008
M : Type ?u.8011
N : Type ?u.8014
P : Type ?u.8017
M₀ : Type ?u.8020
G : Type ?u.8023
R : Type ?u.8026
l : List ℤ
h : prod l = -1
⊢ -1 ∈ l
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
no goals
case intro.intro
ι : Type ?u.8005
α : Type ?u.8008
M : Type ?u.8011
N : Type ?u.8014
P : Type ?u.8017
M₀ : Type ?u.8020
G : Type ?u.8023
R : Type ?u.8026
l : List ℤ
h : prod l = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
exact
  Or.resolve_left
      (Int.isUnit_iff.mp
        (prod_isUnit_iff.mp (h.symm ▸ IsUnit.neg isUnit_one : IsUnit l.prod) x h₁))
      h₂ ▸
    h₁
no goals
ι : Type ?u.8005
α : Type ?u.8008
M : Type ?u.8011
N : Type ?u.8014
P : Type ?u.8017
M₀ : Type ?u.8020
G : Type ?u.8023
R : Type ?u.8026
l : List ℤ
h : prod l = -1
⊢ -1 ≠ 1
decide