awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α : Sort u_1
x : α
p : x ≍ x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯

Tactic:
h rfl

Premises used: rfl
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
α : Sort u_1
x : α
p : x ≍ x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯

Tactic:
exact h rfl

Premises used: rfl
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
refl : ∀ {p : x = x → Prop} (h : ∀ (he : x ↔ x), p ⋯), p ⋯
⊢ p he

Tactic:
cases he
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯

Tactic:
h Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Tactic.CongrExclamation
Goal:
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯

Tactic:
exact h Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (¬q → ¬p) → p → q

Tactic:
fun h hp ↦ by_contra fun h' ↦ h h' hp

Premises used: by_contra
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (¬q → p) → ¬p → q

Tactic:
fun h hp ↦ by_contra fun h' ↦ hp (h h')

Premises used: by_contra
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (q → ¬p) → p → ¬q

Tactic:
Imp.swap.mp

Premises used: Iff.mp, Not, Imp.swap
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (q → p) → ¬p → ¬q

Tactic:
mt

Premises used: mt
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (¬p ↔ ¬q) → (p ↔ q)

Tactic:
not_iff_not.mp

Premises used: not_iff_not, Iff.mp
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (p ↔ ¬q) → (¬p ↔ q)

Tactic:
(iff_not_comm.trans Iff.comm).mp

Premises used: iff_not_comm, Iff.mp, Iff.trans, Iff.comm
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (¬p ↔ q) → (p ↔ ¬q)

Tactic:
(not_iff_comm.trans Iff.comm).mp

Premises used: Iff.mp, Iff.trans, Iff.comm, not_iff_comm
-- Module: Mathlib.Tactic.Contrapose
Goal:
p q : Prop
⊢ (p ↔ q) → (¬p ↔ ¬q)

Tactic:
fun ⟨h₁, h₂⟩ ↦ ⟨mt h₂, mt h₁⟩

Premises used: mt, Iff, _private.0.Mathlib.Tactic.Contrapose.contrapose_iff₄.match_1, Iff.intro, Not
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
refl : f a ⋯ = Eq.rec (motive := fun (x : α) (h' : a = x) ↦ β x ⋯) (f a ⋯) ⋯
⊢ Eq (α := β a ⋯) (f a ⋯) (Eq.rec (motive := fun (x : α) (h' : a' = x) ↦ β x ⋯) (f a' h) ⋯)

Tactic:
cases h
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = Eq.rec (motive := fun (x : α) (h' : a = x) ↦ β x ⋯) (f a ⋯) ⋯

Tactic:
rfl
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a a' : α
β : Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β
refl : f a ⋯ = f a ⋯
⊢ f a ⋯ = f a' h

Tactic:
cases h
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a : α
β : Sort v
f : (a' : α) → (h : a = a') → β
⊢ f a ⋯ = f a ⋯

Tactic:
rfl
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α β : Sort u
a : α
b : β
h : a ≍ b
refl : a = cast ⋯ a
⊢ a = cast ⋯ b

Tactic:
cases h
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a : α
⊢ a = cast ⋯ a

Tactic:
rfl
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α β : Sort u
a : α
b : β
h : a ≍ b
refl : cast ⋯ a = a
⊢ cast ⋯ a = b

Tactic:
cases h
-- Module: Mathlib.Tactic.DepRewrite
Goal:
α : Sort u
a : α
⊢ cast ⋯ a = a

Tactic:
rfl
-- Module: Mathlib.Tactic.DeriveCountable
Goal:
α : Sort u_1
inst : Countable α
⊢ Function.Injective.{u_1, 1} (α := α) encode

Tactic:
(Countable.exists_injective_nat α).choose_spec

Premises used: Exists.choose_spec, Countable.exists_injective_nat, Mathlib.Deriving.Countable.encode
-- Module: Mathlib.Tactic.DeriveCountable
Goal:
p : Prop
a b b' : ℕ
h : b = b' → p
⊢ Nat.pair a b = Nat.pair a b' → p

Tactic:
simpa [Nat.pair_eq_pair, and_imp] using h

Premises used: and_imp, Nat.pair_eq_pair
-- Module: Mathlib.Tactic.DeriveCountable
Goal:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
rwa : a = a' ∧ b = b' → p
rwa₁ rwa₂ rwa₃ rwa₄ : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p

Tactic:
rwa [Nat.pair_eq_pair, and_imp]

Premises used: and_imp, Nat.pair_eq_pair
-- Module: Mathlib.Tactic.DeriveCountable
Goal:
p : Prop
α : Sort u_1
inst : Countable α
a b : α
m n : ℕ
h : a = b → m = n → p
⊢ Nat.pair (encode a) m = Nat.pair (encode b) n → p

Tactic:
cons_eq_imp fun ha => h (encode_injective ha)

Premises used: Mathlib.Deriving.Countable.encode_injective, Mathlib.Deriving.Countable.cons_eq_imp
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
h : (Nat.unpair n).1 ≠ 0
obtain :
  ∀ (a b : ℕ) (h : (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).1 ≠ 0),
    (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).2 < (Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b)
⊢ (Nat.unpair n).2 < n

Tactic:
obtain ⟨⟨a, b⟩, rfl⟩ := Nat.pairEquiv.surjective n

Premises used: Equiv.surjective, Nat.pairEquiv, rfl
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).1 ≠ 0
simp : ∀ (h : a ≠ 0), b < Nat.pair a b
⊢ (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).2 < (Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b)

Tactic:
simp only [Nat.pairEquiv_apply, Function.uncurry_apply_pair, Nat.unpair_pair] at *

Premises used: Nat.pairEquiv_apply, Nat.unpair_pair, Function.uncurry_apply_pair
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : a ≠ 0
⊢ a ≤ a * a

Tactic:
have := Nat.le_mul_self a
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : a ≠ 0
this : a ≤ a * a
⊢ b ≤ b * b

Tactic:
have := Nat.le_mul_self b
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : a ≠ 0
this_1 : a ≤ a * a
this : b ≤ b * b
isTrue : a < b → b < b * b + a
isFalse : ¬a < b → b < a * a + a + b
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
split
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : a ≠ 0
this_1 : a ≤ a * a
this : b ≤ b * b
h_1 : a < b
⊢ b < b * b + a

Tactic:
lia
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : ℕ
h : a ≠ 0
this_1 : a ≤ a * a
this : b ≤ b * b
h_1 : ¬a < b
⊢ b < a * a + a + b

Tactic:
lia
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
p : ℕ × ℕ := Nat.unpair n
h : ¬p.1 = 0
this : p.1 ≤ n
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
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 := ⋯;
      have this := ⋯;
      have this := ⋯;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    S.nat n
⊢ S.decode (S.nat n).encode = S.nat n

Tactic:
unfold S.encode S.decode

Premises used: _private.0.Mathlib.Deriving.Encodable.S.encode, _private.0.Mathlib.Deriving.Encodable.S.decode
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
⊢ (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 := ⋯;
      have this := ⋯;
      have this := ⋯;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    S.nat n

Tactic:
simp
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : S
iha : S.decode a.encode = a
ihb : S.decode b.encode = b
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 := ⋯;
      have this := ⋯;
      have this := ⋯;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    a.cons b
⊢ S.decode (a.cons b).encode = a.cons b

Tactic:
unfold S.encode S.decode

Premises used: _private.0.Mathlib.Deriving.Encodable.S.encode, _private.0.Mathlib.Deriving.Encodable.S.decode
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
a b : S
iha : S.decode a.encode = a
ihb : S.decode b.encode = b
⊢ (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 := ⋯;
      have this := ⋯;
      have this := ⋯;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    a.cons b

Tactic:
simp [iha, ihb]
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
s : S
nat : ∀ (n : ℕ), S.decode (S.nat n).encode = S.nat n
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
⊢ S.decode s.encode = s

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]

Premises used: _private.0.Mathlib.Deriving.Encodable.S.encode, _private.0.Mathlib.Deriving.Encodable.S.decode
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
ind :
  S.encode
      (let p := Nat.unpair n;
      if h : p.1 = 0 then S.nat p.2
      else
        have this := ⋯;
        have this := ⋯;
        have this := ⋯;
        (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    n
⊢ (S.decode n).encode = n

Tactic:
unfold S.decode

Premises used: _private.0.Mathlib.Deriving.Encodable.S.decode
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
ind : (Nat.unpair n).1 = 0 → (S.nat (Nat.unpair n).2).encode = n
ind₁ : ¬(Nat.unpair n).1 = 0 → ((S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (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

Tactic:
split
-- Module: Mathlib.Tactic.DeriveEncodable
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
rw₁ rw₂ : n = n
⊢ Nat.pair 0 (Nat.unpair n).2 = n

Tactic:
rw [← h, Nat.pair_unpair]

Premises used: Nat.pair_unpair
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ (S.nat (Nat.unpair n).2).encode = n

Tactic:
next h =>
      unfold S.encode
      rw [← h, Nat.pair_unpair]

Premises used: Nat.pair_unpair, _private.0.Mathlib.Deriving.Encodable.S.encode
-- Module: Mathlib.Tactic.DeriveEncodable
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
a₁ : (Nat.unpair n).1 - 1 < n
⊢ Nat.pair ((S.decode ((Nat.unpair n).1 - 1)).encode + 1) (S.decode (Nat.unpair n).2).encode = n

Tactic:
rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]

Premises used: Nat.sub_add_cancel, Nat.pair_unpair
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
rwa rwa₁ rwa₂ rwa₃ : (Nat.unpair n).1 ≠ 0
⊢ 1 ≤ (Nat.unpair n).1

Tactic:
rwa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).2 < n

Tactic:
nat_unpair_lt_2 h

Premises used: _private.0.Mathlib.Deriving.Encodable.nat_unpair_lt_2
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).2 < n

Tactic:
exact nat_unpair_lt_2 h

Premises used: _private.0.Mathlib.Deriving.Encodable.nat_unpair_lt_2
-- Module: Mathlib.Tactic.DeriveEncodable
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
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
⊢ (Nat.unpair n).1 - 1 < n

Tactic:
obtain _ | n' := n
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
ih : ∀ m < 0, (S.decode m).encode = m
h : ¬(Nat.unpair 0).1 = 0
⊢ (Nat.unpair 0).1 - 1 < 0

Tactic:
False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
ih : ∀ m < 0, (S.decode m).encode = m
h : ¬(Nat.unpair 0).1 = 0
⊢ (Nat.unpair 0).1 - 1 < 0

Tactic:
exact False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ 1 ≤ n' + 1

Tactic:
lia
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ (Nat.unpair (n' + 1)).1 < n' + 1

Tactic:
have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
this : (Nat.unpair (n' + 1)).1 < n' + 1
⊢ (Nat.unpair (n' + 1)).1 - 1 < n' + 1

Tactic:
lia
-- Module: Mathlib.Tactic.DeriveEncodable
Goal:
n : ℕ
ind : ∀ (n : ℕ) (ih : ∀ m < n, (S.decode m).encode = m), (S.decode n).encode = n
⊢ (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

Premises used: Nat.sub_add_cancel, Nat.pair_unpair, _private.0.Mathlib.Deriving.Encodable.S.encode, Nat.one_le_iff_ne_zero, _private.0.Mathlib.Deriving.Encodable.S.decode
-- Module: Mathlib.Tactic.ENatToNat
Goal:
x : ℕ∞
top : ¬LT.lt (α := ℕ∞) ⊤ ⊤
coe : ∀ (a : ℕ), ¬LT.lt (α := ℕ∞) ⊤ (↑a : ℕ∞)
⊢ ¬⊤ < x

Tactic:
cases x
-- Module: Mathlib.Tactic.ENatToNat
Goal:
⊢ ¬LT.lt (α := ℕ∞) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Tactic.ENatToNat
Goal:
a : ℕ
⊢ ¬LT.lt (α := ℕ∞) ⊤ (↑a : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Tactic.ENatToNat
Goal:
m n : ℕ
⊢ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) = (↑(m + n) : ℕ∞)

Tactic:
rfl

Premises used: WithTop.map₂, WithTop.some, rfl, Option.map₂
-- Module: Mathlib.Tactic.ENatToNat
Goal:
m n : ℕ
⊢ HSub.hSub (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) = (↑(m - n) : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, WithTop.sub, rfl
-- Module: Mathlib.Tactic.ENatToNat
Goal:
m n : ℕ
⊢ HMul.hMul (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) = (↑(m * n) : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Tactic.ENatToNat
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ∞) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℕ∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.ENatToNat
Goal:
⊢ Eq (α := ℕ∞) 0 (↑0 : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Tactic.ENatToNat
Goal:
⊢ Eq (α := ℕ∞) 1 (↑1 : ℕ∞)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
pos : ∀ (ha : a = 0), zpow' a (m + n) = zpow' a m * zpow' a n
neg : ∀ (ha : ¬a = 0), zpow' a (m + n) = zpow' a m * zpow' a n
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
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
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
simp [zpow', ha]

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
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
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
⊢ (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
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
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:
simp +contextual [hn, zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
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:
simp +contextual [hn, zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
simp [zpow', ha, zpow_add₀]

Premises used: zpow_add₀, Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = a ^ n

Tactic:
simp [zpow', hn]

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
ha : a ≠ 0
⊢ zpow' a n = a ^ n

Tactic:
simp [zpow', ha]

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
n : ℤ
simp : ¬n = 0 → HPow.hPow (α := α) 0 n = 0
⊢ Eq.{u_1 + 1} (α := α) (zpow' 0 n) 0

Tactic:
simp +contextual only [zpow', true_and, ite_eq_left_iff]

Premises used: ite_eq_left_iff, Mathlib.Tactic.FieldSimp.zpow', true_and
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
n : ℤ
hn : ¬n = 0
⊢ HPow.hPow (α := α) 0 n = 0

Tactic:
zero_zpow n hn

Premises used: zero_zpow
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
n : ℤ
hn : ¬n = 0
⊢ HPow.hPow (α := α) 0 n = 0

Tactic:
exact zero_zpow n hn

Premises used: zero_zpow
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
inl : zpow' a 0 = 0 ↔ a = 0
inr : ∀ (hn : n ≠ 0), zpow' a n = 0 ↔ a = 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
⊢ zpow' a 0 = 0 ↔ a = 0

Tactic:
simp [zpow']

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
inr : (a = 0 → ¬n = 0) ∨ a = 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
simp [zpow', zpow_eq_zero_iff hn]

Premises used: zpow_eq_zero_iff, Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
inr : ¬(a = 0 → ¬n = 0) → a = 0
inr₁ : a = 0 → ¬¬n = 0 → a = 0
⊢ (a = 0 → ¬n = 0) ∨ a = 0

Tactic:
tauto
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (zpow' 1 n) 1

Tactic:
simp [zpow']

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
⊢ zpow' a 1 = a

Tactic:
simp [zpow']

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
simp : (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
⊢ zpow' a 0 = a / a

Tactic:
simp [zpow']

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
pos : ∀ (h : a = 0), (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a
neg : ∀ (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

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
h : a = 0
⊢ (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a

Tactic:
simp [h]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ Eq (α := ℤ) 0 0 then 0 else 1) = a / a

Tactic:
simp [h]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
ha : a ≠ 0
⊢ zpow' a 0 = 1

Tactic:
simp [zpow', ha]

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
simp : if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0
⊢ zpow' a (-n) = (zpow' a n)⁻¹

Tactic:
simp +contextual [zpow', apply_ite]

Premises used: apply_ite, Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
pos : ∀ (h : a = 0 ∧ n = 0), (a = 0 → ¬n = 0) → a ^ n = 0
neg : ∀ (h : ¬(a = 0 ∧ n = 0)), a = 0 → ¬n = 0
⊢ if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0

Tactic:
split_ifs with h
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
pos : a = 0 → n = 0 → ¬a = 0 → a ^ n = 0
pos₁ : a = 0 → n = 0 → ¬n = 0 → a ^ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0

Tactic:
tauto
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
neg : a = 0 → ∀ (h : ¬a = 0), ¬n = 0
neg₁ neg₂ : a = 0 → ∀ (h : ¬n = 0), ¬n = 0
neg₃ neg₄ : a = 0 → ∀ (h : ¬n = 0), n = 0 → False
⊢ a = 0 → ¬n = 0

Tactic:
tauto
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
pos : ∀ (ha : a = 0), zpow' a (m * n) = zpow' (zpow' a m) n
neg : ∀ (ha : ¬a = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
simp [ha]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
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
neg : ∀ (hn : ¬n = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
pos : zpow' a (m * 0) = zpow' (zpow' a m) 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
rw [hn]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * 0) = zpow' (zpow' a m) 0

Tactic:
simp [zpow', ha, zpow_ne_zero ]

Premises used: Mathlib.Tactic.FieldSimp.zpow', zpow_ne_zero
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
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
neg : ∀ (hm : ¬m = 0), zpow' a (m * n) = zpow' (zpow' a m) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
pos : zpow' a (0 * n) = zpow' (zpow' a 0) n
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
rw [hm]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (0 * n) = zpow' (zpow' a 0) n

Tactic:
simp [zpow', ha]

Premises used: Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
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

Tactic:
simpa [zpow', ha, hm, hn] using zpow_mul a m n

Premises used: zpow_mul, Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (β := ℤ) a (↑n : ℤ) = a ^ n
hn₁ : Ne (α := ℤ) (↑n : ℤ) 0
⊢ zpow' a (↑n : ℤ) = a ^ n

Tactic:
rw [zpow'_of_ne_zero_right]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℤ) a (↑n : ℤ) = a ^ n

Tactic:
simp
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ Ne (α := ℤ) (↑n : ℤ) 0

Tactic:
exact_mod_cast hn