awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ (↑p : ℕ+) ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset
have rw : k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset
Tactic: rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
    factorMultiset_ofPrime]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset
have a : PrimeMultiset = Multiset Nat.Primes → k • PrimeMultiset.ofPrime p = Multiset.replicate k p
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p
have a : Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
Tactic: apply Multiset.eq_replicate.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
have a : Multiset.card (k • PrimeMultiset.ofPrime p) = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : Multiset.card (k • PrimeMultiset.ofPrime p) = k
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
have a₁ : ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k
have a : k * Multiset.card (PrimeMultiset.ofPrime p) = k
Tactic: rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : k * Multiset.card (PrimeMultiset.ofPrime p) = k
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k
have a₁ : k * 1 = k
Tactic: rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
a : k * Multiset.card (PrimeMultiset.ofPrime p) = k
a₁ : k * 1 = k
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k
have a₂ : k = k
Tactic: rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
m : ℕ+
p : Nat.Primes
k : ℕ
e_1 : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
have h₁ : q ∈ Multiset.replicate k p
Tactic: rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = n.gcd m
have this : u = n.factorMultiset
Tactic: have : u = n.factorMultiset := u.factorMultiset_prod.symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊓ v).prod = n.gcd m
have rw : (n.factorMultiset ⊓ v).prod = n.gcd m
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m
have this₁ : v = m.factorMultiset
Tactic: have : v = m.factorMultiset := v.factorMultiset_prod.symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m
have rw : (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m
have rw : (n.gcd m).factorMultiset.prod = n.gcd m
Tactic: rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m
have rw₁ : n.gcd m = n.gcd m
Tactic: rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = n.lcm m
have this : u = n.factorMultiset
Tactic: have : u = n.factorMultiset := u.factorMultiset_prod.symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊔ v).prod = n.lcm m
have rw : (n.factorMultiset ⊔ v).prod = n.lcm m
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m
have this₁ : v = m.factorMultiset
Tactic: have : v = m.factorMultiset := v.factorMultiset_prod.symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m
have rw : (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this_1 : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
have rw : (n.lcm m).factorMultiset.prod = n.lcm m
Tactic: rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
have rw₁ : n.lcm m = n.lcm m
Tactic: rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
n' : ℕ
⊢ (∃ (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)
have simp_rw : (∃ (a : ℕ), ∃ (h : 0 < a), ∃ (x : n' = a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a sorry)) ↔
  ∃ (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']
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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)
⊢ (∃ (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)
have simp_rw₁ : (∃ (a : ℕ), ∃ (b : n' = a), ∃ (a_1 : 0 < a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a sorry)) ↔
  ∃ (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']
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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)
⊢ (∃ (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)
have simp_rw₂ : (∃ (a : ℕ), n' = a ∧ ∃ (a_1 : 0 < a), p (Subtype.mk (p := fun (a : ℕ) ↦ 0 < a) a sorry)) ↔
  ∃ (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']
-- Lean 4 proof step from Mathlib.Data.PNat.Find (hypothesis)
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
have this : ∃ (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⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
Goal:
p q : ℕ+ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∃ (n : ℕ+), p n
this : ∃ (n' : ℕ), ∃ (n : ℕ+), ∃ (x : n' = (↑n : ℕ)), p n
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
have 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 }
Tactic: have n := Nat.findX this
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
have refine_1 : 0 < (↑n : ℕ)
Tactic: refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 : ℕ)
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
have refine_2 : p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) sorry)
Tactic: refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 : ℕ) ⋯)
⊢ { n : ℕ+ // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
have refine_3 : ∀ (m : ℕ+) (hm : m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) sorry) (pm : p m), False
Tactic: refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 }
⊢ 0 < (↑n : ℕ)
have refine_1 : ∀ (n' : ℕ+) (hn' : (↑n : ℕ) = (↑n' : ℕ)), 0 < (↑n : ℕ)
Tactic: obtain ⟨n', hn', -⟩ := n.prop.1
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 : ℕ)
have refine_1 : 0 < (↑n' : ℕ)
Tactic: rw [hn']
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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 }
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) ⋯)
have refine_2 : ∀ (n' : ℕ+) (hn' : (↑n : ℕ) = (↑n' : ℕ)) (pn' : p n'), p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑n : ℕ) sorry)
Tactic: obtain ⟨n', hn', pn'⟩ := n.prop.1
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
m : ℕ+
⊢ PNat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n
have mp : PNat.find (p := p) h = m → p m ∧ ∀ (n : ℕ+), n < m → ¬p n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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
⊢ PNat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n
have mpr : (p m ∧ ∀ (n : ℕ+), n < m → ¬p n) → PNat.find (p := p) h = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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
have refine : ∀ (n : ℕ+), n < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p n
Tactic: refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Find (hypothesis)
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
⊢ ¬p (m + 1)
have hm₁ : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
Tactic: simp only [add_lt_add_iff_right, lt_find_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
Goal:
p : ℕ+ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ+), p n
h₂ : ∃ (n : ℕ+), p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ n < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p n
have one : 1 < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p 1
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PNat.Find (goal)
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
⊢ n < PNat.find (p := fun (n : ℕ+) ↦ p (n + 1)) h₂ + 1 → ¬p n
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw₁ : #(Icc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Icc a b))
Tactic: rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Icc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Icc a b))
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw₂ : #(Icc a b) = #(Icc a b)
Tactic: rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ico a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ico a b))
Tactic: rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ico a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ico a b))
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₂ : #(Ico a b) = #(Ico a b)
Tactic: rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Ioc, ← map_subtype_embedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ioc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ioc a b))
Tactic: rw [← Nat.card_Ioc, ← map_subtype_embedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ioc a b))
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₂ : #(Ioc a b) = #(Ioc a b)
Tactic: rw [← Nat.card_Ioc, ← map_subtype_embedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw₁ : #(uIcc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (uIcc a b))
Tactic: rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(uIcc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (uIcc a b))
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw₂ : #(uIcc a b) = #(uIcc a b)
Tactic: rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ Fintype.card (↑(Set.Icc a b) : Type) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw : Fintype.card (↑(Set.Icc a b) : Type) = #(Icc a b)
Tactic: rw [← card_Icc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Icc a b) : Type) = #(Icc a b)
⊢ Fintype.card (↑(Set.Icc a b) : Type) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw₁ : #(Icc a b) = #(Icc a b)
Tactic: rw [← card_Icc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ Fintype.card (↑(Set.Ico a b) : Type) = (↑b : ℕ) - (↑a : ℕ)
have rw : Fintype.card (↑(Set.Ico a b) : Type) = #(Ico a b)
Tactic: rw [← card_Ico, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ico a b) : Type) = #(Ico a b)
⊢ Fintype.card (↑(Set.Ico a b) : Type) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ico a b) = #(Ico a b)
Tactic: rw [← card_Ico, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ Fintype.card (↑(Set.Ioc a b) : Type) = (↑b : ℕ) - (↑a : ℕ)
have rw : Fintype.card (↑(Set.Ioc a b) : Type) = #(Ioc a b)
Tactic: rw [← card_Ioc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ioc a b) : Type) = #(Ioc a b)
⊢ Fintype.card (↑(Set.Ioc a b) : Type) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ioc a b) = #(Ioc a b)
Tactic: rw [← card_Ioc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ Fintype.card (↑(Set.Ioo a b) : Type) = (↑b : ℕ) - (↑a : ℕ) - 1
have rw : Fintype.card (↑(Set.Ioo a b) : Type) = #(Ioo a b)
Tactic: rw [← card_Ioo, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ioo a b) : Type) = #(Ioo a b)
⊢ Fintype.card (↑(Set.Ioo a b) : Type) = (↑b : ℕ) - (↑a : ℕ) - 1
have rw₁ : #(Ioo a b) = #(Ioo a b)
Tactic: rw [← card_Ioo, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
⊢ Fintype.card (↑(Set.uIcc a b) : Type) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw : Fintype.card (↑(Set.uIcc a b) : Type) = #(uIcc a b)
Tactic: rw [← card_uIcc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Interval (goal)
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.uIcc a b) : Type) = #(uIcc a b)
⊢ Fintype.card (↑(Set.uIcc a b) : Type) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw₁ : #(uIcc a b) = #(uIcc a b)
Tactic: rw [← card_uIcc, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (hypothesis)
Goal:
n m : ℕ+
h : 0 < (↑n : ℕ) * (↑m : ℕ) := ⋯
⊢ 0 < (↑n : ℕ).lcm (↑m : ℕ)
have h₁ : 0 < (↑n : ℕ).lcm (↑m : ℕ) * (↑n : ℕ).gcd (↑m : ℕ)
Tactic: rw [← gcd_mul_lcm (n : ℕ) (m : ℕ), mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
⊢ n < HAdd.hAdd (α := ℕ+) 1 1 → n = 1
have rw : n = 1 → n = 1
Tactic: rw [lt_add_one_iff, le_one_iff_eq_one]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
p m : ℕ+
pp : p.Prime
⊢ m ∣ p ↔ m = 1 ∨ m = p
have rw : (↑m : ℕ) ∣ (↑p : ℕ) ↔ m = 1 ∨ m = p
Tactic: rw [PNat.dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
p m : ℕ+
pp : p.Prime
⊢ (↑m : ℕ) ∣ (↑p : ℕ) ↔ m = 1 ∨ m = p
have rw : (↑m : ℕ) = 1 ∨ (↑m : ℕ) = (↑p : ℕ) ↔ m = 1 ∨ m = p
Tactic: rw [Nat.dvd_prime pp]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False
have apply : (↑p : ℕ) = 1
Tactic: apply Nat.Prime.ne_one pp
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
p : ℕ+
pp : p.Prime
⊢ ¬p ∣ 1
have rw : ¬(↑p : ℕ) ∣ (↑1 : ℕ)
Tactic: rw [dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
hn : n ≠ 1
⊢ ∃ (p : ℕ+), p.Prime ∧ p ∣ n
have obtain : ∀ (p : ℕ) (hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)), ∃ (p : ℕ+), p.Prime ∧ p ∣ n
Tactic: obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)
⊢ ∃ (p : ℕ+), p.Prime ∧ p ∣ n
have exists : Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p sorry) ∧ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p sorry ∣ n
Tactic: exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)
⊢ Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) ∧ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯ ∣ n
have rw : Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p sorry) ∧ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p sorry) : ℕ) ∣ (↑n : ℕ)
Tactic: rw [dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n : ℕ+
⊢ (↑m : ℕ).gcd (↑n : ℕ) = 1 ↔ m.gcd n = 1
have rw : (↑m : ℕ).gcd (↑n : ℕ) = 1 ↔ (↑(m.gcd n) : ℕ) = (↑1 : ℕ)
Tactic: rw [← coe_inj]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ m.Coprime k → n.Coprime k → (m * n).Coprime k
have rw : (↑m : ℕ).Coprime (↑k : ℕ) → n.Coprime k → (m * n).Coprime k
Tactic: rw [← coprime_coe]