awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
a₁ : m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Premises used: PrimeMultiset.prod_dvd_iff, PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
a₁ : n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
apply lcm_dvd

Premises used: PNat.lcm_dvd
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
rw [← factorMultiset_le_iff']

Premises used: PNat.factorMultiset_le_iff'
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
rw [← factorMultiset_le_iff']

Premises used: PNat.factorMultiset_le_iff'
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
apply sup_le_iff.mpr

Premises used: Iff.mpr, sup_le_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.factorMultiset ≤ (m.lcm n).factorMultiset
a₁ : n.factorMultiset ≤ (m.lcm n).factorMultiset
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m ∣ m.lcm n
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
apply factorMultiset_le_iff.mpr

Premises used: Iff.mpr, PNat.factorMultiset_le_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : n ∣ m.lcm n
⊢ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
apply factorMultiset_le_iff.mpr

Premises used: Iff.mpr, PNat.factorMultiset_le_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m ∣ m.lcm n

Tactic:
dvd_lcm_left m n

Premises used: PNat.dvd_lcm_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m ∣ m.lcm n

Tactic:
exact dvd_lcm_left m n

Premises used: PNat.dvd_lcm_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ n ∣ m.lcm n

Tactic:
dvd_lcm_right m n

Premises used: PNat.dvd_lcm_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ n ∣ m.lcm n

Tactic:
exact dvd_lcm_right m n

Premises used: PNat.dvd_lcm_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
rw : k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset
⊢ (↑p : ℕ+) ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset

Tactic:
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
    factorMultiset_ofPrime]

Premises used: PNat.factorMultiset_le_iff, PNat.factorMultiset_ofPrime, PNat.factorMultiset_pow, Multiset.le_count_iff_replicate_le
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
a : PrimeMultiset = Multiset Nat.Primes → k • PrimeMultiset.ofPrime p = Multiset.replicate k p
⊢ k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset

Tactic:
congr! 2
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p

Tactic:
apply Multiset.eq_replicate.mpr

Premises used: Iff.mpr, Multiset.eq_replicate
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : Multiset.card (k • PrimeMultiset.ofPrime p) = k
a₁ : ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : k * Multiset.card (PrimeMultiset.ofPrime p) = k
a₁ : k * 1 = k
a₂ a₃ : k = k
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k

Tactic:
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]

Premises used: Multiset.card_nsmul, mul_one, PrimeMultiset.card_ofPrime
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q ∈ Multiset.replicate k p

Tactic:
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h

Premises used: Multiset.nsmul_singleton, PrimeMultiset.ofPrime
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p

Tactic:
Multiset.eq_of_mem_replicate h

Premises used: Multiset.eq_of_mem_replicate
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p

Tactic:
exact Multiset.eq_of_mem_replicate h

Premises used: Multiset.eq_of_mem_replicate
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
change : (u ⊓ v).prod = n.gcd m
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
change (u ⊓ v).prod = PNat.gcd n m

Premises used: PNat.gcd, PrimeMultiset.prod, Min.min
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ u = n.factorMultiset

Tactic:
have : u = n.factorMultiset := u.factorMultiset_prod.symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
rw : (n.factorMultiset ⊓ v).prod = n.gcd m
⊢ (u ⊓ v).prod = n.gcd m

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ v = m.factorMultiset

Tactic:
have : v = m.factorMultiset := v.factorMultiset_prod.symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
rw : (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
rw : (n.gcd m).factorMultiset.prod = n.gcd m
rw₁ rw₂ : n.gcd m = n.gcd m
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m

Tactic:
rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]

Premises used: PNat.factorMultiset_gcd, PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
change : (u ⊔ v).prod = n.lcm m
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
change (u ⊔ v).prod = PNat.lcm n m

Premises used: PrimeMultiset.prod, PNat.lcm, Max.max
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
rw : (n.factorMultiset ⊔ v).prod = n.lcm m
⊢ (u ⊔ v).prod = n.lcm m

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
rw : (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
rw : (n.lcm m).factorMultiset.prod = n.lcm m
rw₁ rw₂ : n.lcm m = n.lcm m
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m

Tactic:
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]

Premises used: PNat.factorMultiset_lcm, PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
n' : ℕ
simp_rw :
  (∃ (a : ℕ), ∃ (h : 0 < a), ∃ (x : n' = a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a ⋯)) ↔
    ∃ (h : 0 < n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n' h)
simp_rw₁ :
  (∃ (a : ℕ), ∃ (b : n' = a), ∃ (a_1 : 0 < a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a ⋯)) ↔
    ∃ (h : 0 < n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n' h)
simp_rw₂ :
  (∃ (a : ℕ), n' = a ∧ ∃ (a_1 : 0 < a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a ⋯)) ↔
    ∃ (h : 0 < n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n' h)
⊢ (∃ (a : ℕ),
      ∃ (b : 0 < a),
        ∃ (x : n' = (↑(Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a b) : ℕ)),
          p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a b)) ↔
    ∃ (h : 0 < n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n' h)

Tactic:
simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']

Premises used: exists_eq_left', exists_prop, exists_comm, PNat.mk_coe
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
⊢ ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n

Tactic:
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
have :
  (n :
      { n : ℕ //
        (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }) →
    { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
have n := Nat.findX this
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
refine_1 : 0 < (↑n : ℕ)
refine_2 : p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯)
refine_3 : ∀ (m : ℕ+) (hm : m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯) (pm : p m), False
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
refine_1 : ∀ (n' : ℕ+) (hn' : (↑n : ℕ) = (↑n' : ℕ)), 0 < (↑n : ℕ)
⊢ 0 < (↑n : ℕ)

Tactic:
obtain ⟨n', hn', -⟩ := n.prop.1

Premises used: And.left, Subtype.prop
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
n' : ℕ+
hn' : (↑n : ℕ) = (↑n' : ℕ)
refine_1 : 0 < (↑n' : ℕ)
⊢ 0 < (↑n : ℕ)

Tactic:
rw [hn']
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
n' : ℕ+
hn' : (↑n : ℕ) = (↑n' : ℕ)
⊢ 0 < (↑n' : ℕ)

Tactic:
n'.prop

Premises used: PNat.val, Subtype.prop
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
n' : ℕ+
hn' : (↑n : ℕ) = (↑n' : ℕ)
⊢ 0 < (↑n' : ℕ)

Tactic:
exact n'.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
refine_2 : ∀ (n' : ℕ+) (hn' : (↑n : ℕ) = (↑n' : ℕ)) (pn' : p n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯)

Tactic:
obtain ⟨n', hn', pn'⟩ := n.prop.1

Premises used: And.left, Subtype.prop
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
n' : ℕ+
hn' : (↑n : ℕ) = (↑n' : ℕ)
pn' : p n'
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯)

Tactic:
simpa [hn', Subtype.coe_eta] using pn'

Premises used: Subtype.coe_eta
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
m : ℕ+
hm : m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯
pm : p m
⊢ False

Tactic:
n.prop.2 m hm ⟨m, rfl, pm⟩

Premises used: PNat.val, And.right, Subtype.prop, Exists.intro, rfl
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
n :
  { n : ℕ // (∃ (n_1 : ℕ+), ∃ (x : n = (↑n_1 : ℕ)), p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ (n : ℕ+), ∃ (x : m = (↑n : ℕ)), p n }
m : ℕ+
hm : m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯
pm : p m
⊢ False

Tactic:
exact n.prop.2 m hm ⟨m, rfl, pm⟩

Premises used: PNat.val, And.right, Subtype.prop, Exists.intro, rfl
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ p (PNat.find (p := p) h)

Tactic:
(PNat.findX h).prop.left

Premises used: And.left, Subtype.prop, PNat.findX, PNat.find
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ ∀ {m : ℕ+}, m < PNat.find (p := p) h → ¬p m

Tactic:
@(PNat.findX h).prop.right

Premises used: And.right, Subtype.prop, PNat.findX, PNat.find
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
m : ℕ+
hm : p m
⊢ PNat.find (p := p) h ≤ m

Tactic:
le_of_not_gt fun l => PNat.find_min h l hm

Premises used: le_of_not_gt, PNat.find_min
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
m : ℕ+
mp : PNat.find (p := p) h = m → p m ∧ ∀ (n : ℕ+), n < m → ¬p n
mpr : (p m ∧ ∀ (n : ℕ+), n < m → ¬p n) → PNat.find (p := p) h = m
⊢ PNat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ p (PNat.find (p := p) h) ∧ ∀ (n : ℕ+), n < PNat.find (p := p) h → ¬p n

Tactic:
⟨PNat.find_spec h, fun _ => PNat.find_min h⟩

Premises used: PNat.find_spec, PNat.find_min, And.intro
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ p (PNat.find (p := p) h) ∧ ∀ (n : ℕ+), n < PNat.find (p := p) h → ¬p n

Tactic:
exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
m : ℕ+
hm : p m
hlt : ∀ (n : ℕ+), n < m → ¬p n
⊢ PNat.find (p := p) h = m

Tactic:
le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)

Premises used: PNat.find_spec, le_antisymm, imp_not_comm, not_lt, PNat.find_min', Iff.mp
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
m : ℕ+
hm : p m
hlt : ∀ (n : ℕ+), n < m → ¬p n
⊢ PNat.find (p := p) h = m

Tactic:
exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)

Premises used: PNat.find_spec, le_antisymm, imp_not_comm, not_lt, PNat.find_min', Iff.mp
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
n : ℕ+
⊢ PNat.find (p := p) h < n ↔ ∃ (m : ℕ+), m < n ∧ p m

Tactic:
⟨fun h2 => ⟨PNat.find h, h2, PNat.find_spec h⟩, fun ⟨_, hmn, hm⟩ =>
    (PNat.find_min' h hm).trans_lt hmn⟩

Premises used: PNat.find_spec, _private.0.PNat.find_lt_iff.match_1, And.intro, LT.lt, Iff.intro, Exists.intro, PNat.find_min', LE.le.trans_lt, PNat.find
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
n : ℕ+
⊢ PNat.find (p := p) h ≤ n ↔ ∃ (m : ℕ+), m ≤ n ∧ p m

Tactic:
simp only [← lt_add_one_iff, find_lt_iff]

Premises used: PNat.find_lt_iff, PNat.lt_add_one_iff
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
n : ℕ+
⊢ n ≤ PNat.find (p := p) h ↔ ∀ (m : ℕ+), m < n → ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

Premises used: not_exists, PNat.find_lt_iff, not_lt, not_and
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
n : ℕ+
⊢ n < PNat.find (p := p) h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m

Tactic:
simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]

Premises used: PNat.add_one_le_iff, add_le_add_iff_right, PNat.le_find_iff
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ PNat.find (p := p) h = 1 ↔ p 1

Tactic:
simp [find_eq_iff]

Premises used: PNat.find_eq_iff
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
⊢ 1 < PNat.find (p := p) h ↔ ¬p 1

Tactic:
simp
-- Module: Mathlib.Data.PNat.Find
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (n : ℕ+), q n → p n
hp : ∃ (n : ℕ+), p n
hq : ∃ (n : ℕ+), q n
⊢ PNat.find (p := p) hp ≤ PNat.find (p := q) hq

Tactic:
PNat.find_min' _ (h _ (PNat.find_spec hq))

Premises used: PNat.find_spec, PNat.find_min'
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
n : ℕ+
h : ∃ (n : ℕ+), p n
hn : p n
⊢ PNat.find (p := p) h ≤ n

Tactic:
(PNat.find_le_iff _ _).2 ⟨n, le_rfl, hn⟩

Premises used: Iff.mpr, le_rfl, PNat.find_le_iff, And.intro, Exists.intro
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
⊢ PNat.find (p := p) h = PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1

Tactic:
(find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩

Premises used: Iff.mpr, PNat.find_spec, And.intro, PNat.find_eq_iff
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
refine : ∀ (n : ℕ+), n < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p n
⊢ PNat.find (p := p) h = PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩

Premises used: Iff.mpr, PNat.find_spec, And.intro, PNat.find_eq_iff
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
⊢ 1 < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p 1

Tactic:
simp [h1]
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
m : ℕ+
h_1 : m < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p m
hm : m + 1 < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1
⊢ ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)

Tactic:
simp only [add_lt_add_iff_right, lt_find_iff] at hm

Premises used: PNat.lt_find_iff, add_lt_add_iff_right
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
m : ℕ+
h_1 : m < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)

Tactic:
hm _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
m : ℕ+
h_1 : m < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)

Tactic:
exact hm _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.PNat.Find
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
n : ℕ+
one : 1 < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p 1
succ :
  ∀ (m : ℕ+),
    (m < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p m) →
      m + 1 < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p (m + 1)
⊢ n < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p n

Tactic:
induction n with
  | one => simp [h1]
  | succ m _ =>
    intro hm
    simp only [add_lt_add_iff_right, lt_find_iff] at hm
    exact hm _ le_rfl

Premises used: PNat.lt_find_iff, add_lt_add_iff_right
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ Icc a b = Finset.subtype (fun (n : ℕ) ↦ 0 < n) (Icc (↑a : ℕ) (↑b : ℕ))

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, Finset.map, Finset.Icc, Finset.subtype, rfl
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ Ico a b = Finset.subtype (fun (n : ℕ) ↦ 0 < n) (Ico (↑a : ℕ) (↑b : ℕ))

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, Finset.map, Finset.Ico, Finset.subtype, rfl
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ Ioc a b = Finset.subtype (fun (n : ℕ) ↦ 0 < n) (Ioc (↑a : ℕ) (↑b : ℕ))

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, Finset.map, Finset.subtype, rfl, Finset.Ioc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ Ioo a b = Finset.subtype (fun (n : ℕ) ↦ 0 < n) (Ioo (↑a : ℕ) (↑b : ℕ))

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, Finset.map, Finset.subtype, Finset.Ioo, rfl
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ uIcc a b = Finset.subtype (fun (n : ℕ) ↦ 0 < n) (uIcc (↑a : ℕ) (↑b : ℕ))

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, Finset.map, Finset.Icc, Finset.subtype, rfl, Finset.uIcc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Icc a b) = Icc (↑a : ℕ) (↑b : ℕ)

Tactic:
Finset.map_subtype_embedding_Icc _ _ _ fun _c _ _x hx _ hc _ => hc.trans_le hx

Premises used: PNat.val, LT.lt.trans_le, Finset.map_subtype_embedding_Icc, PNat
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ico a b) = Ico (↑a : ℕ) (↑b : ℕ)

Tactic:
Finset.map_subtype_embedding_Ico _ _ _ fun _c _ _x hx _ hc _ => hc.trans_le hx

Premises used: PNat.val, LT.lt.trans_le, Finset.map_subtype_embedding_Ico, PNat