awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(-(↑n : ℤ)) : R) (if Even (α := ℤ) (-(↑n : ℤ)) then 0 else 1)

Tactic:
simpa using natCast_eq_ite n

Premises used: CharTwo.natCast_eq_ite
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
hp : ∃ (a : ℤ), Even a
hn : ∃ (a : ℤ), ¬Even a
⊢ Eq (α := Set R) (Set.range Int.cast) {0, 1}

Tactic:
rw [funext intCast_eq_ite, Set.range_ite_const]

Premises used: funext, Set.range_ite_const, CharTwo.intCast_eq_ite
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
h : Even (α := ℤ) 0
⊢ ∃ (a : ℤ), Even a

Tactic:
use 0
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ Even (α := ℤ) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
h : ¬Even (α := ℤ) 1
⊢ ∃ (a : ℤ), ¬Even a

Tactic:
use 1
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ ¬Even (α := ℤ) 1

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_1 + 1} (α := R) (↑n : R) 1

Tactic:
(Set.ext_iff.1 range_intCast _).1 (Set.mem_range_self _)

Premises used: Set.mem_range_self, Set.insert, Set.Mem, setOf, Set.singleton, Iff.mp, Set.ext_iff, CharTwo.range_intCast
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (↑(n % 2) : R)

Tactic:
simp [intCast_eq_ite, Int.even_iff]

Premises used: Int.even_iff, CharTwo.intCast_eq_ite
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
⊢ HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
simp [add_pow_two]

Premises used: add_pow_two
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
rw : HPow.hPow (β := ℕ) (x + y) 2 = x * x + y * y
rw₁ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + y * y
rw₂ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
rw₃ rw₄ : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ (x + y) * (x + y) = x * x + y * y

Tactic:
rw [← pow_two, ← pow_two, ← pow_two, add_sq]

Premises used: pow_two, CharTwo.add_sq
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : List R
⊢ HPow.hPow (β := ℕ) l.sum 2 = List.sum (List.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)

Tactic:
map_list_sum sqAddMonoidHom _

Premises used: _private.0.CharTwo.sqAddMonoidHom, map_list_sum
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : List R
simp_rw : HPow.hPow (β := ℕ) l.sum 2 = List.sum (List.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)
⊢ l.sum * l.sum = List.sum (List.map (fun (x : R) ↦ x * x) l)

Tactic:
simp_rw [← pow_two, list_sum_sq]

Premises used: pow_two, CharTwo.list_sum_sq
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : Multiset R
⊢ HPow.hPow (β := ℕ) l.sum 2 = Multiset.sum (Multiset.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)

Tactic:
map_multiset_sum sqAddMonoidHom _

Premises used: map_multiset_sum, _private.0.CharTwo.sqAddMonoidHom
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : Multiset R
simp_rw : HPow.hPow (β := ℕ) l.sum 2 = Multiset.sum (Multiset.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)
⊢ l.sum * l.sum = Multiset.sum (Multiset.map (fun (x : R) ↦ x * x) l)

Tactic:
simp_rw [← pow_two, multiset_sum_sq]

Premises used: pow_two, CharTwo.multiset_sum_sq
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring R
inst_1 : CharP R 2
s : Finset ι
f : ι → R
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 = ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2

Tactic:
map_sum sqAddMonoidHom _ _

Premises used: _private.0.CharTwo.sqAddMonoidHom, map_sum
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring R
inst_1 : CharP R 2
s : Finset ι
f : ι → R
simp_rw : HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 = ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2
⊢ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i

Tactic:
simp_rw [← pow_two, sum_sq]

Premises used: pow_two, CharTwo.sum_sq
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y)
rwa :
  ∀ (h : HAdd.hAdd (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y) = 0),
    x = y
rwa₁ : ∀ (h : HPow.hPow (β := ℕ) (x + y) 2 = 0), x = y
rwa₂ : ∀ (h : x + y = 0), x = y
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : x = y), x = y
⊢ x = y

Tactic:
rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

Premises used: pow_eq_zero_iff, two_ne_zero, CharTwo.add_eq_zero, CharTwo.add_sq
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
⊢ HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℕ) y 2 ↔ x = y

Tactic:
sq_injective.eq_iff

Premises used: Function.Injective.eq_iff, CharTwo.sq_injective
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) (-1) 1 ↔ ringChar R = 2

Tactic:
⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩

Premises used: CharTwo.neg_eq, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
refine : ∀ (h : Eq.{u_1 + 1} (α := R) (-1) 1), ringChar R = 2
⊢ Eq.{u_1 + 1} (α := R) (-1) 1 ↔ ringChar R = 2

Tactic:
refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : Eq.{u_1 + 1} (α := R) (-1) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 0

Tactic:
rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h

Premises used: sub_eq_zero, eq_comm, Nat.cast_add, Nat.cast_one, sub_neg_eq_add
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 0
⊢ ringChar R = 2

Tactic:
((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

Premises used: ringChar.dvd, Or.resolve_left, Nat.dvd_prime, Nat.prime_two, Iff.mp, CharP.ringChar_ne_one
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 0
⊢ ringChar R = 2

Tactic:
exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

Premises used: ringChar.dvd, Or.resolve_left, Nat.dvd_prime, Nat.prime_two, Iff.mp, CharP.ringChar_ne_one
-- Module: Mathlib.Algebra.CharZero.AddMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommMonoidWithOne N
inst_2 : CharZero M
e : M →+ N
he : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) 1 : N) (1 : N)
he' : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)
n m : ℕ
h : Eq.{u_2 + 1} (α := N) (↑n : N) (↑m : N)
rwa : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((↑m : N) : N)), n = m
rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((e : (a : M) → N) (↑m : M) : N)), n = m
rwa₂ : ∀ (h : Eq.{u_1 + 1} (α := M) (↑n : M) (↑m : M)), n = m
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : n = m), n = m
⊢ n = m

Tactic:
rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h

Premises used: Function.Injective.eq_iff, Nat.cast_inj, map_natCast'
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)
zero : Eq.{u_1 + 1} (α := R) (↑n : R) 0
⊢ 0 = n

Tactic:
rw [H n]
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)
zero : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
zero₁ zero₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
rw [← h, Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑n : R)
succ : ∀ (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)), m + 1 = 0
succ₁ : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑(n + 1) : R)), m + 1 = n + 1
⊢ m + 1 = n

Tactic:
cases n
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)
succ : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) 0
⊢ m + 1 = 0

Tactic:
apply H
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)
succ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
succ₁ succ₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) 0

Tactic:
rw [h, Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑(n + 1) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)

Tactic:
simp only [Nat.cast_succ, add_right_cancel_iff] at h

Premises used: Nat.cast_succ, add_right_cancel_iff
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
succ : n + 1 = n + 1
succ₁ : ℕ
succ₂ : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
succ₃ : n + 1 = n + 1
succ₄ : ℕ
succ₅ succ₆ succ₇ : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
⊢ m + 1 = n + 1

Tactic:
rwa [ih]
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
zero : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)), 0 = n
succ :
  ∀ (m : ℕ) (ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n) (n : ℕ)
    (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑n : R)), m + 1 = n
⊢ m = n

Tactic:
induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]

Premises used: Nat.cast_succ, add_right_cancel_iff, Nat.cast_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Function.Injective.{1, u_1 + 1} (β := R) Nat.cast

Tactic:
CharZero.cast_injective

Premises used: CharZero.cast_injective
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R) ↔ m = n

Tactic:
cast_injective.eq_iff

Premises used: Function.Injective.eq_iff, Nat.cast_injective
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑0 : R) ↔ n = 0
rw₁ rw₂ : n = 0 ↔ n = 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ n = 0

Tactic:
rw [← cast_zero, cast_inj]

Premises used: Nat.cast_inj, Nat.cast_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
⊢ Ne.{u_1 + 1} (α := R) (↑n : R) 0 ↔ n ≠ 0

Tactic:
not_congr cast_eq_zero

Premises used: Nat.cast_eq_zero, not_congr
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
⊢ HAdd.hAdd (α := R) (↑n : R) 1 ≠ 0

Tactic:
mod_cast n.succ_ne_zero

Premises used: congrArg, False.elim, Nat.cast_add._simp_1, noConfusion_of_Nat, cast, Ne, Nat.cast, Nat.succ_ne_zero, HAdd.hAdd, congr, Nat.ctorIdx, Nat.cast_inj._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, eq_false', Nat.cast_one, Not, Eq.trans
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑1 : R) ↔ n = 1
rw₁ rw₂ : n = 1 ↔ n = 1
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

Premises used: Nat.cast_inj, Nat.cast_one
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
⊢ Ne.{u_1 + 1} (α := R) (↑n : R) 1 ↔ n ≠ 1

Tactic:
cast_eq_one.not

Premises used: Iff.not, Nat.cast_eq_one
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Ne.{u_1 + 1} (α := R) (ofNat n) 0

Tactic:
Nat.cast_ne_zero.2 (NeZero.ne n)

Premises used: Iff.mpr, Nat.cast_ne_zero, NeZero.ne
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Ne.{u_1 + 1} (α := R) 0 (ofNat n)

Tactic:
(ofNat_ne_zero n).symm

Premises used: OfNat.ofNat_ne_zero, Ne.symm
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Ne.{u_1 + 1} (α := R) (ofNat n) 1

Tactic:
Nat.cast_ne_one.2 (Nat.AtLeastTwo.ne_one)

Premises used: Iff.mpr, Nat.cast_ne_one, Nat.AtLeastTwo.ne_one
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Ne.{u_1 + 1} (α := R) 1 (ofNat n)

Tactic:
(ofNat_ne_one n).symm

Premises used: OfNat.ofNat_ne_one, Ne.symm
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
m n : ℕ
inst_2 : m.AtLeastTwo
inst_3 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (ofNat m) (ofNat n) ↔ Eq (α := ℕ) (ofNat m) (ofNat n)

Tactic:
Nat.cast_inj

Premises used: Nat.cast_inj
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
M : Type u_2
n : ℕ
inst : NeZero n
inst_1 : AddMonoidWithOne M
inst_2 : CharZero M
⊢ NeZero.{u_2} (R := M) (↑n : M)

Tactic:
⟨Nat.cast_ne_zero.mpr out⟩

Premises used: Iff.mpr, NeZero.mk, NeZero.out, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoidWithOne M
inst_1 : CharZero M
rw : Ne (α := ℕ) 1 0
⊢ Ne.{u_2 + 1} (α := M) 1 0

Tactic:
rw [← Nat.cast_one, Nat.cast_ne_zero]

Premises used: Nat.cast_one, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoidWithOne M
inst_1 : CharZero M
⊢ Ne (α := ℕ) 1 0

Tactic:
trivial
-- Module: Mathlib.Algebra.CharZero.Defs
Goal:
R : Type u_1
M : Type u_2
n : ℕ
inst : n.AtLeastTwo
inst_1 : AddMonoidWithOne M
inst_2 : CharZero M
⊢ NeZero.{u_2} (R := M) (OfNat.ofNat n)

Tactic:
⟨OfNat.ofNat_ne_zero n⟩

Premises used: NeZero.mk, OfNat.ofNat_ne_zero
-- Module: Mathlib.Algebra.CharZero.Infinite
Goal:
M : Type u_1
inst : AddMonoidWithOne M
inst_1 : CharZero M
⊢ Infinite M

Tactic:
Infinite.of_injective Nat.cast Nat.cast_injective

Premises used: Infinite.of_injective, Nat.cast, Nat.cast_injective
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
simp_rw : (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r
⊢ (∃ (k : ℤ), k • p = z • r) ↔
    ∃ (k : Fin z.natAbs), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑z : R)))

Tactic:
simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]

Premises used: eq_sub_iff_add_eq, smul_mul_assoc, AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (↑z : R) 0

Tactic:
have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
simp : ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r
| ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r

Tactic:
simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]

Premises used: Function.Injective.eq_iff, mul_right_injective₀
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
conv_rhs :
  (∃ (k : ℤ), k • p = z • r) ↔
    ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r

Tactic:
conv_rhs => simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]

Premises used: Function.Injective.eq_iff, mul_right_injective₀
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
simp_rw : (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
⊢ (∃ (k : ℤ), k • p = z • r) ↔
    ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r

Tactic:
simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel₀ hz',
    mul_one, ← natCast_zsmul, smul_smul, ← add_smul]

Premises used: Int.cast, zsmul_eq_mul, mul_inv_cancel₀, smul_smul, Inv.inv, add_smul, mul_smul_comm, mul_one, natCast_zsmul, smul_add
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
mp : (∃ (k : ℤ), k • p = z • r) → ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
mpr : (∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r) → ∃ (k : ℤ), k • p = z • r
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r

Tactic:
constructor
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p
⊢ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r

Tactic:
simp_rw [← h]
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p

Tactic:
⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩

Premises used: Fin.mk, HDiv.hDiv, HMod.hMod, Exists.intro, Int.toNat
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : (k % z).toNat < z.natAbs
mp₁ : (z * (k / z) + (↑(↑(⟨(k % z).toNat, ⋯⟩ : Fin z.natAbs) : ℕ) : ℤ)) • p = k • p
⊢ ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p

Tactic:
refine ⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : k % z < (↑z.natAbs : ℤ)
⊢ (k % z).toNat < z.natAbs

Tactic:
rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]

Premises used: Int.toNat_of_nonneg, Int.ofNat_lt, Int.emod_nonneg
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ k % z < (↑z.natAbs : ℤ)

Tactic:
(Int.emod_lt_abs _ hz).trans_eq (Int.abs_eq_natAbs _)

Premises used: Int.emod_lt_abs, LT.lt.trans_eq, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ k % z < (↑z.natAbs : ℤ)

Tactic:
exact (Int.emod_lt_abs _ hz).trans_eq (Int.abs_eq_natAbs _)

Premises used: Int.emod_lt_abs, LT.lt.trans_eq, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : (z * (k / z) + k % z) • p = k • p
⊢ (z * (k / z) + (↑(↑(⟨(k % z).toNat, ⋯⟩ : Fin z.natAbs) : ℕ) : ℤ)) • p = k • p

Tactic:
rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]

Premises used: Int.toNat_of_nonneg, Fin.val_mk, Int.emod_nonneg
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : (z * (k / z) + k % z) • p = (z * (k / z) + k % z) • p
⊢ (z * (k / z) + k % z) • p = k • p

Tactic:
nth_rewrite 3 [← Int.mul_ediv_add_emod k z]

Premises used: Int.mul_ediv_add_emod
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = (z * (k / z) + k % z) • p

Tactic:
rfl
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : Fin z.natAbs
n : ℤ
h : (z * n + (↑(↑k : ℕ) : ℤ)) • p = z • r
⊢ ∃ (k : ℤ), k • p = z • r

Tactic:
⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : Fin z.natAbs
n : ℤ
h : (z * n + (↑(↑k : ℕ) : ℤ)) • p = z • r
⊢ ∃ (k : ℤ), k • p = z • r

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
rw :
  (∃ (k : Fin (Int.natAbs (↑n : ℤ))),
      Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))) ↔
    ∃ (k : Fin n), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))
⊢ Membership.mem (γ := AddSubgroup R) (zmultiples p) (n • r) ↔
    ∃ (k : Fin n), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))

Tactic:
rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
    Int.cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.natCast_ne_zero, AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div, natCast_zsmul
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ (k : Fin (Int.natAbs (↑n : ℤ))),
      Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))) ↔
    ∃ (k : Fin n), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))

Tactic:
rfl