awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b n : ℕ
ha : Prime a
hb : b ≠ 0
⊢ replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
have zero : ∀ {b : ℕ} (hb : b ≠ 0), replicate 0 a <+~ b.primeFactorsList ↔ HPow.hPow (β := ℕ) a 0 ∣ 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 _ _
Cleared hypotheses: b, n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
have 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
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 _ _
Cleared hypotheses: b, n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
have rw : Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
Tactic: rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
    ← and_or_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ False
have apply : Prime 1
Tactic: apply not_prime_one
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime 1
have rw : Prime q
Tactic: rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
    (dvd_of_mem_primeFactorsList hqb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inl : ∀ (hab : Coprime 0 b), p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList
Tactic: rcases a.eq_zero_or_pos with (rfl | ha)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
inl : ∀ (hab : Coprime 0 b), p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inr : ∀ (ha : a > 0), p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
Tactic: rcases a.eq_zero_or_pos with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inr : ∀ (hab : a.Coprime 0), p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inr₁ : ∀ (hb : b > 0), p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inr : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
Tactic: rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
have inr₁ : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
Tactic: rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
⊢ p ∈ (a * b).primeFactorsList
have inl : ∀ (hpa : p ∈ primeFactorsList 0), p ∈ (0 * b).primeFactorsList
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, hpa
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
inl : ∀ (hpa : p ∈ primeFactorsList 0), p ∈ (0 * b).primeFactorsList
⊢ p ∈ (a * b).primeFactorsList
have inr : ∀ (ha : a ≠ 0), p ∈ (a * b).primeFactorsList
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList
have rw : p ∈ (b * a).primeFactorsList
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
n2 : 2 < n
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p
have inl : ∀ (n2 : 2 < HPow.hPow (α := ℕ) (β := ℕ) 2 0),
  4 ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∨ ∃ (p : ℕ), Prime p ∧ p ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ∧ Odd p
Tactic: obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
Cleared hypotheses: n, n2
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p
have 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
Tactic: obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
Cleared hypotheses: n, n2
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p
have 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
Tactic: obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
Cleared hypotheses: n, n2
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
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
⊢ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p
have inr : ∀ (p : ℕ) (hp : Prime p) (hdvd : p ∣ n) (hodd : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (goal)
Goal:
n k : ℕ
hk : k ≠ 0
⊢ (n ^ k).minFac = n.minFac
have inl : (HPow.hPow (α := ℕ) 1 k).minFac = minFac 1
Tactic: rcases eq_or_ne n 1 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (goal)
Goal:
n k : ℕ
hk : k ≠ 0
inl : (HPow.hPow (α := ℕ) 1 k).minFac = minFac 1
⊢ (n ^ k).minFac = n.minFac
have inr : ∀ (hn : n ≠ 1), (n ^ k).minFac = n.minFac
Tactic: rcases eq_or_ne n 1 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (hypothesis)
Goal:
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac
have hnk : n ^ k ≠ 1
Tactic: have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff_left hk).1 hk')
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (goal)
Goal:
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ (n ^ k).minFac = n.minFac
have inr : n.minFac ≤ (n ^ k).minFac
Tactic: apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (goal)
Goal:
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ (p ^ k).minFac = p
have rw : p.minFac = p
Tactic: rw [Nat.pow_minFac hk, hp.minFac_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Pow (goal)
Goal:
p k : ℕ
hp : Prime p
hk : k ≠ 0
rw : p.minFac = p
⊢ (p ^ k).minFac = p
have rw₁ : p = p
Tactic: rw [Nat.pow_minFac hk, hp.minFac_eq]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sInf (a • s) = a • sInf s
have inl : sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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 ∅)
⊢ sInf (a • s) = a • sInf s
have inr : ∀ (hs : s.Nonempty), sInf (a • s) = a • sInf s
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
Tactic: rw [smul_set_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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 ∅)
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [smul_set_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [smul_set_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (a • s) = a • sInf s
have 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)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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)
⊢ sInf (a • s) = a • sInf s
have inr₁ : ∀ (ha' : 0 < a), sInf (a • s) = a • sInf s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)
have inr : Eq (α := ℝ) (sInf 0) 0
Tactic: rw [zero_smul_set hs, zero_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (a • s) = a • sInf s
have pos : ∀ (h : BddBelow s), sInf (a • s) = a • sInf s
Tactic: by_cases h : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (a • s) = a • sInf s
have neg : ∀ (h : ¬BddBelow s), sInf (a • s) = a • sInf s
Tactic: by_cases h : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
have neg : 0 = 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]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (a • s) = a • sInf s
have neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sInf (a • s) = a • sInf s
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sSup (a • s) = a • sSup s
have inl : sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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 ∅)
⊢ sSup (a • s) = a • sSup s
have inr : ∀ (hs : s.Nonempty), sSup (a • s) = a • sSup s
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
Tactic: rw [smul_set_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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 ∅)
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [smul_set_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [smul_set_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sSup (a • s) = a • sSup s
have 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)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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)
⊢ sSup (a • s) = a • sSup s
have inr₁ : ∀ (ha' : 0 < a), sSup (a • s) = a • sSup s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)
have inr : Eq (α := ℝ) (sSup 0) 0
Tactic: rw [zero_smul_set hs, zero_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sSup (a • s) = a • sSup s
have pos : ∀ (h : BddAbove s), sSup (a • s) = a • sSup s
Tactic: by_cases h : BddAbove s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
⊢ sSup (a • s) = a • sSup s
have neg : ∀ (h : ¬BddAbove s), sSup (a • s) = a • sSup s
Tactic: by_cases h : BddAbove s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
have neg : 0 = a • sSup s
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
neg : 0 = a • sSup s
⊢ sSup (a • s) = a • sSup s
have neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
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
neg : 0 = a • sSup s
neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
⊢ sSup (a • s) = a • sSup s
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
⊢ sInf (a • s) = a • sSup s
have inl : sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
inl : sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
⊢ sInf (a • s) = a • sSup s
have inr : ∀ (hs : s.Nonempty), sInf (a • s) = a • sSup s
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
Tactic: rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sSup ∅)
Tactic: rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sSup ∅)
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl₂ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]