[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ IsCoprime m n ↔ gcd m n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ IsCoprime m n → gcd m n = 1
[PROOFSTEP]
rintro ⟨a, b, h⟩
[GOAL]
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
⊢ gcd m n = 1
[PROOFSTEP]
have : 1 = m * a + n * b := by rwa [mul_comm m, mul_comm n, eq_comm]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
⊢ 1 = m * a + n * b
[PROOFSTEP]
rwa [mul_comm m, mul_comm n, eq_comm]
[GOAL]
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
this : 1 = m * a + n * b
⊢ gcd m n = 1
[PROOFSTEP]
exact Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, this⟩)
[GOAL]
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcd m n = 1 → IsCoprime m n
[PROOFSTEP]
rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
[GOAL]
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcdA m n * m + gcdB m n * n = 1 → ∃ a b, a * m + b * n = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
h : gcdA m n * m + gcdB m n * n = 1
⊢ ∃ a b, a * m + b * n = 1
[PROOFSTEP]
exact ⟨_, _, h⟩
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
⊢ IsCoprime ↑m ↑n ↔ coprime m n
[PROOFSTEP]
rw [Int.isCoprime_iff_gcd_eq_one, Int.coe_nat_gcd]
[GOAL]
R : Type u
I : Type v
inst✝² : CommSemiring R
x y z : R
s : I → R
t : Finset I
A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : Nat.coprime a b
⊢ IsCoprime ↑a ↑b
[PROOFSTEP]
simpa only [map_natCast] using IsCoprime.map (Nat.coprime.isCoprime h) (Int.castRingHom A)
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : ¬b ∈ t
ih : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
⊢ IsCoprime (∏ i in insert b t, s i) x
[PROOFSTEP]
rw [Finset.prod_insert hbt]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : ¬b ∈ t
ih : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
[PROOFSTEP]
rw [Finset.forall_mem_insert] at H
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : ¬b ∈ t
ih : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : IsCoprime (s b) x ∧ ∀ (x_1 : I), x_1 ∈ t → IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
[PROOFSTEP]
exact H.1.mul_left (ih H.2)
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
⊢ (∀ (i : I), i ∈ t → IsCoprime x (s i)) → IsCoprime x (∏ i in t, s i)
[PROOFSTEP]
simpa only [isCoprime_comm] using IsCoprime.prod_left (R := R)
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsCoprime (s x✝) x
[PROOFSTEP]
simp
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : ¬b ∈ t
ih : IsCoprime (∏ i in t, s i) x ↔ ∀ (i : I), i ∈ t → IsCoprime (s i) x
⊢ IsCoprime (∏ i in insert b t, s i) x ↔ ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
[PROOFSTEP]
rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i in t, s i) ↔ ∀ (i : I), i ∈ t → IsCoprime x (s i)
[PROOFSTEP]
simpa only [isCoprime_comm] using IsCoprime.prod_left_iff (R := R)
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
⊢ ∀ ⦃a : I⦄ {s_1 : Finset I},
    ¬a ∈ s_1 →
      (Set.Pairwise (↑s_1) (IsCoprime on s) → (∀ (i : I), i ∈ s_1 → s i ∣ z) → ∏ x in s_1, s x ∣ z) →
        Set.Pairwise (↑(insert a s_1)) (IsCoprime on s) →
          (∀ (i : I), i ∈ insert a s_1 → s i ∣ z) → ∏ x in insert a s_1, s x ∣ z
[PROOFSTEP]
intro a r har ih Hs Hs1
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
⊢ ∏ x in insert a r, s x ∣ z
[PROOFSTEP]
rw [Finset.prod_insert har]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
⊢ s a * ∏ x in r, s x ∣ z
[PROOFSTEP]
have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ s a * ∏ x in r, s x ∣ z
[PROOFSTEP]
refine'
  (IsCoprime.prod_right fun i hir ↦
        Hs aux1 (Finset.mem_insert_of_mem hir) <| by
          rintro rfl
          exact har hir).mul_dvd
    (Hs1 a aux1) (ih (Hs.mono _) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
aux1 : a ∈ ↑(insert a r)
i : I
hir : i ∈ r
⊢ a ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
aux1 : a ∈ ↑(insert a r)
hir : a ∈ r
⊢ False
[PROOFSTEP]
exact har hir
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : ¬a ∈ r
ih : Set.Pairwise (↑r) (IsCoprime on s) → (∀ (i : I), i ∈ r → s i ∣ z) → ∏ x in r, s x ∣ z
Hs : Set.Pairwise (↑(insert a r)) (IsCoprime on s)
Hs1 : ∀ (i : I), i ∈ insert a r → s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ ↑r ⊆ ↑(insert a r)
[PROOFSTEP]
simp only [Finset.coe_insert, Set.subset_insert]
[GOAL]
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h : Finset.Nonempty t
⊢ (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
[PROOFSTEP]
refine' h.cons_induction _ _
[GOAL]
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h : Finset.Nonempty t
⊢ ∀ (a : I), (∃ μ, ∑ i in {a}, μ i * ∏ j in {a} \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
[PROOFSTEP]
simp only [sum_singleton, Finset.sdiff_self, prod_empty, mul_one, exists_apply_eq, Pairwise, Ne.def, true_iff_iff]
[GOAL]
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h : Finset.Nonempty t
⊢ ∀ (a : I) ⦃i j : { x // x ∈ {a} }⦄, ¬i = j → (IsCoprime on fun i => s ↑i) i j
[PROOFSTEP]
rintro a ⟨i, hi⟩ ⟨j, hj⟩ h
[GOAL]
case refine'_1.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t
a i : I
hi : i ∈ {a}
j : I
hj : j ∈ {a}
h : ¬{ val := i, property := hi } = { val := j, property := hj }
⊢ (IsCoprime on fun i => s ↑i) { val := i, property := hi } { val := j, property := hj }
[PROOFSTEP]
rw [Finset.mem_singleton] at hi hj
[GOAL]
case refine'_1.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t
a i : I
hi✝ : i ∈ {a}
hi : i = a
j : I
hj✝ : j ∈ {a}
hj : j = a
h : ¬{ val := i, property := hi✝ } = { val := j, property := hj✝ }
⊢ (IsCoprime on fun i => s ↑i) { val := i, property := hi✝ } { val := j, property := hj✝ }
[PROOFSTEP]
simp [hi, hj] at h
[GOAL]
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
h : Finset.Nonempty t
⊢ ∀ ⦃a : I⦄ (s_1 : Finset I) (h : ¬a ∈ s_1),
    Finset.Nonempty s_1 →
      ((∃ μ, ∑ i in s_1, μ i * ∏ j in s_1 \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)) →
        ((∃ μ, ∑ i in cons a s_1 h, μ i * ∏ j in cons a s_1 h \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i))
[PROOFSTEP]
intro a t hat h ih
[GOAL]
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
⊢ (∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
[PROOFSTEP]
rw [pairwise_cons']
[GOAL]
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
⊢ (∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
have mem : ∀ x ∈ t, a ∈ insert a t \ { x } := fun x hx ↦
  by
  rw [mem_sdiff, mem_singleton]
  refine ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
[GOAL]
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t \ {x}
[PROOFSTEP]
rw [mem_sdiff, mem_singleton]
[GOAL]
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t ∧ ¬a = x
[PROOFSTEP]
refine ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
[GOAL]
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1) →
    Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
rintro ⟨μ, hμ⟩
[GOAL]
case refine'_2.mp.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ : ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1
⊢ Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
[GOAL]
case refine'_2.mp.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
⊢ Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
refine' ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
⊢ ∑ i in t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x => s a) i * ∏ j in t \ {i}, s j = 1
[PROOFSTEP]
rw [prod_eq_mul_prod_diff_singleton h.choose_spec, ← mul_assoc, ← @if_pos _ _ h.choose_spec R (_ * _) 0, ←
  sum_pi_single', ← sum_add_distrib] at hμ
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
⊢ ∑ i in t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x => s a) i * ∏ j in t \ {i}, s j = 1
[PROOFSTEP]
rw [← hμ, sum_congr rfl]
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
⊢ ∀ (x : I),
    x ∈ t →
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x => s a) x * ∏ j in t \ {x}, s j =
        Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
          μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x => s a) x * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
      μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
dsimp
  -- porting note: terms were showing as sort of `HAdd.hadd` instead of `+`
        -- this whole proof pretty much breaks and has to be rewritten from scratch
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x + μ x * s a) * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
      μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_2.mp.intro.refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j in t \ {x}, s j + μ x * s a * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
      μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x
[PROOFSTEP]
by_cases hx : x = h.choose
[GOAL]
case pos
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x
[PROOFSTEP]
rw [hx, Pi.single_eq_same, Pi.single_eq_same]
[GOAL]
case neg
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j in t \ {x}, s j =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x
[PROOFSTEP]
rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * s a * ∏ j in t \ {x}, s j = μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * (s a * ∏ j in t \ {x}, s j) = μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
congr
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ s a * ∏ j in t \ {x}, s j = ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
rw [prod_eq_prod_diff_singleton_mul (mem x hx) _, mul_comm]
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ (∏ j in t \ {x}, s j) * s a = (∏ x in (insert a t \ {x}) \ {a}, s x) * s a
[PROOFSTEP]
congr 2
[GOAL]
case refine'_2.mp.intro.refine'_1.e_a.e_a.e_a.e_s
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝¹ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ✝ : μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
hμ :
  ∑ x in t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x in t \ {Exists.choose h}, s x) x +
        μ x * ∏ j in insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ t \ {x} = (insert a t \ {x}) \ {a}
[PROOFSTEP]
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
[GOAL]
case refine'_2.mp.intro.refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
have : IsCoprime (s b) (s a) := ⟨μ a * ∏ i in t \ { b }, s i, ∑ i in t, μ i * ∏ j in t \ { i }, s j, ?_⟩
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
this : IsCoprime (s b) (s a)
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
[PROOFSTEP]
exact ⟨this.symm, this⟩
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ (μ a * ∏ i in t \ {b}, s i) * s b + (∑ i in t, μ i * ∏ j in t \ {i}, s j) * s a = 1
[PROOFSTEP]
rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ ∀ (x : I), x ∈ t → (μ x * ∏ j in t \ {x}, s j) * s a = μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (μ x * ∏ j in t \ {x}, s j) * s a = μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ μ x * ((∏ j in t \ {x}, s j) * s a) = μ x * ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
congr
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (∏ j in t \ {x}, s j) * s a = ∏ j in insert a t \ {x}, s j
[PROOFSTEP]
rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (∏ j in t \ {x}, s j) * s a = (∏ x in (insert a t \ {x}) \ {a}, s x) * s a
[PROOFSTEP]
congr 2
[GOAL]
case refine'_2.mp.intro.refine'_2.refine_1.e_a.e_a.e_s
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * ∏ j in cons a t hat \ {a}, s j + ∑ x in t, μ x * ∏ j in cons a t hat \ {x}, s j = 1
hμ : μ a * ∏ j in t, s j + ∑ x in t, μ x * ∏ j in insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ t \ {x} = (insert a t \ {x}) \ {a}
[PROOFSTEP]
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
[GOAL]
case refine'_2.mpr
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
⊢ (Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)) →
    ∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
rintro ⟨hs, Hb⟩
[GOAL]
case refine'_2.mpr.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
⊢ ∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
obtain ⟨μ, hμ⟩ := ih.mpr hs
[GOAL]
case refine'_2.mpr.intro.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
⊢ ∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
⊢ ∃ μ, ∑ i in cons a t hat, μ i * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
use fun i ↦ if i = a then u else v * μ i
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
⊢ ∑ i in cons a t hat, (if i = a then u else v * μ i) * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
have hμ' : (∑ i in t, v * ((μ i * ∏ j in t \ { i }, s j) * s a)) = v * s a := by rw [← mul_sum, ← sum_mul, hμ, one_mul]
[GOAL]
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
⊢ ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
[PROOFSTEP]
rw [← mul_sum, ← sum_mul, hμ, one_mul]
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
⊢ ∑ i in cons a t hat, (if i = a then u else v * μ i) * ∏ j in cons a t hat \ {i}, s j = 1
[PROOFSTEP]
rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat, if_pos rfl, ← huv, ← hμ', sum_congr rfl]
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
⊢ ∀ (x : I),
    x ∈ t → (if x = a then u else v * μ x) * ∏ j in insert a t \ {x}, s j = v * ((μ x * ∏ j in t \ {x}, s j) * s a)
[PROOFSTEP]
intro x hx
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u else v * μ x) * ∏ j in insert a t \ {x}, s j = v * ((μ x * ∏ j in t \ {x}, s j) * s a)
[PROOFSTEP]
rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * μ x * ∏ j in insert a t \ {x}, s j = v * (μ x * ((∏ j in t \ {x}, s j) * s a))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j in insert a t \ {x}, s j) = v * (μ x * ((∏ j in t \ {x}, s j) * s a))
[PROOFSTEP]
congr
[GOAL]
case h.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ ∏ j in insert a t \ {x}, s j = (∏ j in t \ {x}, s j) * s a
[PROOFSTEP]
rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
[GOAL]
case h.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (∏ x in (insert a t \ {x}) \ {a}, s x) * s a = (∏ j in t \ {x}, s j) * s a
[PROOFSTEP]
congr 2
[GOAL]
case h.e_a.e_a.e_a.e_s
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x✝ y z : R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
h✝ : Finset.Nonempty t✝
a : I
t : Finset I
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ (x : I), x ∈ t → a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ (b : I), b ∈ t → IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1
u v : R
huv : u * ∏ i in t, s i + v * s a = 1
hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (insert a t \ {x}) \ {a} = t \ {x}
[PROOFSTEP]
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
[GOAL]
R : Type u
I : Type v
inst✝³ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ (∃ μ, ∑ i : I, μ i * ∏ j in {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)
[PROOFSTEP]
convert exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
[GOAL]
case h.e'_2.a
R : Type u
I : Type v
inst✝³ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)
[PROOFSTEP]
simp only [Function.onFun, pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]
[GOAL]
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on fun i => s ↑i) ↔ ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
[PROOFSTEP]
refine' ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
[GOAL]
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsCoprime (s i) (s j)
[PROOFSTEP]
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
[GOAL]
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)
[PROOFSTEP]
obtain ⟨hj, ji⟩ := hj
[GOAL]
case refine'_1.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsCoprime (s i) (s j)
[PROOFSTEP]
refine @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
[GOAL]
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
⊢ Pairwise (IsCoprime on fun i => s ↑i)
[PROOFSTEP]
rintro ⟨i, hi⟩ ⟨j, hj⟩ h
[GOAL]
case refine'_2.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ (IsCoprime on fun i => s ↑i) { val := i, property := hi } { val := j, property := hj }
[PROOFSTEP]
apply IsCoprime.prod_right_iff.mp (hp i hi)
[GOAL]
case refine'_2.mk.mk.a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ ↑{ val := j, property := hj } ∈ t \ {i}
[PROOFSTEP]
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h <| Subtype.ext (Finset.mem_singleton.mp f).symm⟩
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime (x ^ m) y
[PROOFSTEP]
rw [← Finset.card_range m, ← Finset.prod_const]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime (∏ _x in range m, x) y
[PROOFSTEP]
exact IsCoprime.prod_left fun _ _ ↦ H
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (y ^ n)
[PROOFSTEP]
rw [← Finset.card_range n, ← Finset.prod_const]
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x in range n, y)
[PROOFSTEP]
exact IsCoprime.prod_right fun _ _ ↦ H
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y
[PROOFSTEP]
refine' ⟨fun h ↦ _, IsCoprime.pow_left⟩
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [← Finset.card_range m, ← Finset.prod_const] at h
[GOAL]
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (∏ _x in range m, x) y
⊢ IsCoprime x y
[PROOFSTEP]
exact
  h.of_prod_left 0
    (Finset.mem_range.mpr hm)
      -- porting note: I'm not sure why `finset` didn't get corrected automatically to `Finset`
        -- by Mathport, nor whether this is an issue


[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ IsPrimitiveRoot (exp (2 * ↑π * I * (↑i / ↑n))) n
[PROOFSTEP]
rw [IsPrimitiveRoot.iff_def]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), exp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l
[PROOFSTEP]
simp only [← exp_nat_mul, exp_eq_one_iff]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
[PROOFSTEP]
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast h0
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast h0
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
[PROOFSTEP]
constructor
[GOAL]
case left
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)
[PROOFSTEP]
use i
[GOAL]
case h
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)
[PROOFSTEP]
field_simp [hn0, mul_comm (i : ℂ), mul_comm (n : ℂ)]
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
[PROOFSTEP]
simp only [hn0, mul_right_comm _ _ ↑n, mul_left_inj' two_pi_I_ne_zero, Ne.def, not_false_iff, mul_comm _ (i : ℂ), ←
  mul_assoc _ (i : ℂ), exists_imp, field_simps]
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑i * ↑l * (2 * ↑π * I) = ↑x * (2 * ↑π * I) * ↑n → n ∣ l
[PROOFSTEP]
norm_cast
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑(i * l) * (↑(2 * π) * I) = ↑x * (↑(2 * π) * I) * ↑n → n ∣ l
[PROOFSTEP]
rintro l k hk
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
⊢ n ∣ l
[PROOFSTEP]
conv_rhs at hk => rw [mul_comm, ← mul_assoc]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
| ↑k * (↑(2 * π) * I) * ↑n
[PROOFSTEP]
rw [mul_comm, ← mul_assoc]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
| ↑k * (↑(2 * π) * I) * ↑n
[PROOFSTEP]
rw [mul_comm, ← mul_assoc]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
| ↑k * (↑(2 * π) * I) * ↑n
[PROOFSTEP]
rw [mul_comm, ← mul_assoc]
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ n ∣ l
[PROOFSTEP]
have hz : 2 * ↑π * I ≠ 0 := by simp [pi_pos.ne.symm, I_ne_zero]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ 2 * ↑π * I ≠ 0
[PROOFSTEP]
simp [pi_pos.ne.symm, I_ne_zero]
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
hz : 2 * ↑π * I ≠ 0
⊢ n ∣ l
[PROOFSTEP]
field_simp [hz] at hk
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑i * ↑l = ↑n * ↑k
⊢ n ∣ l
[PROOFSTEP]
norm_cast at hk
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ l
[PROOFSTEP]
have : n ∣ i * l := by rw [← Int.coe_nat_dvd, hk, mul_comm]; apply dvd_mul_left
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ i * l
[PROOFSTEP]
rw [← Int.coe_nat_dvd, hk, mul_comm]
[GOAL]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ ↑n ∣ k * ↑n
[PROOFSTEP]
apply dvd_mul_left
[GOAL]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
this : n ∣ i * l
⊢ n ∣ l
[PROOFSTEP]
exact hi.symm.dvd_of_dvd_mul_left this
[GOAL]
n : ℕ
h0 : n ≠ 0
⊢ IsPrimitiveRoot (exp (2 * ↑π * I / ↑n)) n
[PROOFSTEP]
simpa only [Nat.cast_one, one_div] using isPrimitiveRoot_exp_of_coprime 1 n h0 n.coprime_one_left
[GOAL]
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
[PROOFSTEP]
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn
[GOAL]
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
[PROOFSTEP]
constructor
[GOAL]
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
[PROOFSTEP]
swap
[GOAL]
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
[PROOFSTEP]
rintro ⟨i, -, hi, rfl⟩
[GOAL]
case mpr.intro.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : Nat.coprime i n
⊢ IsPrimitiveRoot (exp (2 * ↑π * I * (↑i / ↑n))) n
[PROOFSTEP]
exact isPrimitiveRoot_exp_of_coprime i n hn hi
[GOAL]
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
[PROOFSTEP]
intro h
[GOAL]
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
[PROOFSTEP]
obtain ⟨i, hi, rfl⟩ := (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one (Nat.pos_of_ne_zero hn)
[GOAL]
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ ∃ i_1, i_1 < n ∧ ∃ x, exp (2 * ↑π * I * (↑i_1 / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
[PROOFSTEP]
refine' ⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, _⟩
[GOAL]
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
[PROOFSTEP]
rw [← exp_nat_mul]
[GOAL]
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (↑i * (2 * ↑π * I / ↑n))
[PROOFSTEP]
congr 1
[GOAL]
case mp.intro.intro.e_z
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)
[PROOFSTEP]
field_simp [hn0, mul_comm (i : ℂ)]
[GOAL]
n : ℕ+
x : ℂˣ
⊢ x ∈ rootsOfUnity n ℂ ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]
[GOAL]
n : ℕ+
x : ℂˣ
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast n.ne_zero
[GOAL]
n : ℕ+
x : ℂˣ
⊢ ↑↑n ≠ 0
[PROOFSTEP]
exact_mod_cast n.ne_zero
[GOAL]
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 → ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x := by
  simpa only using (isPrimitiveRoot_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos
[GOAL]
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
[PROOFSTEP]
simpa only using (isPrimitiveRoot_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos
[GOAL]
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
refine' ⟨i, hi, _⟩
[GOAL]
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
[PROOFSTEP]
rw [← H, ← exp_nat_mul]
[GOAL]
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = exp (↑i * (2 * ↑π * I / ↑↑n))
[PROOFSTEP]
congr 1
[GOAL]
case mp.intro.intro.e_z
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ 2 * ↑π * I * (↑i / ↑↑n) = ↑i * (2 * ↑π * I / ↑↑n)
[PROOFSTEP]
field_simp [hn0, mul_comm (i : ℂ)]
[GOAL]
case mpr
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ (∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x) → ↑x ^ ↑n = 1
[PROOFSTEP]
rintro ⟨i, _, H⟩
[GOAL]
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑x ^ ↑n = 1
[PROOFSTEP]
rw [← H, ← exp_nat_mul, exp_eq_one_iff]
[GOAL]
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ∃ n_1, ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑n_1 * (2 * ↑π * I)
[PROOFSTEP]
use i
[GOAL]
case h
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑↑i * (2 * ↑π * I)
[PROOFSTEP]
field_simp [hn0, mul_comm ((n : ℕ) : ℂ), mul_comm (i : ℂ)]
[GOAL]
k : ℕ
⊢ Finset.card (primitiveRoots k ℂ) = φ k
[PROOFSTEP]
by_cases h : k = 0
[GOAL]
case pos
k : ℕ
h : k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k
[PROOFSTEP]
simp [h]
[GOAL]
case neg
k : ℕ
h : ¬k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k
[PROOFSTEP]
exact (isPrimitiveRoot_exp k h).card_primitiveRoots
[GOAL]
n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ i, Complex.arg ζ = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ Int.natAbs i < n
[PROOFSTEP]
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
[GOAL]
n : ℕ
ζ : ℂ
h : ∃ i, i < n ∧ ∃ x, Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, Complex.arg ζ = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ Int.natAbs i < n
[PROOFSTEP]
obtain ⟨i, h, hin, rfl⟩ := h
[GOAL]
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
[PROOFSTEP]
rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
[GOAL]
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
        ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
[PROOFSTEP]
refine' ⟨if i * 2 ≤ n then i else i - n, _, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
[PROOFSTEP]
on_goal 2 =>
  replace hin := Nat.isCoprime_iff_coprime.mpr hin
  split_ifs
  · exact hin
  · convert hin.add_mul_left_left (-1) using 1
    rw [mul_neg_one, sub_eq_add_neg]
[GOAL]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
[PROOFSTEP]
on_goal 2 =>
  replace hin := Nat.isCoprime_iff_coprime.mpr hin
  split_ifs
  · exact hin
  · convert hin.add_mul_left_left (-1) using 1
    rw [mul_neg_one, sub_eq_add_neg]
[GOAL]
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
[PROOFSTEP]
replace hin := Nat.isCoprime_iff_coprime.mpr hin
[GOAL]
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n
[PROOFSTEP]
exact hin
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
[PROOFSTEP]
convert hin.add_mul_left_left (-1) using 1
[GOAL]
case h.e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
[PROOFSTEP]
rw [mul_neg_one, sub_eq_add_neg]
[GOAL]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
[PROOFSTEP]
on_goal 2 =>
  split_ifs with h₂
  · exact_mod_cast h
  suffices (i - n : ℤ).natAbs = n - i by
    rw [this]
    apply tsub_lt_self hn.bot_lt
    contrapose! h₂
    rw [Nat.eq_zero_of_le_zero h₂, zero_mul]
    exact zero_le _
  rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
  exact Or.inl (Int.ofNat_sub h.le).symm
[GOAL]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
[PROOFSTEP]
on_goal 2 =>
  split_ifs with h₂
  · exact_mod_cast h
  suffices (i - n : ℤ).natAbs = n - i by
    rw [this]
    apply tsub_lt_self hn.bot_lt
    contrapose! h₂
    rw [Nat.eq_zero_of_le_zero h₂, zero_mul]
    exact zero_le _
  rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
  exact Or.inl (Int.ofNat_sub h.le).symm
[GOAL]
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
[PROOFSTEP]
split_ifs with h₂
[GOAL]
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Int.natAbs ↑i < n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) < n
[PROOFSTEP]
suffices (i - n : ℤ).natAbs = n - i by
  rw [this]
  apply tsub_lt_self hn.bot_lt
  contrapose! h₂
  rw [Nat.eq_zero_of_le_zero h₂, zero_mul]
  exact zero_le _
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ Int.natAbs (↑i - ↑n) < n
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ n - i < n
[PROOFSTEP]
apply tsub_lt_self hn.bot_lt
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ 0 < i
[PROOFSTEP]
contrapose! h₂
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ i * 2 ≤ n
[PROOFSTEP]
rw [Nat.eq_zero_of_le_zero h₂, zero_mul]
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ 0 ≤ n
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) = n - i
[PROOFSTEP]
rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n - ↑i = ↑(n - i) ∨ ↑n - ↑i = -↑(n - i)
[PROOFSTEP]
exact Or.inl (Int.ofNat_sub h.le).symm
[GOAL]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
[PROOFSTEP]
split_ifs with h₂
[GOAL]
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑↑i / ↑n * (2 * Real.pi)
[PROOFSTEP]
convert Complex.arg_cos_add_sin_mul_I _
[GOAL]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
[PROOFSTEP]
rfl
[GOAL]
case pos.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑↑i / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
[PROOFSTEP]
field_simp [hn]
[GOAL]
case pos.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -Real.pi < ↑i * (2 * Real.pi) / ↑n ∧ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
[PROOFSTEP]
refine' ⟨(neg_lt_neg Real.pi_pos).trans_le _, _⟩
[GOAL]
case pos.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -0 ≤ ↑i * (2 * Real.pi) / ↑n
[PROOFSTEP]
rw [neg_zero]
[GOAL]
case pos.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑i * (2 * Real.pi) / ↑n
[PROOFSTEP]
exact
  mul_nonneg (mul_nonneg i.cast_nonneg <| by simp [Real.pi_pos.le]) (by rw [inv_nonneg]; simp only [Nat.cast_nonneg])
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ 2 * Real.pi
[PROOFSTEP]
simp [Real.pi_pos.le]
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ (↑n)⁻¹
[PROOFSTEP]
rw [inv_nonneg]
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑n
[PROOFSTEP]
simp only [Nat.cast_nonneg]
[GOAL]
case pos.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
[PROOFSTEP]
rw [← mul_rotate', mul_div_assoc]
[GOAL]
case pos.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
[PROOFSTEP]
rw [← mul_one n] at h₂
[GOAL]
case pos.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
[PROOFSTEP]
exact mul_le_of_le_one_right Real.pi_pos.le ((div_le_iff' <| by exact_mod_cast pos_of_gt h).mpr <| by exact_mod_cast h₂)
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ 0 < ↑n
[PROOFSTEP]
exact_mod_cast pos_of_gt h
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ ↑i * 2 ≤ ↑n * 1
[PROOFSTEP]
exact_mod_cast h₂
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
[PROOFSTEP]
rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
[GOAL]
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg
      (Complex.cos (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) +
        Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
[PROOFSTEP]
convert Complex.arg_cos_add_sin_mul_I _
[GOAL]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
[PROOFSTEP]
rw [← sub_one_mul, sub_div, div_self]
[GOAL]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
[PROOFSTEP]
rw [← sub_one_mul, sub_div, div_self]
[GOAL]
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case neg.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑(↑i - ↑n) / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
[PROOFSTEP]
field_simp [hn]
[GOAL]
case neg.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n ∧ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ Real.pi
[PROOFSTEP]
refine' ⟨_, le_trans _ Real.pi_pos.le⟩
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
case neg.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
[PROOFSTEP]
on_goal 2 =>
  rw [mul_div_assoc]
  exact
    mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
      (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
case neg.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
[PROOFSTEP]
on_goal 2 =>
  rw [mul_div_assoc]
  exact
    mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
      (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
[GOAL]
case neg.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
[PROOFSTEP]
rw [mul_div_assoc]
[GOAL]
case neg.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi / ↑n) ≤ 0
[PROOFSTEP]
exact
  mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
    (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i ≤ ↑n
[PROOFSTEP]
exact_mod_cast h.le
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ 2 * Real.pi
[PROOFSTEP]
simp [Real.pi_pos.le]
[GOAL]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ ↑n
[PROOFSTEP]
simp
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
[PROOFSTEP]
rw [← mul_rotate', mul_div_assoc, neg_lt, ← mul_neg, mul_lt_iff_lt_one_right Real.pi_pos, ← neg_div, ← neg_mul, neg_sub,
  div_lt_iff, one_mul, sub_mul, sub_lt_comm, ← mul_sub_one]
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n * (2 - 1) < ↑i * 2
case neg.convert_2.refine'_1 n : ℕ hn : n ≠ 0 i : ℕ h : i < n hin : Nat.coprime i n h₂ : ¬i * 2 ≤ n ⊢ 0 < ↑n
[PROOFSTEP]
norm_num
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n < ↑i * 2
case neg.convert_2.refine'_1 n : ℕ hn : n ≠ 0 i : ℕ h : i < n hin : Nat.coprime i n h₂ : ¬i * 2 ≤ n ⊢ 0 < ↑n
[PROOFSTEP]
exact_mod_cast not_le.mp h₂
[GOAL]
case neg.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
[PROOFSTEP]
exact Nat.cast_pos.mpr hn.bot_lt