Theorem: factorization'.coprime_of_mem (Flt/Edwards.lean)

State before:
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
⊢ IsCoprime b.re b.im
Tactic:
obtain ⟨h1, -⟩ := factorization'_prop h
State after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
h1 : a = Multiset.prod (factorization' h) ∨ a = -Multiset.prod (factorization' h)
⊢ IsCoprime b.re b.im

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
h1 : a = Multiset.prod (factorization' h) ∨ a = -Multiset.prod (factorization' h)
⊢ IsCoprime b.re b.im
Tactic:
set f := factorization' h
State after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ IsCoprime b.re b.im

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ IsCoprime b.re b.im
Tactic:
apply Zsqrtd.coprime_of_dvd_coprime h
State after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ b ∣ a

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ b ∣ a
Tactic:
apply (Multiset.dvd_prod hmem).trans
State after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ Multiset.prod f ∣ a

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ Multiset.prod f ∣ a
Tactic:
cases' h1 with h1 h1 <;> rw [h1]
State after:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod f ∣ -Multiset.prod f

State before:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod f ∣ -Multiset.prod f
Tactic:
simp only [dvd_neg]
State after:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod (factorization' h) ∣ Multiset.prod (factorization' h)

State before:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod (factorization' h) ∣ Multiset.prod (factorization' h)
Tactic:
rfl
State after:
no goals