awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hy : y = 0
pos :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
pos₁ :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [dif_pos hxy, dif_pos hy, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (hypothesis)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have hx : x ≠ 0
Tactic: obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (hypothesis)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have hy : y ≠ 0
Tactic: obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have neg : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hxy) : ℤ) =
  HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx * unzero hy) : ℤ)
Tactic: rw [dif_neg hxy, dif_neg hx, dif_neg hy, ← zpow_add' (Or.inl he), ← toAdd_mul]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hxy) : ℤ) =
    HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx * unzero hy) : ℤ)
have neg : unzero hxy = unzero hx * unzero hy
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ unzero hxy = unzero hx * unzero hy
have neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
⊢ unzero hxy = unzero hx * unzero hy
have neg₁ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) =
  (↑(unzero hx) : WithZero (Multiplicative ℤ)) * (↑(unzero hy) : WithZero (Multiplicative ℤ))
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
neg₁ :
  (↑(unzero hxy) : WithZero (Multiplicative ℤ)) =
    (↑(unzero hx) : WithZero (Multiplicative ℤ)) * (↑(unzero hy) : WithZero (Multiplicative ℤ))
⊢ unzero hxy = unzero hx * unzero hy
have neg₂ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * (↑(unzero hy) : WithZero (Multiplicative ℤ))
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
neg₁ :
  (↑(unzero hxy) : WithZero (Multiplicative ℤ)) =
    (↑(unzero hx) : WithZero (Multiplicative ℤ)) * (↑(unzero hy) : WithZero (Multiplicative ℤ))
neg₂ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * (↑(unzero hy) : WithZero (Multiplicative ℤ))
⊢ unzero hxy = unzero hx * unzero hy
have neg₃ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * y
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
neg₁ :
  (↑(unzero hxy) : WithZero (Multiplicative ℤ)) =
    (↑(unzero hx) : WithZero (Multiplicative ℤ)) * (↑(unzero hy) : WithZero (Multiplicative ℤ))
neg₂ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * (↑(unzero hy) : WithZero (Multiplicative ℤ))
neg₃ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * y
⊢ unzero hxy = unzero hx * unzero hy
have neg₄ : x * y = x * y
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : 1 < e
x y : WithZero (Multiplicative ℤ)
⊢ x < y →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) y : ℝ≥0)
have zero : x < 0 →
  LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
    ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : 1 < e
x y : WithZero (Multiplicative ℤ)
zero :
  x < 0 →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
⊢ x < y →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) y : ℝ≥0)
have coe : ∀ (a : Multiplicative ℤ),
  x < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
a : Multiplicative ℤ
⊢ x < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
have coe : 0 < (↑a : WithZero (Multiplicative ℤ)) →
  LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
    ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
a : Multiplicative ℤ
coe :
  0 < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
⊢ x < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
have coe₁ : ∀ (a_1 : Multiplicative ℤ),
  (↑a_1 : WithZero (Multiplicative ℤ)) < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a_1 : WithZero (Multiplicative ℤ)) : ℝ≥0)
      ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
have pos : ∀ (hm : m = 0), Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
pos : ∀ (hm : m = 0), Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
have neg : ∀ (hm : ¬m = 0), Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
have neg : ∀ (h1 : Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)), m = 1
Tactic: refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (hypothesis)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
⊢ m = 1
have h1₁ : unzero hm = 1
Tactic: rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ m = 1
have neg : (↑(unzero hm) : WithZero (Multiplicative ℤ)) = 1
Tactic: rw [← WithZero.coe_unzero hm, h1, coe_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
neg : (↑(unzero hm) : WithZero (Multiplicative ℤ)) = 1
⊢ m = 1
have neg₁ : Eq (α := WithZero (Multiplicative ℤ)) (↑1 : WithZero (Multiplicative ℤ)) 1
Tactic: rw [← WithZero.coe_unzero hm, h1, coe_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
neg : (↑(unzero hm) : WithZero (Multiplicative ℤ)) = 1
neg₁ : Eq (α := WithZero (Multiplicative ℤ)) (↑1 : WithZero (Multiplicative ℤ)) 1
⊢ m = 1
have neg₂ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
Tactic: rw [← WithZero.coe_unzero hm, h1, coe_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m < 1
have rw : LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
  LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
    ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
Tactic: rw [← (toNNReal_strictMono he).lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
rw :
  LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m < 1
have rw₁ : LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
  LT.lt (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
Tactic: rw [← (toNNReal_strictMono he).lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m ≤ 1
have rw : LE.le (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
  LE.le (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
    ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
Tactic: rw [← (toNNReal_strictMono he).le_iff_le, map_one]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
rw :
  LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m ≤ 1
have rw₁ : LE.le (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
  LE.le (α := ℝ≥0) ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
Tactic: rw [← (toNNReal_strictMono he).le_iff_le, map_one]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs = ys)
have rw : Decidable (xs.entries (β := β) = ys.entries (β := β))
Tactic: rw [AList.ext_iff]
-- Lean 4 proof step from Mathlib.Data.List.AList (hypothesis)
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this : DecidableEq α := Classical.decEq α
⊢ k ∈ s₂.keys (β := β)
have this₁ : Sigma.mk (β := β) k ((lookup (β := β) k s₁).get sorry) ∈ s₂.entries (β := β)
Tactic: have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
-- Lean 4 proof step from Mathlib.Data.List.AList (hypothesis)
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : Sigma.mk (β := β) k ((lookup (β := β) k s₁).get ⋯) ∈ s₂.entries (β := β)
⊢ k ∈ s₂.keys (β := β)
have this₁ : lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get sorry)
Tactic: rw [← mem_lookup_iff, Option.mem_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get ⋯)
⊢ k ∈ s₂.keys (β := β)
have rw : (some ((lookup (β := β) k s₁).get sorry)).isSome = true
Tactic: rw [← mem_keys, ← lookup_isSome, this]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace (β := β) a b s ↔ a' ∈ s
have rw : a' ∈ (replace (β := β) a b s).keys (β := β) ↔ a' ∈ s
Tactic: rw [mem_keys, keys_replace, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s : AList β
rw : a' ∈ (replace (β := β) a b s).keys (β := β) ↔ a' ∈ s
⊢ a' ∈ replace (β := β) a b s ↔ a' ∈ s
have rw₁ : a' ∈ s.keys (β := β) ↔ a' ∈ s
Tactic: rw [mem_keys, keys_replace, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s : AList β
rw : a' ∈ (replace (β := β) a b s).keys (β := β) ↔ a' ∈ s
rw₁ : a' ∈ s.keys (β := β) ↔ a' ∈ s
⊢ a' ∈ replace (β := β) a b s ↔ a' ∈ s
have rw₂ : a' ∈ s ↔ a' ∈ s
Tactic: rw [mem_keys, keys_replace, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase (β := β) a s ↔ a' ≠ a ∧ a' ∈ s
have rw : a' ∈ (erase (β := β) a s).keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
Tactic: rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
rw : a' ∈ (erase (β := β) a s).keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
⊢ a' ∈ erase (β := β) a s ↔ a' ≠ a ∧ a' ∈ s
have rw₁ : a' ∈ s.keys (β := β).erase a ↔ a' ≠ a ∧ a' ∈ s
Tactic: rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
rw : a' ∈ (erase (β := β) a s).keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
rw₁ : a' ∈ s.keys (β := β).erase a ↔ a' ≠ a ∧ a' ∈ s
⊢ a' ∈ erase (β := β) a s ↔ a' ≠ a ∧ a' ∈ s
have rw₂ : a' ≠ a ∧ a' ∈ s.keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
Tactic: rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
rw : a' ∈ (erase (β := β) a s).keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
rw₁ : a' ∈ s.keys (β := β).erase a ↔ a' ≠ a ∧ a' ∈ s
rw₂ : a' ≠ a ∧ a' ∈ s.keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
⊢ a' ∈ erase (β := β) a s ↔ a' ≠ a ∧ a' ∈ s
have rw₃ : a' ≠ a ∧ a' ∈ s ↔ a' ≠ a ∧ a' ∈ s
Tactic: rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert (β := β) a b s).entries (β := β) = Sigma.mk (β := β) a b :: s.entries (β := β)
have rw : Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β)) = Sigma.mk (β := β) a b :: s.entries (β := β)
Tactic: rw [entries_insert, kerase_of_notMem_keys h]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
rw : Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β)) = Sigma.mk (β := β) a b :: s.entries (β := β)
⊢ (insert (β := β) a b s).entries (β := β) = Sigma.mk (β := β) a b :: s.entries (β := β)
have rw₁ : Sigma.mk (β := β) a b :: s.entries (β := β) = Sigma.mk (β := β) a b :: s.entries (β := β)
Tactic: rw [entries_insert, kerase_of_notMem_keys h]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
have pos : ∀ (h : k' = k), lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
Tactic: by_cases h : k' = k
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
pos : ∀ (h : k' = k), lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
have neg : ∀ (h : ¬k' = k), lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
Tactic: by_cases h : k' = k
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
h : k' = k
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
have pos : ∀ {v : β k'}, lookup (β := β) k' (insert (β := β) k' v l) = none ↔ k' ≠ k' ∧ lookup (β := β) k' l = none
Tactic: subst h
Cleared hypotheses: k, v, h
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
have rw : lookup (β := β) a (mk (β := β) (s.dedupKeys (β := β)) sorry) = dlookup (β := β) a s
Tactic: rw [List.toAList, lookup, dlookup_dedupKeys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (mk (β := β) (s.dedupKeys (β := β)) ⋯) = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
have rw₁ : dlookup (β := β) a ((mk (β := β) (s.dedupKeys (β := β)) sorry).entries (β := β)) = dlookup (β := β) a s
Tactic: rw [List.toAList, lookup, dlookup_dedupKeys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (mk (β := β) (s.dedupKeys (β := β)) ⋯) = dlookup (β := β) a s
rw₁ : dlookup (β := β) a ((mk (β := β) (s.dedupKeys (β := β)) ⋯).entries (β := β)) = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
have rw₂ : dlookup (β := β) a s = dlookup (β := β) a s
Tactic: rw [List.toAList, lookup, dlookup_dedupKeys]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ insert (β := β) a b' (insert (β := β) a b s) = insert (β := β) a b' s
have a₁ : (insert (β := β) a b' (insert (β := β) a b s)).entries (β := β) = (insert (β := β) a b' s).entries (β := β)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw : Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
  Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₁ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]