Theorem: factorization'.coprime_of_mem (FltRegular/FltThree/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 = (factorization' h).prod ∨ a = -(factorization' h).prod
⊢ IsCoprime b.re b.im

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
h1 : a = (factorization' h).prod ∨ a = -(factorization' h).prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ f.prod ∣ a

State before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = f.prod ∨ a = -f.prod
⊢ f.prod ∣ 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 = -f.prod
⊢ f.prod ∣ -f.prod

State before:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -f.prod
⊢ f.prod ∣ -f.prod
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 = -f.prod
⊢ f.prod ∣ f.prod

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