awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False
have h'₁ : φ a = φ (p * a * d)
Tactic: rw [← mul_assoc, mul_comm a] at h'
Cleared hypotheses: h', hb, this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ False
have neg : φ a < φ (p * a * d)
Tactic: suffices a.totient < (p * a * d).totient by
    rw [← mul_assoc, mul_comm a] at h'
    exact h'.not_lt this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (p * a * d)
have neg : φ a < φ (a * p * d)
Tactic: rw [mul_comm p]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p * d)
have neg : φ a < φ (a * p)
Tactic: refine lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : φ a < φ (a * p)
⊢ φ a < φ (a * p * d)
have neg₁ : 0 < φ (a * p * d)
Tactic: refine lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p)
have neg : 1 < p
Tactic: rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : 1 < p
⊢ φ a < φ (a * p)
have neg₁ : 0 < φ a
Tactic: rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ a * p * d ≠ 0
have rwa : a * (p * d) ≠ 0
Tactic: rwa [mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
⊢ a = b
have pos : ∀ (ha' : a = 0), a = b
Tactic: by_cases ha' : a = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
pos : ∀ (ha' : a = 0), a = b
⊢ a = b
have neg : ∀ (ha' : ¬a = 0), a = b
Tactic: by_cases ha' : a = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
⊢ a = b
have h'₁ : b = 0
Tactic: rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'
Cleared hypotheses: h', ha'
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' pos : a = 0
⊢ a = b
have pos₁ : Eq (α := ℕ) 0 0
Tactic: rw [h', ha']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b
have neg : ∀ (h : 2 * a = b), False
Tactic: refine (eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
h_1 : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
⊢ False
have h'₁ : Eq (α := ℕ) 2 1
Tactic: rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'
Cleared hypotheses: h', ha', h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
have rw : p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))
Tactic: rw [mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))
have refine : 1 ≤ k * (p - 1)
Tactic: refine le_mul_of_one_le_right (Nat.zero_le _) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
have h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
Tactic: have h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1)) := by
    rw [mul_left_comm]
    refine le_mul_of_one_le_right (Nat.zero_le _) ?_
    exact Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
have simp_rw : p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: simp_rw [Nat.totient_prime_pow hp hk, Nat.primeFactors_prime_pow hk.ne' hp, Finset.prod_singleton,
    Nat.mul_div_left _ (Nat.sub_pos_of_lt hp.one_lt), ← pow_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
have rw : p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: rw [Nat.pow_div h hp.pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
have simp_rw : p ^ (k * (p ^ (k - 1) * p) - k * p ^ (k - 1) - p ^ (k - 1)) =
  p ^ (p ^ (k - 1) * (p * k) - p ^ (k - 1) * k - p ^ (k - 1))
Tactic: simp_rw [Nat.sub_mul, one_mul, Nat.mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : 0 < n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
have this : ∏ p ∈ n.primeFactors, p ∣ n
Tactic: have := Nat.prod_primeFactors_dvd n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : 0 < n
this : ∏ p ∈ n.primeFactors, p ∣ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
have this₁ : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
Tactic: rw [← Nat.pow_dvd_pow_iff (Nat.totient_pos.mpr hn).ne', ← Finset.prod_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
have refine : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), p ^ (φ n / (p - 1)) ∣ p ^ φ n
Tactic: refine dvd_trans (Finset.prod_dvd_prod_of_dvd _ _ fun p hp ↦ ?_) this
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
⊢ WellFounded (Upto.GT p)
have rw : WellFounded (α := Upto p) (InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)
have suffices : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
Tactic: suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
have h₁ : ∀ (a : ℕ) (ha : ∀ (j : ℕ), j < a → ¬p j) (b : ℕ) (property : ∀ (j : ℕ), j < b → ¬p j),
  Upto.GT p (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property) ↔
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (y : Upto p) ↦ x - (↑y : ℕ))
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property)
Tactic: ext ⟨a, ha⟩ ⟨b, _⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property) ↔
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (y : Upto p) ↦ x - (↑y : ℕ))
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) a ha)
      (Subtype.mk (p := fun (i : ℕ) ↦ ∀ (j : ℕ), j < i → ¬p j) b property)
have h₁ : a > b ↔ x - a < x - b
Tactic: dsimp [InvImage, Upto.GT]
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b
have h₁ : a > b ↔ b < a
Tactic: rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
⊢ ¬p j
have inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
⊢ ¬p j
have inr : ∀ (h' : (↑x : ℕ) < (↑x : ℕ).succ), ¬p (↑x : ℕ)
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)
Cleared hypotheses: j, h'
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
⊢ ¬p j
have inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]
-- Lean 4 proof step from Mathlib.Data.Nat.Upto (goal)
Goal:
p : ℕ → Prop
x : Upto p
h : ¬p (↑x : ℕ)
j : ℕ
h' : j < (↑x : ℕ).succ
inl : ∀ (h' : j < (↑x : ℕ)), ¬p j
⊢ ¬p j
have inr : ∀ (h' : (↑x : ℕ) < (↑x : ℕ).succ), ¬p (↑x : ℕ)
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]
Cleared hypotheses: j, h'
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0
have bot : ⊥ + m = 0 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 0 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 0
⊢ n + m = 0 ↔ n = 0 ∧ m = 0
have coe : ∀ (a : ℕ), (↑a : WithBot ℕ) + m = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
⊢ (↑a : WithBot ℕ) + m = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 0
have coe : (↑a : WithBot ℕ) + ⊥ = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
coe : (↑a : WithBot ℕ) + ⊥ = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 0
⊢ (↑a : WithBot ℕ) + m = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 0
have coe₁ : ∀ (a_1 : ℕ), (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 0 ↔ (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
have bot : ⊥ + m = 1 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 1 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 0
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
have coe : ∀ (a : ℕ), (↑a : WithBot ℕ) + m = 1 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
⊢ (↑a : WithBot ℕ) + m = 1 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 0
have coe : (↑a : WithBot ℕ) + ⊥ = 1 ↔
  (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 1 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 0
⊢ (↑a : WithBot ℕ) + m = 1 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 0
have coe₁ : ∀ (a_1 : ℕ),
  (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 1 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
have bot : ⊥ + m = 2 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
bot : ⊥ + m = 2 ↔ Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 0
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
have coe : ∀ (a : ℕ),
  (↑a : WithBot ℕ) + m = 2 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
⊢ (↑a : WithBot ℕ) + m = 2 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 0
have coe : (↑a : WithBot ℕ) + ⊥ = 2 ↔
  (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
    (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 2 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 0
⊢ (↑a : WithBot ℕ) + m = 2 ↔ (↑a : WithBot ℕ) = 0 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 1 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 0
have coe₁ : ∀ (a_1 : ℕ),
  (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 2 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
      (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
have bot : ⊥ + m = 3 ↔
  Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 3 ∨
    Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 3 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
bot :
  ⊥ + m = 3 ↔
    Eq (α := WithBot ℕ) ⊥ 0 ∧ m = 3 ∨
      Eq (α := WithBot ℕ) ⊥ 1 ∧ m = 2 ∨ Eq (α := WithBot ℕ) ⊥ 2 ∧ m = 1 ∨ Eq (α := WithBot ℕ) ⊥ 3 ∧ m = 0
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
have coe : ∀ (a : ℕ),
  (↑a : WithBot ℕ) + m = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ m = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ m = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
⊢ (↑a : WithBot ℕ) + m = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ m = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ m = 0
have coe : (↑a : WithBot ℕ) + ⊥ = 3 ↔
  (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 3 ∨
    (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
      (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 3 ∧ Eq (α := WithBot ℕ) ⊥ 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
coe :
  (↑a : WithBot ℕ) + ⊥ = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ Eq (α := WithBot ℕ) ⊥ 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ Eq (α := WithBot ℕ) ⊥ 2 ∨
        (↑a : WithBot ℕ) = 2 ∧ Eq (α := WithBot ℕ) ⊥ 1 ∨ (↑a : WithBot ℕ) = 3 ∧ Eq (α := WithBot ℕ) ⊥ 0
⊢ (↑a : WithBot ℕ) + m = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ m = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ m = 2 ∨ (↑a : WithBot ℕ) = 2 ∧ m = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ m = 0
have coe₁ : ∀ (a_1 : ℕ),
  (↑a : WithBot ℕ) + (↑a_1 : WithBot ℕ) = 3 ↔
    (↑a : WithBot ℕ) = 0 ∧ (↑a_1 : WithBot ℕ) = 3 ∨
      (↑a : WithBot ℕ) = 1 ∧ (↑a_1 : WithBot ℕ) = 2 ∨
        (↑a : WithBot ℕ) = 2 ∧ (↑a_1 : WithBot ℕ) = 1 ∨ (↑a : WithBot ℕ) = 3 ∧ (↑a_1 : WithBot ℕ) = 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n : ℕ
⊢ LE.le (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
have rw : 0 ≤ n
Tactic: rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x
have refine : ∀ (h : 0 < x), 1 ≤ x
Tactic: refine ⟨zero_lt_one.trans_le, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
have bot : ∀ (h : LT.lt (α := WithBot ℕ) 0 ⊥), LE.le (α := WithBot ℕ) 1 ⊥
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
x : WithBot ℕ
h : 0 < x
bot : ∀ (h : LT.lt (α := WithBot ℕ) 0 ⊥), LE.le (α := WithBot ℕ) 1 ⊥
⊢ 1 ≤ x
have coe : ∀ (a : ℕ) (h : 0 < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)
have coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
Tactic: rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)
have coe₁ : ∀ (h : 0 < a), 1 ≤ (↑a : WithBot ℕ)
Tactic: rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
coe₁ : ∀ (h : 0 < a), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)
have coe₂ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
Tactic: rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
coe₁ : ∀ (h : 0 < a), 1 ≤ (↑a : WithBot ℕ)
coe₂ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
coe₃ : ∀ (h : 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)
have coe₄ : ∀ (h : (↑1 : WithBot ℕ) ≤ (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
Tactic: rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a : ℕ
h : 0 < (↑a : WithBot ℕ)
coe : ∀ (h : (↑0 : WithBot ℕ) < (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
coe₁ : ∀ (h : 0 < a), 1 ≤ (↑a : WithBot ℕ)
coe₂ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
coe₃ : ∀ (h : 1 ≤ a), 1 ≤ (↑a : WithBot ℕ)
coe₄ : ∀ (h : (↑1 : WithBot ℕ) ≤ (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
⊢ 1 ≤ (↑a : WithBot ℕ)
have coe₅ : ∀ (h : 1 ≤ (↑a : WithBot ℕ)), 1 ≤ (↑a : WithBot ℕ)
Tactic: rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
h : n < m
⊢ n + 1 ≤ m
have bot : ∀ (h : ⊥ < m), HAdd.hAdd (α := WithBot ℕ) ⊥ 1 ≤ m
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
n m : WithBot ℕ
h : n < m
bot : ∀ (h : ⊥ < m), HAdd.hAdd (α := WithBot ℕ) ⊥ 1 ≤ m
⊢ n + 1 ≤ m
have coe : ∀ (a : ℕ) (h : (↑a : WithBot ℕ) < m), (↑a : WithBot ℕ) + 1 ≤ m
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
h : (↑a : WithBot ℕ) < m
⊢ (↑a : WithBot ℕ) + 1 ≤ m
have coe : ∀ (h : (↑a : WithBot ℕ) < ⊥), (↑a : WithBot ℕ) + 1 ≤ ⊥
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
m : WithBot ℕ
a : ℕ
h : (↑a : WithBot ℕ) < m
coe : ∀ (h : (↑a : WithBot ℕ) < ⊥), (↑a : WithBot ℕ) + 1 ≤ ⊥
⊢ (↑a : WithBot ℕ) + 1 ≤ m
have coe₁ : ∀ (a_1 : ℕ) (h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
have coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
have coe₁ : ∀ (h : a + 1 ≤ a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₁ : ∀ (h : a + 1 ≤ a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
have coe₂ : ∀ (h : (↑(a + 1) : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₁ : ∀ (h : a + 1 ≤ a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₂ : ∀ (h : (↑(a + 1) : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
have coe₃ : ∀ (h : (↑a : WithBot ℕ) + (↑1 : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.WithBot (goal)
Goal:
a a_1 : ℕ
h : (↑a : WithBot ℕ) < (↑a_1 : WithBot ℕ)
coe : ∀ (h : a < a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₁ : ∀ (h : a + 1 ≤ a_1), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₂ : ∀ (h : (↑(a + 1) : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
coe₃ : ∀ (h : (↑a : WithBot ℕ) + (↑1 : WithBot ℕ) ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
⊢ (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
have coe₄ : ∀ (h : (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)), (↑a : WithBot ℕ) + 1 ≤ (↑a_1 : WithBot ℕ)
Tactic: rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.Bitwise (goal)
Goal:
b : Bool
⊢ (b::zero b) = zero b
have false : (false::zero false) = zero false
Tactic: cases b
Cleared hypotheses: b