awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
h₁ : b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
nth_rw 1 [← Nat.prod_primeFactorsList ha]

Premises used: Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
h₁ : b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
h₂ : b = b.primeFactorsList.prod
h₃ h₄ : b = b
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']

Premises used: List.prod_append, List.Perm.prod_eq, LT.lt.ne', List.subperm_append_diff_self_of_count_le, Iff.mp, Nat.prod_primeFactorsList, List.subperm_ext_iff
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
b : ℕ
hb : b ≠ 0
⊢ replicate 0 a <+~ b.primeFactorsList ↔ HPow.hPow (β := ℕ) a 0 ∣ b

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
succ : replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b
succ₁ : a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList
⊢ replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
succ : (∃ (l : List ℕ), l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

Tactic:
rw [List.subperm_iff]

Premises used: List.subperm_iff
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
succ : (replicate (n + 1) a).prod ∣ u.prod
⊢ a ^ (n + 1) ∣ b

Tactic:
rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]

Premises used: List.Perm.prod_eq, List.prod_replicate, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod

Tactic:
hu2.prod_dvd_prod

Premises used: List.Sublist.prod_dvd_prod
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod

Tactic:
exact hu2.prod_dvd_prod

Premises used: List.Sublist.prod_dvd_prod
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : a ^ (n + 1) * c ≠ 0
⊢ ¬a = 0 ∧ ¬a ^ n * c = 0

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb

Premises used: Nat.pow_succ', mul_assoc, Ne, not_or, Nat.mul_eq_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
succ : a ^ n ∣ a ^ n * c
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]

Premises used: Nat.pow_succ', mul_assoc, Nat.primeFactorsList_prime, List.replicate_succ, List.singleton_append, And.right, And.left, Nat.perm_primeFactorsList_mul, List.subperm_cons, List.Perm.subperm_left
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b n : ℕ
ha : Prime a
hb : b ≠ 0
zero : ∀ {b : ℕ} (hb : b ≠ 0), replicate 0 a <+~ b.primeFactorsList ↔ HPow.hPow (β := ℕ) a 0 ∣ b
succ :
  ∀ (n : ℕ) (ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b) {b : ℕ} (hb : b ≠ 0),
    replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b
⊢ replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b

Tactic:
induction n generalizing b with
  | zero => simp
  | succ n ih =>
    constructor
    · rw [List.subperm_iff]
      rintro ⟨u, hu1, hu2⟩
      rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
      exact hu2.prod_dvd_prod
    · rintro ⟨c, rfl⟩
      rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
      rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]
      exact dvd_mul_right _ _

Premises used: Nat.pow_succ', mul_assoc, Nat.primeFactorsList_prime, Ne, List.subperm_iff, not_or, List.replicate_succ, List.singleton_append, List.subperm_cons, Nat.zero, dvd_mul_right, Nat.succ, List.prod_replicate, Nat.mul_eq_zero, Nat.prod_primeFactorsList, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
rw : Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
    ← and_or_left]

Premises used: and_or_left, Nat.mem_primeFactorsList, mul_ne_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)

Tactic:
simpa only [and_congr_right_iff] using Prime.dvd_mul

Premises used: and_congr_right_iff, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
apply : Prime 1
⊢ False

Tactic:
apply not_prime_one

Premises used: Nat.not_prime_one
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
rw : Prime q
⊢ Prime 1

Tactic:
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
    (dvd_of_mem_primeFactorsList hqb)]

Premises used: Nat.eq_one_of_dvd_coprimes, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Tactic:
prime_of_mem_primeFactorsList hqa

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Tactic:
exact prime_of_mem_primeFactorsList hqa

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
inl : ∀ (hab : Coprime 0 b), p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList
inr : ∀ (ha : a > 0), p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

Premises used: Nat.coprime_zero_left, Iff.mp
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
inr : ∀ (hab : a.Coprime 0), p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0
inr₁ : ∀ (hb : b > 0), p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0

Tactic:
simp [(coprime_zero_right _).mp hab]

Premises used: Nat.coprime_zero_right, Iff.mp
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
inr : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
inr₁ inr₂ : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

Premises used: List.mem_union_iff, LT.lt.ne', Nat.mem_primeFactorsList_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
inl : ∀ (hpa : p ∈ primeFactorsList 0), p ∈ (0 * b).primeFactorsList
inr : ∀ (ha : a ≠ 0), p ∈ (a * b).primeFactorsList
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

Tactic:
simp at hpa
-- Module: Mathlib.Data.Nat.Factors
Goal:
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
apply (mem_primeFactorsList_mul ha hb).2 (Or.inl hpa)

Premises used: Iff.mpr, Or.inl, Nat.mem_primeFactorsList_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
rw : p ∈ (b * a).primeFactorsList
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Factors
Goal:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Tactic:
mem_primeFactorsList_mul_left hpb ha

Premises used: Nat.mem_primeFactorsList_mul_left
-- Module: Mathlib.Data.Nat.Factors
Goal:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Tactic:
exact mem_primeFactorsList_mul_left hpb ha

Premises used: Nat.mem_primeFactorsList_mul_left
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ (∃ (k : ℕ), n = HPow.hPow (α := ℕ) 2 k) ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p

Tactic:
(eq_or_ne n 0).elim (fun hn => Or.inr ⟨3, prime_three, hn.symm ▸ dvd_zero 3, ⟨1, rfl⟩⟩) fun hn =>
    or_iff_not_imp_right.mpr fun H =>
      ⟨n.primeFactorsList.length,
        eq_prime_pow_of_unique_prime_dvd hn fun {_} hprime hdvd =>
          hprime.eq_two_or_odd'.resolve_right fun hodd => H ⟨_, hprime, hdvd, hodd⟩⟩

Premises used: Iff.mpr, dvd_zero, Classical.or_iff_not_imp_right, Eq.rec, Nat.prime_three, Nat.Prime.eq_two_or_odd', And.intro, Exists.intro, eq_or_ne, Or.resolve_right, Nat.eq_prime_pow_of_unique_prime_dvd, Or.elim, OfNat.ofNat, Eq.symm, List.length, Or.inr, rfl, Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
n2 : 2 < n
inl :
  ∀ (n2 : 2 < HPow.hPow (α := ℕ) (β := ℕ) 2 0),
    4 ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∨ ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∧ Odd p
inl₁ :
  ∀ (n2 : 2 < HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)),
    4 ∣ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ∨
      ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ∧ Odd p
inl₂ :
  ∀ (k : ℕ) (n2 : 2 < HPow.hPow (α := ℕ) 2 (k + 1 + 1)),
    4 ∣ HPow.hPow (α := ℕ) 2 (k + 1 + 1) ∨ ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) 2 (k + 1 + 1) ∧ Odd p
inr : ∀ (p : ℕ) (hp : Prime p) (hdvd : p ∣ n) (hodd : Odd p), 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p

Tactic:
obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd

Premises used: Nat.eq_two_pow_or_exists_odd_prime_and_dvd, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
n2 : 2 < HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ 4 ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∨ ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∧ Odd p

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Factors
Goal:
n2 : 2 < HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)
⊢ 4 ∣ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ∨
    ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ∧ Odd p

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
n2 : 2 < HPow.hPow (α := ℕ) 2 (k + 1 + 1)
⊢ 4 ∣ HPow.hPow (α := ℕ) 2 (k + 1 + 1) ∨ ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) 2 (k + 1 + 1) ∧ Odd p

Tactic:
simp [Nat.pow_succ, mul_assoc]

Premises used: mul_assoc, Nat.pow_succ
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p

Tactic:
Or.inr ⟨p, hp, hdvd, hodd⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p

Tactic:
exact Or.inr ⟨p, hp, hdvd, hodd⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
n k : ℕ
hk : k ≠ 0
inl : (HPow.hPow (α := ℕ) 1 k).minFac = minFac 1
inr : ∀ (hn : n ≠ 1), (n ^ k).minFac = n.minFac
⊢ (n ^ k).minFac = n.minFac

Tactic:
rcases eq_or_ne n 1 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
k : ℕ
hk : k ≠ 0
⊢ (HPow.hPow (α := ℕ) 1 k).minFac = minFac 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ n ^ k ≠ 1

Tactic:
have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff_left hk).1 hk')
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
inr : n.minFac ≤ (n ^ k).minFac
⊢ (n ^ k).minFac = n.minFac

Tactic:
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm

Premises used: Nat.minFac_le_of_dvd, LE.le.antisymm, Nat.minFac_dvd, Dvd.dvd.pow, Nat.Prime.two_le, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ n.minFac ≤ (n ^ k).minFac

Tactic:
apply
    minFac_le_of_dvd (minFac_prime hnk).two_le
      ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.minFac_le_of_dvd, Nat.minFac_dvd, Nat.Prime.two_le, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Pow
Goal:
p k : ℕ
hp : Prime p
hk : k ≠ 0
rw : p.minFac = p
rw₁ rw₂ : p = p
⊢ (p ^ k).minFac = p

Tactic:
rw [Nat.pow_minFac hk, hp.minFac_eq]

Premises used: Nat.Prime.minFac_eq, Nat.pow_minFac
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
inl : sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
inr : ∀ (hs : s.Nonempty), sInf (a • s) = a • sInf s
⊢ sInf (a • s) = a • sInf s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a 0
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)

Tactic:
rw [smul_set_empty, Real.sInf_empty, smul_zero]

Premises used: Set.smul_set_empty, smul_zero, Real.sInf_empty
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
inr :
  ∀ (ha : LE.le.{u_2} (α := α) 0 0),
    sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)
inr₁ : ∀ (ha' : 0 < a), sInf (a • s) = a • sInf s
⊢ sInf (a • s) = a • sInf s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
inr : Eq (α := ℝ) (sInf 0) 0
⊢ sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)

Tactic:
rw [zero_smul_set hs, zero_smul]

Premises used: Set.zero_smul_set, zero_smul
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ Eq (α := ℝ) (sInf 0) 0

Tactic:
csInf_singleton 0

Premises used: csInf_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ Eq (α := ℝ) (sInf 0) 0

Tactic:
exact csInf_singleton 0

Premises used: csInf_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
pos : ∀ (h : BddBelow s), sInf (a • s) = a • sInf s
neg : ∀ (h : ¬BddBelow s), sInf (a • s) = a • sInf s
⊢ sInf (a • s) = a • sInf s

Tactic:
by_cases h : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
((OrderIso.smulRight ha').map_csInf' hs h).symm

Premises used: OrderIso.map_csInf', OrderIso.smulRight, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
exact ((OrderIso.smulRight ha').map_csInf' hs h).symm

Premises used: OrderIso.map_csInf', OrderIso.smulRight, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddBelow s
neg : 0 = a • sInf s
neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ sInf (a • s) = a • sInf s

Tactic:
rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]

Premises used: Real.sInf_of_not_bddBelow, smul_zero, mt, Iff.mp, bddBelow_smul_iff_of_pos
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
f : ι → ℝ
⊢ HSMul.hSMul (β := ℝ) a (⨅ (i : ι), f i) = ⨅ (i : ι), a • f i

Tactic:
(Real.sInf_smul_of_nonneg ha _).symm.trans <| congr_arg sInf <| (range_comp _ _).symm

Premises used: Set.range_comp, iInf, Real.sInf_smul_of_nonneg, congr_arg, Eq.symm, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
inl : sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
inr : ∀ (hs : s.Nonempty), sSup (a • s) = a • sSup s
⊢ sSup (a • s) = a • sSup s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a 0
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)

Tactic:
rw [smul_set_empty, Real.sSup_empty, smul_zero]

Premises used: Real.sSup_empty, Set.smul_set_empty, smul_zero
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
inr :
  ∀ (ha : LE.le.{u_2} (α := α) 0 0),
    sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)
inr₁ : ∀ (ha' : 0 < a), sSup (a • s) = a • sSup s
⊢ sSup (a • s) = a • sSup s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
inr : Eq (α := ℝ) (sSup 0) 0
⊢ sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)

Tactic:
rw [zero_smul_set hs, zero_smul]

Premises used: Set.zero_smul_set, zero_smul
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ Eq (α := ℝ) (sSup 0) 0

Tactic:
csSup_singleton 0

Premises used: csSup_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ Eq (α := ℝ) (sSup 0) 0

Tactic:
exact csSup_singleton 0

Premises used: csSup_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
pos : ∀ (h : BddAbove s), sSup (a • s) = a • sSup s
neg : ∀ (h : ¬BddAbove s), sSup (a • s) = a • sSup s
⊢ sSup (a • s) = a • sSup s

Tactic:
by_cases h : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddAbove s
⊢ sSup (a • s) = a • sSup s

Tactic:
((OrderIso.smulRight ha').map_csSup' hs h).symm

Premises used: OrderIso.map_csSup', OrderIso.smulRight, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddAbove s
⊢ sSup (a • s) = a • sSup s

Tactic:
exact ((OrderIso.smulRight ha').map_csSup' hs h).symm

Premises used: OrderIso.map_csSup', OrderIso.smulRight, Eq.symm