awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left : k < n
j : ℤ
hj : a - b = (j * (↑n : ℤ) + (↑k : ℤ)) • p
mpr : ∃ (m : ℤ), (j * (↑n : ℤ) + (↑k : ℤ)) • p = m • p
⊢ ∃ (m : ℤ), a - b = m • p

Tactic:
rw [hj]
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left : k < n
j : ℤ
hj : a - b = (j * (↑n : ℤ) + (↑k : ℤ)) • p
⊢ ∃ (m : ℤ), (j * (↑n : ℤ) + (↑k : ℤ)) • p = m • p

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left : k < n
j : ℤ
hj : a - b = (j * (↑n : ℤ) + (↑k : ℤ)) • p
⊢ ∃ (m : ℤ), (j * (↑n : ℤ) + (↑k : ℤ)) • p = m • p

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ AddCommMonoid ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ AddMonoid ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ Monoid ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ CommSemigroup ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ Semigroup ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ AddCommSemigroup ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
⊢ AddSemigroup ℕ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Nat.Defs
Goal:
m n : ℕ
⊢ m • n = m * n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
h : Even n
m : ℕ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
simp [← Nat.two_mul, hm]

Premises used: Nat.two_mul
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m_1 n m : ℕ
simp_rw : IsSquare m ↔ ∃ (n : ℕ), n * n = m
simp_rw₁ : (∃ (r : ℕ), m = r * r) ↔ ∃ (n : ℕ), n * n = m
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]

Premises used: Nat.exists_mul_self, eq_comm, IsSquare
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
⊢ ¬Even (α := ℕ) 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m : ℕ
⊢ (m + 1) % 2 = 0 ↔ m % 2 = 1

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m : ℕ
⊢ (m + 1) % 2 = 1 ↔ m % 2 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ 0 < n → ¬2 ∣ 2 * n - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inr : ∀ (h₁ : m % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁

Premises used: Nat.mod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 0
inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inl₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one n with h₂ | h₂

Premises used: Nat.mod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 1
inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inr₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one n with h₂ | h₂

Premises used: Nat.mod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

Premises used: Nat.mul_mod, Nat.even_iff
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

Premises used: Nat.mul_mod, Nat.even_iff
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

Premises used: Nat.mul_mod, Nat.even_iff
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

Premises used: Nat.mul_mod, Nat.even_iff
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
⊢ Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n n_1 : ℕ
h : Even (m ^ n_1) ↔ Even m ∧ n_1 ≠ 0
⊢ Even (m ^ (n_1 + 1)) ↔ Even m ∧ n_1 + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
succ : ∀ (n : ℕ), (Even (m ^ n) ↔ Even m ∧ n ≠ 0) → (Even (m ^ (n + 1)) ↔ Even m ∧ n + 1 ≠ 0)
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ Even (n * (n + 1))

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ Even (n * (n - 1))

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ Even n → 2 * (n / 2) = n

Tactic:
fun h ↦
  Nat.mul_div_cancel_left' ((even_iff_exists_two_nsmul _).1 h)

Premises used: even_iff_exists_two_nsmul, Nat.mul_div_cancel_left', Iff.mp
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
⊢ Even n → n / 2 * 2 = n

Tactic:
fun h ↦ Nat.div_mul_cancel ((even_iff_exists_two_nsmul _).1 h)

Premises used: Nat.div_mul_cancel, even_iff_exists_two_nsmul, Iff.mp
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ 1 < n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
hn : Even n
hm : Even m
hnm : n < m
⊢ n + 1 < m

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m_1 n_1 m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (HPow.hPow (β := ℕ) m 2 + m + n)

Tactic:
simp [*, parity_simps]
-- Module: Mathlib.Algebra.Group.Nat.Even
Goal:
m n : ℕ
⊢ ¬Even (α := ℕ) 25394535

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
zero : Eq.{u_2 + 1} (α := A) (0 : A) ((g : (a : ℕ) → A) 0 : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)

Tactic:
simp_rw [map_zero f, map_zero g]

Premises used: map_zero
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
n : ℕ
ihn : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((g : (a : ℕ) → A) (n + 1) : A)

Tactic:
simp [h, ihn]
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
n : ℕ
zero : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)
succ :
  ∀ (n : ℕ) (ihn : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)),
    Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((g : (a : ℕ) → A) (n + 1) : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)

Tactic:
induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]

Premises used: map_zero
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
A : Type u_2
inst : AddZeroClass A
f g : ℕ →+ A
⊢ Eq (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A) → f = g

Tactic:
ext_nat' f g

Premises used: ext_nat'
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddMonoid M
x : M
n : ℕ
⊢ (((multiplesHom M : (a : M) → ℕ →+ M) x : ℕ →+ M) : (a : ℕ) → M) n = n • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddMonoid M
f : ℕ →+ M
⊢ Eq (α := M) ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f : M) ((f : (a : ℕ) → M) 1 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddMonoid M
f : ℕ →+ M
n : ℕ
rw : (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f : M)
rw₁ :
  Eq (α := M) ((f : (a : ℕ) → M) n : M)
    ((((multiplesHom M : (a : M) → ℕ →+ M) ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f) : ℕ →+ M) : (a : ℕ) → M)
        n :
      M)
rw₂ rw₃ : Eq (α := M) ((f : (a : ℕ) → M) n : M) ((f : (a : ℕ) → M) n : M)
⊢ (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((f : (a : ℕ) → M) 1 : M)

Tactic:
rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, multiplesHom_symm_apply, multiplesHom_apply
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : Monoid M
x : M
n : Multiplicative ℕ
⊢ (((powersHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (β := ℕ) x ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : Monoid M
f : Multiplicative ℕ →* M
⊢ Eq (α := M) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
    ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
rw :
  (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
rw₁ :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M)
    ((((powersHom M : (a : M) → Multiplicative ℕ →* M)
              ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f) :
            Multiplicative ℕ →* M) :
          (a : Multiplicative ℕ) → M)
        n :
      M)
rw₂ rw₃ : Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((f : (a : Multiplicative ℕ) → M) n : M)
⊢ (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)

Tactic:
rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, powersHom_symm_apply, powersHom_apply
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : Monoid M
f g : Multiplicative ℕ →* M
h :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
n : Multiplicative ℕ
rw :
  HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    (g : (a : Multiplicative ℕ) → M) n
rw₁ :
  HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    HPow.hPow (α := M) (β := ℕ)
      ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
rw₂ rw₃ :
  HPow.hPow (α := M) (β := ℕ)
      ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    HPow.hPow (α := M) (β := ℕ)
      ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
⊢ Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((g : (a : Multiplicative ℕ) → M) n : M)

Tactic:
rw [f.apply_mnat, g.apply_mnat, h]

Premises used: MonoidHom.apply_mnat
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddCommMonoid M
a b : M
n : ℕ
⊢ Eq (α := M) ((Equiv.toFun (multiplesHom M) (a + b) : (a : ℕ) → M) n : M)
    ((HAdd.hAdd (α := ℕ →+ M) (Equiv.toFun (multiplesHom M) a) (Equiv.toFun (multiplesHom M) b) : (a : ℕ) → M) n : M)

Tactic:
simp [nsmul_add]

Premises used: nsmul_add
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddCommMonoid M
x : M
n : ℕ
⊢ (((multiplesAddHom M : (a : M) → ℕ →+ M) x : ℕ →+ M) : (a : ℕ) → M) n = n • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : AddCommMonoid M
f : ℕ →+ M
⊢ Eq (α := M) ((AddEquiv.symm (multiplesAddHom M) : (a : ℕ →+ M) → M) f : M) ((f : (a : ℕ) → M) 1 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
n : Multiplicative ℕ
⊢ Eq (α := M) ((Equiv.toFun (powersHom M) (a * b) : (a : Multiplicative ℕ) → M) n : M)
    ((HMul.hMul (α := Multiplicative ℕ →* M) (Equiv.toFun (powersHom M) a) (Equiv.toFun (powersHom M) b) :
          (a : Multiplicative ℕ) → M)
        n :
      M)

Tactic:
simp [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : CommMonoid M
x : M
n : Multiplicative ℕ
⊢ (((powersMulHom M : (a : M) → Multiplicative ℕ →* M) x : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (β := ℕ) x ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Hom
Goal:
M : Type u_1
inst : CommMonoid M
f : Multiplicative ℕ →* M
⊢ Eq (α := M) ((MulEquiv.symm (powersMulHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
    ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a : ℕ
s : Finset ℕ
simp_rw : ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
simp_rw [disjoint_left, mem_map, mem_range, addLeftEmbedding_apply]

Premises used: addLeftEmbedding_apply, Finset.mem_range, Finset.disjoint_left, Finset.mem_map
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a : ℕ
s : Finset ℕ
l : ℕ
h : a + l < a
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a : ℕ
s : Finset ℕ
rw : Disjoint (range a) (map (addLeftEmbedding a) s)
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
rw [← addLeftEmbedding_eq_addRightEmbedding]

Premises used: addLeftEmbedding_eq_addRightEmbedding
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
apply disjoint_range_addLeftEmbedding

Premises used: Finset.disjoint_range_addLeftEmbedding
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a b : ℕ
rw : (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
rw [← val_inj, union_val]

Premises used: Finset.union_val, Finset.val_inj
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val

Tactic:
Multiset.range_add_eq_union a b

Premises used: Multiset.range_add_eq_union, Multiset.map, Multiset.ofList, Multiset.range
-- Module: Mathlib.Algebra.Group.Nat.Range
Goal:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val

Tactic:
exact Multiset.range_add_eq_union a b

Premises used: Multiset.range_add_eq_union
-- Module: Mathlib.Algebra.Group.Nat.TypeTags
Goal:
a : Multiplicative ℕ
b : ℕ
⊢ (toAdd : (a : Multiplicative ℕ) → ℕ) (a ^ b) = HMul.hMul (α := ℕ) ((toAdd : (a : Multiplicative ℕ) → ℕ) a : ℕ) b

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Nat.TypeTags
Goal:
a b : ℕ
⊢ (ofAdd : (a : ℕ) → Multiplicative ℕ) (a * b) =
    HPow.hPow (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) a : Multiplicative ℕ) b

Tactic:
(toAdd_pow _ _).symm

Premises used: Multiplicative, Nat.toAdd_pow, Eq.symm
-- Module: Mathlib.Algebra.Group.Nat.Units
Goal:
u : ℕˣ
⊢ u = 1

Tactic:
Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩

Premises used: Units.ext, Exists.intro, Units.inv, Eq.symm, Units.val_inv, Nat.eq_one_of_dvd_one
-- Module: Mathlib.Algebra.Group.Nat.Units
Goal:
u : AddUnits ℕ
⊢ u = 0

Tactic:
AddUnits.ext <| (Nat.eq_zero_of_add_eq_zero u.val_neg).1

Premises used: AddUnits.val_neg, Nat.eq_zero_of_add_eq_zero, AddUnits.ext, And.left
-- Module: Mathlib.Algebra.Group.Nat.Units
Goal:
n : ℕ
⊢ IsUnit n ↔ n = 1

Tactic:
isUnit_iff_eq_one

Premises used: isUnit_iff_eq_one
-- Module: Mathlib.Algebra.Group.Nat.Units
Goal:
n : ℕ
⊢ IsAddUnit n ↔ n = 0

Tactic:
isAddUnit_iff_eq_zero

Premises used: isAddUnit_iff_eq_zero
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
k n : ℕ
x : M
⊢ x ^ (k + n) = x ^ k * x ^ n

Tactic:
NatPowAssoc.npow_add k n x

Premises used: NatPowAssoc.npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
⊢ HPow.hPow (β := ℕ) x 0 = 1

Tactic:
NatPowAssoc.npow_zero x

Premises used: NatPowAssoc.npow_zero
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
⊢ HPow.hPow (β := ℕ) x 1 = x

Tactic:
NatPowAssoc.npow_one x

Premises used: NatPowAssoc.npow_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
k m n : ℕ
x : M
⊢ x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

Tactic:
simp only [← npow_add, add_assoc]

Premises used: add_assoc, npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
m n : ℕ
x : M
⊢ x ^ m * x ^ n = x ^ n * x ^ m

Tactic:
simp only [← npow_add, add_comm]

Premises used: add_comm, npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m : ℕ
zero : x ^ (m * 0) = 1
zero₁ : HPow.hPow (β := ℕ) x 0 = 1
zero₂ zero₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0

Tactic:
rw [npow_zero, mul_zero, npow_zero]

Premises used: npow_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₂ : (x ^ m) ^ n * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₃ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ (n + 1)
succ₄ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * HPow.hPow (β := ℕ) (x ^ m) 1
succ₅ succ₆ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * x ^ m
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)

Tactic:
rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

Premises used: npow_one, npow_add, mul_add, mul_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
zero : x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
succ : ∀ (n : ℕ) (ih : x ^ (m * n) = (x ^ m) ^ n), x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
induction n with
  | zero => rw [npow_zero, mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

Premises used: npow_one, npow_zero, MulZeroClass.mul_zero, npow_add, mul_add, mul_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
rw : x ^ (n * m) = (x ^ n) ^ m
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
npow_mul x n m

Premises used: npow_mul
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
exact npow_mul x n m

Premises used: npow_mul
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
⊢ HPow.hPow (α := R) (β := ℕ) (-1) 0 * a * b = HPow.hPow (α := R) (β := ℕ) (-1) 0 * (a * b)

Tactic:
simp only [npow_zero, one_mul]

Premises used: npow_zero, one_mul
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
ih : HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)
succ : -HPow.hPow (α := R) (-1) k * a * b = -HPow.hPow (α := R) (-1) k * (a * b)
⊢ HPow.hPow (α := R) (-1) (k + 1) * a * b = HPow.hPow (α := R) (-1) (k + 1) * (a * b)

Tactic:
rw [npow_add, npow_one, ← neg_mul_comm, mul_one]

Premises used: npow_one, npow_add, neg_mul_comm, mul_one
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
ih : HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)
⊢ -HPow.hPow (α := R) (-1) k * a * b = -HPow.hPow (α := R) (-1) k * (a * b)

Tactic:
simp only [neg_mul, ih]

Premises used: neg_mul
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
zero : HPow.hPow (α := R) (β := ℕ) (-1) 0 * a * b = HPow.hPow (α := R) (β := ℕ) (-1) 0 * (a * b)
succ :
  ∀ (k : ℕ) (ih : HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)),
    HPow.hPow (α := R) (-1) (k + 1) * a * b = HPow.hPow (α := R) (-1) (k + 1) * (a * b)
⊢ HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)

Tactic:
induction k with
  | zero => simp only [npow_zero, one_mul]
  | succ k ih =>
    rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
    simp only [neg_mul, ih]

Premises used: npow_one, npow_zero, npow_add, neg_mul_comm, neg_mul, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x x_1 : ℕ
x_2 : (i : ι) → α i
h : ∀ (x_3 : ι), (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x x_1 : ℕ
x_2 : (i : ι) → α i
x_3 : ι
⊢ (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3

Tactic:
simp [npow_add]

Premises used: npow_add
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
h : ∀ (x_1 : ι), HPow.hPow (β := ℕ) x 0 x_1 = 1 x_1
⊢ HPow.hPow (β := ℕ) x 0 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.NatPowAssoc
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
x_1 : ι
⊢ HPow.hPow (β := ℕ) x 0 x_1 = 1 x_1

Tactic:
simp