case pos
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n

case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
by_cases hs : s = 0
case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
suffices (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s =
    (d ⟨p ^ s, hs'⟩) by
  rw [this]
  apply Subtype.prop (d ⟨p ^ s, hs'⟩)
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
obtain ⟨c₁, rfl, hc₁', hc₁''⟩ := exists_chain_of_prime_pow hs (prime_of_normalized_factor p hp)
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
let c₂ : Fin (s + 1) → Associates N := fun t => d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
have c₂_def : ∀ t, c₂ t = d ⟨c₁ t, _⟩ := fun t => rfl
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ c₂ 1 ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
rw [← c₂_def]
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ c₂ t < c₂ u

case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
⊢ ∃ i, r = c₂ i

case neg.intro.intro.intro.refine'_3
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
⊢ (∃ i, r = c₂ i) → r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })

case neg.intro.intro.intro.refine'_4
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1 ^ s, property := hs' }) ≠ 0
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ c₂ 1 ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
refine'
  (eq_pow_second_of_chain_of_has_chain hs (fun t u h => _) (@fun r => ⟨@fun hr => _, _⟩) _).symm
no goals
case neg.intro.intro.intro.refine'_4
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1 ^ s, property := hs' }) ≠ 0
exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))
no goals
case pos
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
simp [hs]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
⊢ ↑(↑d { val := p ^ s, property := hs' }) ≤ n
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
rw [this]
no goals
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
⊢ ↑(↑d { val := p ^ s, property := hs' }) ≤ n
apply Subtype.prop (d ⟨p ^ s, hs'⟩)
no goals
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
t : Fin (s + 1)
⊢ c₁ t = c₁ t
simp
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ t < u
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ c₂ t < c₂ u
rw [c₂_def, c₂_def, Subtype.coe_lt_coe, d.lt_iff_lt, Subtype.mk_lt_mk, hc₁'.lt_iff_lt]
no goals
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ t < u
exact h
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ∃ i, r = c₂ i
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
⊢ ∃ i, r = c₂ i
have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ { val := c₁ 1 ^ s, property := hs' }
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ∃ i, r = c₂ i
suffices d.symm ⟨r, this⟩ ≤ ⟨c₁ 1 ^ s, hs'⟩ by
  obtain ⟨i, hi⟩ := hc₁''.1 this
  use i
  simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ ↑(OrderIso.symm d) (↑d { val := c₁ 1 ^ s, property := hs' })
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ { val := c₁ 1 ^ s, property := hs' }
conv_rhs => rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ { val := r, property := this } ≤ ↑d { val := c₁ 1 ^ s, property := hs' }
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ ↑(OrderIso.symm d) (↑d { val := c₁ 1 ^ s, property := hs' })
rw [d.symm.le_iff_le]
no goals
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ { val := r, property := this } ≤ ↑d { val := c₁ 1 ^ s, property := hs' }
simpa only [← Subtype.coe_le_coe, Subtype.coe_mk] using hr
case intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ ∃ i, r = c₂ i
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
⊢ ∃ i, r = c₂ i
obtain ⟨i, hi⟩ := hc₁''.1 this
case intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ r = c₂ i
case intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ ∃ i, r = c₂ i
use i
no goals
case intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ r = c₂ i
simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
case neg.intro.intro.intro.refine'_3
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
⊢ (∃ i, r = c₂ i) → r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
rintro ⟨i, hr⟩
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ { val := c₁ i, property := (_ : c₁ i ≤ m) } ≤ { val := c₁ 1 ^ s, property := hs' }
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]
no goals
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ { val := c₁ i, property := (_ : c₁ i ≤ m) } ≤ { val := c₁ 1 ^ s, property := hs' }
simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩