awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℕ
rw : n • a = (↑(↑n : ℤ) : α) * a
rw₁ : (↑n : α) * a = (↑(↑n : ℤ) : α) * a
rw₂ rw₃ : (↑n : α) * a = (↑n : α) * a
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) a = (↑(↑n : ℤ) : α) * a

Tactic:
rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]

Premises used: Int.cast_natCast, nsmul_eq_mul, natCast_zsmul
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℕ
⊢ -[n+1] • a = (↑-[n+1] : α) * a

Tactic:
simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]

Premises used: neg_add_rev, add_mul, Nat.cast_succ, Int.cast_negSucc
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
rw : (↑n : α) * a = a * (↑n : α)
rw₁ rw₂ : a * (↑n : α) = a * (↑n : α)
⊢ n • a = a * (↑n : α)

Tactic:
rw [zsmul_eq_mul, (n.cast_commute a).eq]

Premises used: zsmul_eq_mul, Int.cast_commute, Commute.eq
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
n : ℤ
hn : Odd n
⊢ Odd.{u_3} (α := α) (↑n : α)

Tactic:
hn.map (castRingHom α)

Premises used: Odd.map, Int.castRingHom
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
m n : ℤ
h : m ∣ n
⊢ Dvd.dvd.{u_3} (α := α) (↑m : α) (↑n : α)

Tactic:
map_dvd (Int.castRingHom α) h

Premises used: map_dvd, Int.castRingHom
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a x y : α
h : SemiconjBy a x y
n : ℤ
⊢ SemiconjBy a ((↑n : α) * x) ((↑n : α) * y)

Tactic:
SemiconjBy.mul_right (Int.commute_cast _ _) h

Premises used: Int.commute_cast, SemiconjBy.mul_right
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a x y : α
h : SemiconjBy a x y
n : ℤ
⊢ SemiconjBy ((↑n : α) * a) x y

Tactic:
SemiconjBy.mul_left (Int.cast_commute _ _) h

Premises used: Int.cast_commute, SemiconjBy.mul_left
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a x y : α
h : SemiconjBy a x y
m n : ℤ
⊢ SemiconjBy ((↑m : α) * a) ((↑n : α) * x) ((↑n : α) * y)

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
⊢ Commute (↑n : α) a

Tactic:
Int.cast_commute _ _

Premises used: Int.cast_commute
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
⊢ Commute a (↑n : α)

Tactic:
Int.commute_cast _ _

Premises used: Int.commute_cast
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute a ((↑m : α) * b)

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute ((↑m : α) * a) b

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a b : α
h : Commute a b
m n : ℤ
⊢ Commute ((↑m : α) * a) ((↑n : α) * b)

Tactic:
SemiconjBy.intCast_mul_intCast_mul h m n

Premises used: Commute, SemiconjBy.intCast_mul_intCast_mul
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a : α
n : ℤ
⊢ Commute a ((↑n : α) * a)

Tactic:
(Commute.refl a).intCast_mul_right n

Premises used: Commute.refl, Commute.intCast_mul_right
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a : α
n : ℤ
⊢ Commute ((↑n : α) * a) a

Tactic:
(Commute.refl a).intCast_mul_left n

Premises used: Commute.refl, Commute.intCast_mul_left
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Ring α
a : α
m n : ℤ
⊢ Commute ((↑m : α) * a) ((↑n : α) * a)

Tactic:
(Commute.refl a).intCast_mul_intCast_mul m n

Premises used: Commute.refl, Commute.intCast_mul_intCast_mul
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
A : Type u_5
inst : AddMonoid A
f g : ℤ →+ A
h1 : Eq (α := A) ((f : (a : ℤ) → A) 1 : A) ((g : (a : ℤ) → A) 1 : A)
⊢ f = g

Tactic:
have : f.comp (Int.ofNatHom : ℕ →+ ℤ) = g.comp (Int.ofNatHom : ℕ →+ ℤ) := ext_nat' _ _ h1
  have this' : ∀ n : ℕ, f n = g n := DFunLike.ext_iff.1 this
  ext fun n => match n with
  | (n : ℕ) => this' n
  | .negSucc n => eq_on_neg _ _ (this' <| n + 1)

Premises used: Int.ofNatHom, AddMonoidHomClass.toAddMonoidHom, eq_on_neg, DFunLike.ext_iff, AddMonoidHom.ext, HAdd.hAdd, Iff.mp, _private.0.zsmul_eq_mul.match_1, OfNat.ofNat, Eq, AddMonoidHom.comp, DFunLike.coe, ext_nat'
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
A : Type u_5
inst : AddGroupWithOne A
f : ℤ →+ A
h1 : Eq (α := A) ((f : (a : ℤ) → A) 1 : A) (1 : A)
⊢ Eq (α := A) ((f : (a : ℤ) → A) 1 : A) ((castAddHom A : (a : ℤ) → A) 1 : A)

Tactic:
simp [h1]
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
A : Type u_5
inst : AddMonoid A
f g : ℤ ≃+ A
h1 : Eq (α := A) ((f : (a : ℤ) → A) 1 : A) ((g : (a : ℤ) → A) 1 : A)
⊢ f = g

Tactic:
toAddMonoidHom_injective <| AddMonoidHom.ext_int h1

Premises used: AddMonoidHom.ext_int, AddEquiv.toAddMonoidHom_injective
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
α : Type u_3
inst : AddGroupWithOne α
inst_1 : FunLike F ℤ α
inst_2 : AddMonoidHomClass F ℤ α
f : F
h₁ : Eq.{u_3 + 1} (α := α) ((f : (a : ℤ) → α) 1 : α) (1 : α)
⊢ ∀ (n : ℤ), Eq.{u_3 + 1} (α := α) ((f : (a : ℤ) → α) n : α) ((↑n : α) : α)

Tactic:
DFunLike.ext_iff.1 <| (f : ℤ →+ α).eq_intCastAddHom h₁

Premises used: AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.eq_intCastAddHom, DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
inst_2 : FunLike F α β
inst_3 : AddMonoidHomClass F α β
f : F
h₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
⊢ Eq (α := β) ((AddMonoidHom.comp (↑f : α →+ β) (castAddHom α) : (a : ℤ) → β) 1 : β) (1 : β)

Tactic:
simpa
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
⊢ castAddHom ℤ = AddMonoidHom.id ℤ

Tactic:
((AddMonoidHom.id ℤ).eq_intCastAddHom rfl).symm

Premises used: AddMonoidHom.eq_intCastAddHom, AddMonoidHom.id, Int, Eq.symm, rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : Multiplicative ℤ →* M
h1 :
  Eq (α := M) ((f : (a : Multiplicative ℤ) → M) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : M)
    ((g : (a : Multiplicative ℤ) → M) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : M)
⊢ f = g

Tactic:
MonoidHom.toAdditiveRight.injective <| AddMonoidHom.ext_int <| Additive.toMul.injective h1

Premises used: Additive.toMul, AddMonoidHom.ext_int, Equiv.injective, MonoidHom.toAdditiveRight
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
h : ∀ (x : ℕ), Eq (α := M) ((f : (a : ℤ) → M) (ofNat x) : M) ((g : (a : ℤ) → M) (ofNat x) : M)
h₁ : ∀ (x : ℕ), Eq (α := M) ((f : (a : ℤ) → M) -[x+1] : M) ((g : (a : ℤ) → M) -[x+1] : M)
⊢ f = g

Tactic:
ext (x | x)
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ Eq (α := M) ((f : (a : ℤ) → M) (ofNat x) : M) ((g : (a : ℤ) → M) (ofNat x) : M)

Tactic:
(DFunLike.congr_fun h_nat x :)

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ Eq (α := M) ((f : (a : ℤ) → M) (ofNat x) : M) ((g : (a : ℤ) → M) (ofNat x) : M)

Tactic:
exact (DFunLike.congr_fun h_nat x :)

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
h :
  HMul.hMul (α := M) (β := M) ((f : (a : ℤ) → M) (-1) : M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M) =
    HMul.hMul (α := M) (β := M) ((g : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
⊢ Eq (α := M) ((f : (a : ℤ) → M) -[x+1] : M) ((g : (a : ℤ) → M) -[x+1] : M)

Tactic:
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]

Premises used: neg_one_mul, Int.negSucc_eq, MonoidHom.map_mul
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
h :
  Eq (α := M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
    ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
⊢ HMul.hMul (α := M) (β := M) ((f : (a : ℤ) → M) (-1) : M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M) =
    HMul.hMul (α := M) (β := M) ((g : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)

Tactic:
congr 1
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ Eq (α := M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
    ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)

Tactic:
mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

Premises used: DFunLike.congr_fun, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ Eq (α := M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
    ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)

Tactic:
exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

Premises used: DFunLike.congr_fun, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
M : Type u_5
inst : MonoidWithZero M
f g : ℤ →*₀ M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp ofNatHom.toMonoidWithZeroHom = g.comp ofNatHom.toMonoidWithZeroHom
⊢ f = g

Tactic:
toMonoidHom_injective <| MonoidHom.ext_int h_neg_one <|
    MonoidHom.ext (DFunLike.congr_fun h_nat :)

Premises used: DFunLike.congr_fun, MonoidHom.ext_int, MonoidHom.ext, MonoidWithZeroHom.toMonoidHom_injective
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
α : Type u_3
inst : MonoidWithZero α
inst_1 : FunLike F ℤ α
inst_2 : MonoidWithZeroHomClass F ℤ α
f g : F
h_neg_one : Eq.{u_3 + 1} (α := α) ((f : (a : ℤ) → α) (-1) : α) ((g : (a : ℤ) → α) (-1) : α)
h_pos : ∀ (n : ℕ), 0 < n → Eq.{u_3 + 1} (α := α) ((f : (a : ℤ) → α) (↑n : ℤ) : α) ((g : (a : ℤ) → α) (↑n : ℤ) : α)
⊢ f = g

Tactic:
(DFunLike.ext _ _) fun n =>
    haveI :=
      DFunLike.congr_fun
        (@MonoidWithZeroHom.ext_int _ _ (f : ℤ →*₀ α) (g : ℤ →*₀ α) h_neg_one <|
          MonoidWithZeroHom.ext_nat (h_pos _))
        n
    this

Premises used: DFunLike.congr_fun, MonoidWithZeroHom.ext_int, DFunLike.ext, MonoidWithZeroHom.ext_nat
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
β : Type u_4
inst : AddGroup β
x : β
n : ℤ
⊢ (((zmultiplesHom β : (a : β) → ℤ →+ β) x : ℤ →+ β) : (a : ℤ) → β) n = n • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
β : Type u_4
inst : AddGroup β
f : ℤ →+ β
⊢ Eq (α := β) ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f : β) ((f : (a : ℤ) → β) 1 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Group α
x : α
n : Multiplicative ℤ
⊢ (((zpowersHom α : (a : α) → Multiplicative ℤ →* α) x : Multiplicative ℤ →* α) : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (β := ℤ) x ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Group α
f : Multiplicative ℤ →* α
⊢ Eq (α := α) ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
    ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
rw :
  (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ) ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
rw₁ :
  Eq (α := α) ((f : (a : Multiplicative ℤ) → α) n : α)
    ((((zpowersHom α : (a : α) → Multiplicative ℤ →* α)
              ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f) :
            Multiplicative ℤ →* α) :
          (a : Multiplicative ℤ) → α)
        n :
      α)
rw₂ rw₃ : Eq (α := α) ((f : (a : Multiplicative ℤ) → α) n : α) ((f : (a : Multiplicative ℤ) → α) n : α)
⊢ (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ)
      ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)

Tactic:
rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, zpowersHom_symm_apply, zpowersHom_apply
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
β : Type u_4
inst : AddGroup β
f : ℤ →+ β
n : ℤ
rw : (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f : β)
rw₁ :
  Eq (α := β) ((f : (a : ℤ) → β) n : β)
    ((((zmultiplesHom β : (a : β) → ℤ →+ β) ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f) : ℤ →+ β) :
          (a : ℤ) → β)
        n :
      β)
rw₂ rw₃ : Eq (α := β) ((f : (a : ℤ) → β) n : β) ((f : (a : ℤ) → β) n : β)
⊢ (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((f : (a : ℤ) → β) 1 : β)

Tactic:
rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, zmultiplesHom_apply, zmultiplesHom_symm_apply
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst : CommGroup α
inst_1 : AddCommGroup β
a b : β
n : ℤ
⊢ Eq (α := β) ((Equiv.toFun (zmultiplesHom β) (a + b) : (a : ℤ) → β) n : β)
    ((HAdd.hAdd (α := ℤ →+ β) (Equiv.toFun (zmultiplesHom β) a) (Equiv.toFun (zmultiplesHom β) b) : (a : ℤ) → β) n : β)

Tactic:
simp [zsmul_add]

Premises used: zsmul_add
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst : CommGroup α
inst_1 : AddCommGroup β
a b : α
n : Multiplicative ℤ
⊢ Eq (α := α) ((Equiv.toFun (zpowersHom α) (a * b) : (a : Multiplicative ℤ) → α) n : α)
    ((HMul.hMul (α := Multiplicative ℤ →* α) (Equiv.toFun (zpowersHom α) a) (Equiv.toFun (zpowersHom α) b) :
          (a : Multiplicative ℤ) → α)
        n :
      α)

Tactic:
simp [mul_zpow]

Premises used: mul_zpow
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : CommGroup α
x : α
n : Multiplicative ℤ
⊢ (((zpowersMulHom α : (a : α) → Multiplicative ℤ →* α) x : Multiplicative ℤ →* α) : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (β := ℤ) x ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : CommGroup α
f : Multiplicative ℤ →* α
⊢ Eq (α := α) ((MulEquiv.symm (zpowersMulHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
    ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
β : Type u_4
inst : AddCommGroup β
x : β
n : ℤ
⊢ (((zmultiplesAddHom β : (a : β) → ℤ →+ β) x : ℤ →+ β) : (a : ℤ) → β) n = n • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
β : Type u_4
inst : AddCommGroup β
f : ℤ →+ β
⊢ Eq (α := β) ((AddEquiv.symm (zmultiplesAddHom β) : (a : ℤ →+ β) → β) f : β) ((f : (a : ℤ) → β) 1 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
α : Type u_3
inst : NonAssocRing α
inst_1 : FunLike F ℤ α
inst_2 : RingHomClass F ℤ α
f : F
n : ℤ
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℤ) → α) n : α) ((↑n : α) : α)

Tactic:
eq_intCast' f (map_one _) n

Premises used: eq_intCast', map_one
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : NonAssocRing α
inst_1 : NonAssocRing β
inst_2 : FunLike F α β
inst_3 : RingHomClass F α β
f : F
n : ℤ
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
eq_intCast ((f : α →+* β).comp (Int.castRingHom α)) n

Premises used: eq_intCast, RingHom.comp, RingHomClass.toRingHom, Int.castRingHom
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
f : ℤ →+* α
⊢ f = Int.castRingHom α

Tactic:
RingHom.ext <| eq_intCast f

Premises used: eq_intCast, RingHom.ext
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
R : Type u_5
inst : NonAssocSemiring R
f g : ℤ →+* R
⊢ f = g

Tactic:
coe_addMonoidHom_injective <| AddMonoidHom.ext_int <| f.map_one.trans g.map_one.symm

Premises used: RingHom.map_one, AddMonoidHom.ext_int, Eq.symm, RingHom.coe_addMonoidHom_injective, Eq.trans
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst : NonAssocRing α
inst_1 : NonAssocRing β
R : Type u_5
inst_2 : NonAssocSemiring R
⊢ Subsingleton.{max (u_5 + 1) 1} (ℤ →+* R)

Tactic:
⟨RingHom.ext_int⟩

Premises used: RingHom.ext_int, Subsingleton.intro
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
⊢ castRingHom ℤ = RingHom.id ℤ

Tactic:
(RingHom.id ℤ).eq_intCast'.symm

Premises used: Int, RingHom.eq_intCast', Eq.symm, RingHom.id
-- Module: Mathlib.Data.Int.Cast.Pi
Goal:
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → IntCast (π i)
n : ℤ
i : ι
⊢ Eq.{u_2 + 1} (α := π i) ((↑n : (i : ι) → π i) i) (↑n : π i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Pi
Goal:
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → IntCast (π i)
n : ℤ
⊢ Eq (α := (i : ι) → π i) (↑n : (i : ι) → π i) fun (x : ι) ↦ (↑n : π x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Pi
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : IntCast γ
n : ℤ
⊢ Eq (α := α ⊕ β → γ) (Sum.elim (↑n : α → γ) (↑n : β → γ)) (↑n : α ⊕ β → γ)

Tactic:
Sum.elim_lam_const_lam_const (γ := γ) n

Premises used: Int.cast, Sum.elim_lam_const_lam_const
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
fst : Eq.{u_1 + 1} (α := α) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).1 (↑x : α × β).1
snd : Eq.{u_2 + 1} (α := β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).2 (↑x : α × β).2
⊢ Eq (α := α × β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)) (↑x : α × β)

Tactic:
ext
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).1 (↑x : α × β).1

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).2 (↑x : α × β).2

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
fst : Eq.{u_1 + 1} (α := α) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).1 (-(↑(x + 1) : α × β)).1
snd : Eq.{u_2 + 1} (α := β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).2 (-(↑(x + 1) : α × β)).2
⊢ Eq (α := α × β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)) (-(↑(x + 1) : α × β))

Tactic:
ext
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).1 (-(↑(x + 1) : α × β)).1

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).2 (-(↑(x + 1) : α × β)).2

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (↑n : α × β).1 (↑n : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Prod
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
n : ℤ
⊢ Eq.{u_2 + 1} (α := β) (↑n : α × β).2 (↑n : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.CharZero
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℤ
n_dvd : n ∣ m
inl : ∀ (n_dvd : 0 ∣ m), (↑(m / 0) : k) = HDiv.hDiv (α := k) (↑m : k) (↑0 : k)
inr : ∀ (hn : n ≠ 0), (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
⊢ (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Int.CharZero
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ (↑(m / 0) : k) = HDiv.hDiv (α := k) (↑m : k) (↑0 : k)

Tactic:
simp [Int.ediv_zero]

Premises used: Int.ediv_zero
-- Module: Mathlib.Data.Int.CharZero
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)

Tactic:
cast_div n_dvd (cast_ne_zero.mpr hn)

Premises used: Iff.mpr, Int.cast_ne_zero, Int.cast_div
-- Module: Mathlib.Data.Int.CharZero
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)

Tactic:
exact cast_div n_dvd (cast_ne_zero.mpr hn)

Premises used: Iff.mpr, Int.cast_ne_zero, Int.cast_div
-- Module: Mathlib.Data.Int.CharZero
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℕ
n_dvd : n ∣ m
rw : HDiv.hDiv (α := k) (↑(↑m : ℤ) : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
rw₁ : HDiv.hDiv (α := k) (↑m : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
rw₂ rw₃ : HDiv.hDiv (α := k) (↑m : k) (↑n : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
⊢ (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)

Tactic:
rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.ofNat_dvd, Int.cast_div_charZero
-- Module: Mathlib.Data.Int.CharZero
Goal:
α : Type u_3
inst : NonAssocRing α
f : ℤ →+* α
inst_1 : CharZero α
⊢ Function.Injective (α := ℤ) (β := α) (⇑f : (a : ℤ) → α)

Tactic:
Subsingleton.elim (Int.castRingHom _) f ▸ Int.cast_injective

Premises used: Eq.rec, Int.castRingHom, Subsingleton.elim, Int.cast_injective
-- Module: Mathlib.Data.Int.CharZero
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne β
inst_1 : CharZero β
n : ℤ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Set α) (support.{u_1, u_2} (M := β) (↑n : α → β)) univ

Tactic:
support_const <| Int.cast_ne_zero.2 hn

Premises used: Iff.mpr, Function.support_const, Int.cast_ne_zero
-- Module: Mathlib.Data.Int.CharZero
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne β
inst_1 : CharZero β
n : ℤ
hn : n ≠ 1
⊢ Eq.{u_1 + 1} (α := Set α) (mulSupport.{u_1, u_2} (M := β) (↑n : α → β)) univ

Tactic:
mulSupport_const <| Int.cast_ne_one.2 hn

Premises used: Iff.mpr, Int.cast_ne_one, Function.mulSupport_const
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddAbove x
rw :
  IsLUB x (↑((Classical.choose (p := Membership.mem (upperBounds x)) ⋯).greatestOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
⊢ IsLUB x
    (if h : x.Nonempty ∧ BddAbove x then
      (↑((Classical.choose (p := Membership.mem (upperBounds x)) ⋯).greatestOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
    else 0)

Tactic:
rw [dif_pos ⟨hn, hb⟩]

Premises used: dif_pos
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddAbove x
⊢ IsLUB x (↑((Classical.choose (p := Membership.mem (upperBounds x)) ⋯).greatestOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)

Tactic:
(isGreatest_coe_greatestOfBdd ..).isLUB

Premises used: Set.Mem, setOf, Int.isGreatest_coe_greatestOfBdd, IsGreatest.isLUB