awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (hypothesis)
Goal:
a b : ℕ
h : a ≠ 0
⊢ b < if a < b then b * b + a else a * a + a + b
have this : a ≤ a * a
Tactic: have := Nat.le_mul_self a
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (hypothesis)
Goal:
a b : ℕ
h : a ≠ 0
this : a ≤ a * a
⊢ b < if a < b then b * b + a else a * a + a + b
have this₁ : b ≤ b * b
Tactic: have := Nat.le_mul_self b
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
a b : ℕ
h : a ≠ 0
this_1 : a ≤ a * a
this : b ≤ b * b
⊢ b < if a < b then b * b + a else a * a + a + b
have isTrue : a < b → b < b * b + a
Tactic: split
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
a b : ℕ
h : a ≠ 0
this_1 : a ≤ a * a
this : b ≤ b * b
isTrue : a < b → b < b * b + a
⊢ b < if a < b then b * b + a else a * a + a + b
have isFalse : ¬a < b → b < a * a + a + b
Tactic: split
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
⊢ S.decode (S.nat n).encode = S.nat n
have nat : (let p := Nat.unpair (Nat.pair 0 n);
  if h : p.1 = 0 then S.nat p.2
  else
    have this : p.1 ≤ Nat.pair 0 n := sorry;
    have this := sorry;
    have this := sorry;
    (S.decode (p.1 - 1)).cons (S.decode p.2)) =
  S.nat n
Tactic: unfold S.encode S.decode
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
a b : S
iha : S.decode a.encode = a
ihb : S.decode b.encode = b
⊢ S.decode (a.cons b).encode = a.cons b
have cons : (let p := Nat.unpair (Nat.pair (a.encode + 1) b.encode);
  if h : p.1 = 0 then S.nat p.2
  else
    have this : p.1 ≤ Nat.pair (a.encode + 1) b.encode := sorry;
    have this := sorry;
    have this := sorry;
    (S.decode (p.1 - 1)).cons (S.decode p.2)) =
  a.cons b
Tactic: unfold S.encode S.decode
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
s : S
⊢ S.decode s.encode = s
have nat : ∀ (n : ℕ), S.decode (S.nat n).encode = S.nat n
Tactic: induction s with
    | nat n =>
      unfold S.encode S.decode
      simp
    | cons a b iha ihb =>
      unfold S.encode S.decode
      simp [iha, ihb]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
s : S
nat : ∀ (n : ℕ), S.decode (S.nat n).encode = S.nat n
⊢ S.decode s.encode = s
have cons : ∀ (a b : S) (iha : S.decode a.encode = a) (ihb : S.decode b.encode = b), S.decode (a.cons b).encode = a.cons b
Tactic: induction s with
    | nat n =>
      unfold S.encode S.decode
      simp
    | cons a b iha ihb =>
      unfold S.encode S.decode
      simp [iha, ihb]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
⊢ (S.decode n).encode = n
have ind : S.encode
    (let p := Nat.unpair n;
    if h : p.1 = 0 then S.nat p.2
    else
      have this := sorry;
      have this := sorry;
      have this := sorry;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
  n
Tactic: unfold S.decode
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
⊢ S.encode
      (if h : (Nat.unpair n).1 = 0 then S.nat (Nat.unpair n).2
      else (S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)) =
    n
have ind : (Nat.unpair n).1 = 0 → (S.nat (Nat.unpair n).2).encode = n
Tactic: split
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
ind : (Nat.unpair n).1 = 0 → (S.nat (Nat.unpair n).2).encode = n
⊢ S.encode
      (if h : (Nat.unpair n).1 = 0 then S.nat (Nat.unpair n).2
      else (S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)) =
    n
have ind₁ : ¬(Nat.unpair n).1 = 0 → ((S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)).encode = n
Tactic: split
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ Nat.pair 0 (Nat.unpair n).2 = n
have rw : Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n
Tactic: rw [← h, Nat.pair_unpair]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
rw : Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n
⊢ Nat.pair 0 (Nat.unpair n).2 = n
have rw₁ : n = n
Tactic: rw [← h, Nat.pair_unpair]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ Nat.pair ((S.decode ((Nat.unpair n).1 - 1)).encode + 1) (S.decode (Nat.unpair n).2).encode = n
have rw : 1 ≤ (Nat.unpair n).1
Tactic: rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
rw : 1 ≤ (Nat.unpair n).1
⊢ Nat.pair ((S.decode ((Nat.unpair n).1 - 1)).encode + 1) (S.decode (Nat.unpair n).2).encode = n
have a : (Nat.unpair n).2 < n
Tactic: rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
rw : 1 ≤ (Nat.unpair n).1
a : (Nat.unpair n).2 < n
⊢ Nat.pair ((S.decode ((Nat.unpair n).1 - 1)).encode + 1) (S.decode (Nat.unpair n).2).encode = n
have a₁ : (Nat.unpair n).1 - 1 < n
Tactic: rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ 1 ≤ (Nat.unpair n).1
have rwa : (Nat.unpair n).1 ≠ 0
Tactic: rwa [Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 - 1 < n
have a : ∀ (ih : ∀ m < 0, (S.decode m).encode = m) (h : ¬(Nat.unpair 0).1 = 0), (Nat.unpair 0).1 - 1 < 0
Tactic: obtain _ | n' := n
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
a : ∀ (ih : ∀ m < 0, (S.decode m).encode = m) (h : ¬(Nat.unpair 0).1 = 0), (Nat.unpair 0).1 - 1 < 0
⊢ (Nat.unpair n).1 - 1 < n
have a₁ : ∀ (n' : ℕ) (ih : ∀ m < n' + 1, (S.decode m).encode = m) (h : ¬(Nat.unpair (n' + 1)).1 = 0),
  (Nat.unpair (n' + 1)).1 - 1 < n' + 1
Tactic: obtain _ | n' := n
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (hypothesis)
Goal:
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ (Nat.unpair (n' + 1)).1 - 1 < n' + 1
have this : (Nat.unpair (n' + 1)).1 < n' + 1
Tactic: have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
⊢ (S.decode n).encode = n
have ind : ∀ (n : ℕ) (ih : ∀ m < n, (S.decode m).encode = m), (S.decode n).encode = n
Tactic: induction n using Nat.strongRecOn with | _ n ih =>
    unfold S.decode
    dsimp only
    split
    next h =>
      unfold S.encode
      rw [← h, Nat.pair_unpair]
    next h =>
      unfold S.encode
      rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
      · rwa [Nat.one_le_iff_ne_zero]
      · exact nat_unpair_lt_2 h
      · obtain _ | n' := n
        · exact False.elim (h rfl)
        · have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Tactic.ENatToNat (goal)
Goal:
x : ℕ∞
⊢ ¬⊤ < x
have top : ¬LT.lt (α := ℕ∞) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Tactic.ENatToNat (goal)
Goal:
x : ℕ∞
top : ¬LT.lt (α := ℕ∞) ⊤ ⊤
⊢ ¬⊤ < x
have coe : ∀ (a : ℕ), ¬LT.lt (α := ℕ∞) ⊤ (↑a : ℕ∞)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
have pos : ∀ (ha : a = 0), zpow' a (m + n) = zpow' a m * zpow' a n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
pos : ∀ (ha : a = 0), zpow' a (m + n) = zpow' a m * zpow' a n
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
have neg : ∀ (ha : ¬a = 0), zpow' a (m + n) = zpow' a m * zpow' a n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
have pos : (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
  if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
Tactic: simp [zpow', ha]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
    if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
have pos : ∀ (hn : n = 0),
  (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
    if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
pos :
  ∀ (hn : n = 0),
    (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
      if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
⊢ (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
    if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
have neg : ∀ (hn : ¬n = 0),
  (if m + n = 0 then 0 else HPow.hPow (α := α) 0 (m + n)) =
    if n = 0 then 0 else if m = 0 then 0 else HPow.hPow (α := α) 0 m * HPow.hPow (α := α) 0 n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (zpow' 0 n) 0
have simp : ¬n = 0 → HPow.hPow (α := α) 0 n = 0
Tactic: simp +contextual only [zpow', true_and, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a n = 0 ↔ a = 0
have inl : zpow' a 0 = 0 ↔ a = 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
inl : zpow' a 0 = 0 ↔ a = 0
⊢ zpow' a n = 0 ↔ a = 0
have inr : ∀ (hn : n ≠ 0), zpow' a n = 0 ↔ a = 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0
have inr : (a = 0 → ¬n = 0) ∨ a = 0
Tactic: simp [zpow', zpow_eq_zero_iff hn]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ (a = 0 → ¬n = 0) ∨ a = 0
have inr : ¬(a = 0 → ¬n = 0) → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
inr : ¬(a = 0 → ¬n = 0) → a = 0
⊢ (a = 0 → ¬n = 0) ∨ a = 0
have inr₁ : a = 0 → ¬¬n = 0 → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
⊢ zpow' a 0 = a / a
have simp : (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
Tactic: simp [zpow']
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
⊢ (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
have pos : ∀ (h : a = 0), (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
pos : ∀ (h : a = 0), (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
⊢ (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
have neg : ∀ (h : ¬a = 0), (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a (-n) = (zpow' a n)⁻¹
have simp : if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0
Tactic: simp +contextual [zpow', apply_ite]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
⊢ if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0
have pos : ∀ (h : a = 0 ∧ n = 0), (a = 0 → ¬n = 0) → a ^ n = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
pos : ∀ (h : a = 0 ∧ n = 0), (a = 0 → ¬n = 0) → a ^ n = 0
⊢ if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0
have neg : ∀ (h : ¬(a = 0 ∧ n = 0)), a = 0 → ¬n = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0
have pos : a = 0 → n = 0 → ¬a = 0 → a ^ n = 0
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
pos : a = 0 → n = 0 → ¬a = 0 → a ^ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0
have pos₁ : a = 0 → n = 0 → ¬n = 0 → a ^ n = 0
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0
have neg : a = 0 → ∀ (h : ¬a = 0), ¬n = 0
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
neg : a = 0 → ∀ (h : ¬a = 0), ¬n = 0
⊢ a = 0 → ¬n = 0
have neg₁ : a = 0 → ∀ (h : ¬n = 0), ¬n = 0
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have pos : ∀ (ha : a = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
pos : ∀ (ha : a = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have neg : ∀ (ha : ¬a = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have pos : ∀ (hn : n = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
pos : ∀ (hn : n = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have neg : ∀ (hn : ¬n = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have pos : zpow' a (m * 0) = zpow' (zpow' a m) 0
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have pos : ∀ (hm : m = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
pos : ∀ (hm : m = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have neg : ∀ (hm : ¬m = 0), zpow' a (m * n) = zpow' (zpow' a m) n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
have pos : zpow' a (0 * n) = zpow' (zpow' a 0) n
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a (↑n : ℤ) = a ^ n
have rw : HPow.hPow (β := ℤ) a (↑n : ℤ) = a ^ n
Tactic: rw [zpow'_of_ne_zero_right]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (β := ℤ) a (↑n : ℤ) = a ^ n
⊢ zpow' a (↑n : ℤ) = a ^ n
have hn₁ : Ne (α := ℤ) (↑n : ℤ) 0
Tactic: rw [zpow'_of_ne_zero_right]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
have pos : ∀ (ha : a = 0), zpow' (a * b) n = zpow' a n * zpow' b n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
pos : ∀ (ha : a = 0), zpow' (a * b) n = zpow' a n * zpow' b n
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
have neg : ∀ (ha : ¬a = 0), zpow' (a * b) n = zpow' a n * zpow' b n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
have pos : ∀ (hb : b = 0), zpow' (a * b) n = zpow' a n * zpow' b n
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
pos : ∀ (hb : b = 0), zpow' (a * b) n = zpow' a n * zpow' b n
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
have neg : ∀ (hb : ¬b = 0), zpow' (a * b) n = zpow' a n * zpow' b n
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Semiring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ + X₂ = Y
hy : a * Y = y
⊢ x₁ + x₂ = y
have subst : a * X₁ + a * X₂ = a * (X₁ + X₂)
Tactic: subst h₁ h₂ H_atom hy
Cleared hypotheses: x₁, x₂, Y, y, h₁, h₂, H_atom, hy
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Ring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ - X₂ = Y
hy : a * Y = y
⊢ x₁ - x₂ = y
have subst : a * X₁ - a * X₂ = a * (X₁ - X₂)
Tactic: subst h₁ h₂ H_atom hy
Cleared hypotheses: x₁, x₂, Y, y, h₁, h₂, H_atom, hy
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
⊢ l = n
have rw : l_n / 1 = n
Tactic: rw [h, hn, div_one]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
rw : l_n / 1 = n
⊢ l = n
have rw₁ : n / 1 = n
Tactic: rw [h, hn, div_one]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
rw : l_n / 1 = n
rw₁ : n / 1 = n
⊢ l = n
have rw₂ : n = n
Tactic: rw [h, hn, div_one]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_d d : M
h : l = 1 / l_d
hn : l_d = d
⊢ l = d⁻¹
have rw : 1 / l_d = d⁻¹
Tactic: rw [h, hn, one_div]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_d d : M
h : l = 1 / l_d
hn : l_d = d
rw : 1 / l_d = d⁻¹
⊢ l = d⁻¹
have rw₁ : 1 / d = d⁻¹
Tactic: rw [h, hn, one_div]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_d d : M
h : l = 1 / l_d
hn : l_d = d
rw : 1 / l_d = d⁻¹
rw₁ : 1 / d = d⁻¹
⊢ l = d⁻¹
have rw₂ : d⁻¹ = d⁻¹
Tactic: rw [h, hn, one_div]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
⊢ l = n / d
have rw : l_n / l_d = n / d
Tactic: rw [h, hn, hd]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
rw : l_n / l_d = n / d
⊢ l = n / d
have rw₁ : n / l_d = n / d
Tactic: rw [h, hn, hd]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
rw : l_n / l_d = n / d
rw₁ : n / l_d = n / d
⊢ l = n / d
have rw₂ : n / d = n / d
Tactic: rw [h, hn, hd]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ a = D * f
have rw : b = D * f
Tactic: rw [h₁, h₂, h₃, h₄]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
rw : b = D * f
⊢ a = D * f
have rw₁ : c = D * f
Tactic: rw [h₁, h₂, h₃, h₄]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
rw : b = D * f
rw₁ : c = D * f
⊢ a = D * f
have rw₂ : D * e = D * f
Tactic: rw [h₁, h₂, h₃, h₄]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
rw : b = D * f
rw₁ : c = D * f
rw₂ : D * e = D * f
⊢ a = D * f
have rw₃ : D * f = D * f
Tactic: rw [h₁, h₂, h₃, h₄]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : L ≠ 0
⊢ (e₁ = e₂) = (f₁ = f₂)
have subst : (L * f₁ = L * f₂) = (f₁ = f₂)
Tactic: subst H₁ H₂
Cleared hypotheses: e₁, e₂, H₁, H₂
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
⊢ (L * f₁ = L * f₂) = (f₁ = f₂)
have rw : (f₁ = f₂) = (f₁ = f₂)
Tactic: rw [mul_right_inj' HL]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ ≤ e₂) = (f₁ ≤ f₂)
have subst : (L * f₁ ≤ L * f₂) = (f₁ ≤ f₂)
Tactic: subst H₁ H₂
Cleared hypotheses: e₁, e₂, H₁, H₂
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
f₁ f₂ L : M
HL : 0 < L
⊢ (L * f₁ ≤ L * f₂) = (f₁ ≤ f₂)
have a : L * f₁ ≤ L * f₂ ↔ f₁ ≤ f₂
Tactic: apply Iff.eq
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ < e₂) = (f₁ < f₂)
have subst : (L * f₁ < L * f₂) = (f₁ < f₂)
Tactic: subst H₁ H₂
Cleared hypotheses: e₁, e₂, H₁, H₂
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
f₁ f₂ L : M
HL : 0 < L
⊢ (L * f₁ < L * f₂) = (f₁ < f₂)
have a : L * f₁ < L * f₂ ↔ f₁ < f₂
Tactic: apply Iff.eq
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ (p ::ᵣ l).eval = l.eval * zpow' p.2 p.1
have unfold : prod
    (map
      (fun (x : ℤ × M) ↦
        match (motive := ℤ × M → M) x with
        | (r, x) => zpow' x r)
      (p :: l)) =
  prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        l) *
    zpow' p.2 p.1
Tactic: unfold eval cons