awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
t u : Fin (s + 1)
h : t < u
⊢ t < u

Tactic:
exact h
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
⊢ r ≤ n

Tactic:
have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this_1 : r ≤ n
this :
  LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1) :
      (↑(Set.Iic m) : Type u_1))
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs' : { x : Associates M // x ∈ Set.Iic m })
obtain :
  ∀ (i : Fin (s + 1))
    (hi :
      (↑((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
              (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1)) :
          Associates M) =
        c₁ i),
    ∃ (i : Fin (s + 1)), r = c₂ i
⊢ ∃ (i : Fin (s + 1)), r = c₂ i

Tactic:
obtain ⟨i, hi⟩ := hc₁''.1 this

Premises used: Iff.mp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this_1 : r ≤ n
this :
  LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1) :
      (↑(Set.Iic m) : Type u_1))
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs' : { x : Associates M // x ∈ Set.Iic m })
i : Fin (s + 1)
hi :
  (↑((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
          (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1)) :
      Associates M) =
    c₁ i
h : r = c₂ i
⊢ ∃ (i : Fin (s + 1)), r = c₂ i

Tactic:
use i
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this_1 : r ≤ n
this :
  LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1) :
      (↑(Set.Iic m) : Type u_1))
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs' : { x : Associates M // x ∈ Set.Iic m })
i : Fin (s + 1)
hi :
  (↑((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
          (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this_1)) :
      Associates M) =
    c₁ i
⊢ r = c₂ i

Tactic:
simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]

Premises used: Subtype.coe_mk, OrderIso.apply_symm_apply, Subtype.coe_eta
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this : r ≤ n
neg :
  LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this) :
      (↑(Set.Iic m) : Type u_1))
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs' : { x : Associates M // x ∈ Set.Iic m })
⊢ ∃ (i : Fin (s + 1)), r = c₂ i

Tactic:
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]
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this : r ≤ n
rw :
  ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
      ((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
        (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
    (↑(Set.Iic m) : Type u_1))
| Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs'

Tactic:
rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]

Premises used: Subtype.mk, HPow.hPow, OrderIso.symm_apply_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this : r ≤ n
neg :
  LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this) :
      (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        ((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      (↑(Set.Iic m) : Type u_1))
⊢ LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this) :
      (↑(Set.Iic m) : Type u_1))
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs' : { x : Associates M // x ∈ Set.Iic m })

Tactic:
conv_rhs => rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]

Premises used: Subtype.mk, HPow.hPow, OrderIso.symm_apply_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this : r ≤ n
neg :
  LE.le (α := (↑(Set.Iic n) : Type u_2)) (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this)
    ((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
      (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs'))
⊢ LE.le.{u_1} (α := (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this) :
      (↑(Set.Iic m) : Type u_1))
    ((d.symm : (a : (↑(Set.Iic n) : Type u_2)) → (↑(Set.Iic m) : Type u_1))
        ((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      (↑(Set.Iic m) : Type u_1))

Tactic:
rw [d.symm.le_iff_le]

Premises used: OrderIso.le_iff_le, OrderIso.symm
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
hr :
  r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
this : r ≤ n
⊢ LE.le (α := (↑(Set.Iic n) : Type u_2)) (Subtype.mk (p := fun (x : Associates N) ↦ x ∈ Set.Iic n) r this)
    ((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
      (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs'))

Tactic:
simpa only [← Subtype.coe_le_coe, Subtype.coe_mk] using hr

Premises used: Subtype.coe_mk, Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
neg :
  LE.le (α := (↑(Set.Iic m) : Type u_1)) (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ i) ⋯)
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')
⊢ r ≤
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)

Tactic:
rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]

Premises used: Subtype.coe_le_coe, OrderIso.le_iff_le
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ LE.le (α := (↑(Set.Iic m) : Type u_1)) (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ i) ⋯)
    (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')

Tactic:
simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩

Premises used: Iff.mpr, Exists.intro, Subtype.mk_le_mk, rfl
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
⊢ Ne.{u_2 + 1} (α := Associates N)
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
    0

Tactic:
ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))

Premises used: Subtype.mk, HPow.hPow, Subtype.prop, ne_zero_of_dvd_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
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 : Fin (s + 1)), r = c₁ i
c₂ : Fin (s + 1) → Associates N :=
  fun (t : Fin (s + 1)) ↦
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
      Associates N)
c₂_def :
  ∀ (t : Fin (s + 1)),
    c₂ t =
      (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ t) ⋯)) :
        Associates N)
⊢ Ne.{u_2 + 1} (α := Associates N)
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) (c₁ 1 ^ s) hs')) :
      Associates N)
    0

Tactic:
exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))

Premises used: Subtype.mk, HPow.hPow, Subtype.prop, ne_zero_of_dvd_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : UniqueFactorizationMonoid N
inst_4 : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : OrderIso.{u_1, u_2} (↑(Set.Iic m) : Type u_1) (↑(Set.Iic n) : Type u_2)
rw :
  Irreducible.{u_2} (M := Associates N)
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) p ⋯)) :
      Associates N)
⊢ Prime.{u_2} (M := Associates N)
    (↑((d : (a : (↑(Set.Iic m) : Type u_1)) → (↑(Set.Iic n) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦ x ∈ Set.Iic m) p ⋯)) :
      Associates N)

Tactic:
rw [← irreducible_iff_prime]

Premises used: irreducible_iff_prime