awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have H : ∀ (a : α),
  a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
Tactic: have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : Eq.{u_1 + 1} (α := α) (↑(na * nb) : α) (↑((↑k : ℤ) * nc) : α)
Tactic: have h₁ := congr_arg (Int.cast (R := α)) h₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : Eq.{u_1 + 1} (α := α) (↑(na * nb) : α) (↑((↑k : ℤ) * nc) : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
Tactic: simp only [Int.cast_mul, Int.cast_natCast] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have simp : HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
Tactic: simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : Eq.{u_1 + 1} (α := α)
  ((fun (x : ℕ) ↦
      HMul.hMul (α := α) (↑nc : α) (↑x : α) *
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
    (da * db))
  ((fun (x : ℕ) ↦
      HMul.hMul (α := α) (↑nc : α) (↑x : α) *
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
    (k * dc))
Tactic: have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  Eq.{u_1 + 1} (α := α)
    ((fun (x : ℕ) ↦
        HMul.hMul (α := α) (↑nc : α) (↑x : α) *
          (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
      (da * db))
    ((fun (x : ℕ) ↦
        HMul.hMul (α := α) (↑nc : α) (↑x : α) *
          (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
      (k * dc))
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: simp only [Nat.cast_mul, ← mul_assoc] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: rw [H] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: simp only [mul_invOf_cancel_right'] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have rw : HMul.hMul (α := α) (↑nc : α) (↑k : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: rw [h₂, Nat.cast_commute]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
x y : ℕ
⊢ x.ble y = false ↔ y < x
have rw : x.ble y = false ↔ ¬x ≤ y
Tactic: rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
x y : ℕ
rw : x.ble y = false ↔ ¬x ≤ y
⊢ x.ble y = false ↔ y < x
have rw₁ : ¬x.ble y = true ↔ ¬x ≤ y
Tactic: rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
x y : ℕ
rw : x.ble y = false ↔ ¬x ≤ y
rw₁ : ¬x.ble y = true ↔ ¬x ≤ y
⊢ x.ble y = false ↔ y < x
have rw₂ : ¬x ≤ y ↔ ¬x ≤ y
Tactic: rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u
inst : Semiring α
num denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have e_a : inv = inv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u
inst : Ring α
num : ℤ
denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have e_a : inv = inv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []
have rw : List.range (↑0 : ℕ) = []
Tactic: rw [pn.out, Nat.cast_zero, List.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : List.range (↑0 : ℕ) = []
⊢ List.range n = []
have rw₁ : List.range 0 = []
Tactic: rw [pn.out, Nat.cast_zero, List.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : List.range (↑0 : ℕ) = []
rw₁ : List.range 0 = []
⊢ List.range n = []
have rw₂ : Eq (α := List ℕ) [] []
Tactic: rw [pn.out, Nat.cast_zero, List.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
have rw : List.range (↑nn : ℕ) = 0 :: List.map Nat.succ (List.range n')
Tactic: rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : List.range (↑nn : ℕ) = 0 :: List.map Nat.succ (List.range n')
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
have rw₁ : List.range nn = 0 :: List.map Nat.succ (List.range n')
Tactic: rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : List.range (↑nn : ℕ) = 0 :: List.map Nat.succ (List.range n')
rw₁ : List.range nn = 0 :: List.map Nat.succ (List.range n')
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
have rw₂ : List.range n'.succ = 0 :: List.map Nat.succ (List.range n')
Tactic: rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : List.range (↑nn : ℕ) = 0 :: List.map Nat.succ (List.range n')
rw₁ : List.range nn = 0 :: List.map Nat.succ (List.range n')
rw₂ : List.range n'.succ = 0 :: List.map Nat.succ (List.range n')
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
have rw₃ : 0 :: List.map Nat.succ (List.range n') = 0 :: List.map Nat.succ (List.range n')
Tactic: rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0
have rw : Multiset.range (↑0 : ℕ) = 0
Tactic: rw [pn.out, Nat.cast_zero, Multiset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Multiset.range (↑0 : ℕ) = 0
⊢ Multiset.range n = 0
have rw₁ : Multiset.range 0 = 0
Tactic: rw [pn.out, Nat.cast_zero, Multiset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Multiset.range (↑0 : ℕ) = 0
rw₁ : Multiset.range 0 = 0
⊢ Multiset.range n = 0
have rw₂ : Eq (α := Multiset ℕ) 0 0
Tactic: rw [pn.out, Nat.cast_zero, Multiset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
have rw : Multiset.range (↑nn : ℕ) = n' ::ₘ Multiset.range n'
Tactic: rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Multiset.range (↑nn : ℕ) = n' ::ₘ Multiset.range n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
have rw₁ : Multiset.range nn = n' ::ₘ Multiset.range n'
Tactic: rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Multiset.range (↑nn : ℕ) = n' ::ₘ Multiset.range n'
rw₁ : Multiset.range nn = n' ::ₘ Multiset.range n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
have rw₂ : Multiset.range n'.succ = n' ::ₘ Multiset.range n'
Tactic: rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Multiset.range (↑nn : ℕ) = n' ::ₘ Multiset.range n'
rw₁ : Multiset.range nn = n' ::ₘ Multiset.range n'
rw₂ : Multiset.range n'.succ = n' ::ₘ Multiset.range n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
have rw₃ : n' ::ₘ Multiset.range n' = n' ::ₘ Multiset.range n'
Tactic: rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅
have rw : Finset.range (↑0 : ℕ) = ∅
Tactic: rw [pn.out, Nat.cast_zero, Finset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Finset.range (↑0 : ℕ) = ∅
⊢ Finset.range n = ∅
have rw₁ : Finset.range 0 = ∅
Tactic: rw [pn.out, Nat.cast_zero, Finset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Finset.range (↑0 : ℕ) = ∅
rw₁ : Finset.range 0 = ∅
⊢ Finset.range n = ∅
have rw₂ : Eq (α := Finset ℕ) ∅ ∅
Tactic: rw [pn.out, Nat.cast_zero, Finset.range_zero]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') sorry
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') ⋯
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have rw₁ : Finset.range nn = Finset.cons n' (Finset.range n') sorry
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') ⋯
rw₁ : Finset.range nn = Finset.cons n' (Finset.range n') ⋯
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have rw₂ : Finset.range n'.succ = Finset.cons n' (Finset.range n') sorry
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') ⋯
rw₁ : Finset.range nn = Finset.cons n' (Finset.range n') ⋯
rw₂ : Finset.range n'.succ = Finset.cons n' (Finset.range n') ⋯
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have rw₃ : insert n' (Finset.range n') = Finset.cons n' (Finset.range n') sorry
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') ⋯
rw₁ : Finset.range nn = Finset.cons n' (Finset.range n') ⋯
rw₂ : Finset.range n'.succ = Finset.cons n' (Finset.range n') ⋯
rw₃ : insert n' (Finset.range n') = Finset.cons n' (Finset.range n') ⋯
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have rw₄ : Finset.cons n' (Finset.range n') sorry = Finset.cons n' (Finset.range n') sorry
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]