awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℤ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
add₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
neg₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
sub₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
zsmul₁ : ∀ (n : ℤ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
⊢ NonUnitalCommRing α

Tactic:
apply e.injective.nonUnitalCommRing _

Premises used: Function.Injective.nonUnitalCommRing, Equiv.injective
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x y : α
⊢ (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n : ℕ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n : ℕ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n : ℤ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n : ℤ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
add :
  ∀ (x y : α),
    (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
neg : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
sub :
  ∀ (x y : α),
    (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
zsmul : ∀ (n : ℤ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
intCast : ∀ (n : ℤ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
⊢ CommRing α

Tactic:
apply e.injective.commRing _

Premises used: Equiv.injective, Function.Injective.commRing
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℕ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℕ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℤ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℤ
x : α
⊢ (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℤ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n : ℤ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : IsDomain β
e : α ≃ β
⊢ IsDomain α

Tactic:
letI := e.semiring; e.injective.isDomain e.ringEquiv

Premises used: Equiv.ringEquiv, Function.Injective.isDomain, Equiv.injective
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
M₀ : Type u_1
inst : MulZeroClass M₀
x : ULift.{u_2, u_1} M₀
⊢ Eq.{u_1 + 1} (α := M₀) ((Equiv.ulift : (a : ULift M₀) → M₀) (0 * x) : M₀) ((Equiv.ulift : (a : ULift M₀) → M₀) 0 : M₀)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
M₀ : Type u_1
inst : MulZeroClass M₀
x : ULift.{u_2, u_1} M₀
⊢ Eq.{u_1 + 1} (α := M₀) ((Equiv.ulift : (a : ULift M₀) → M₀) (x * 0) : M₀) ((Equiv.ulift : (a : ULift M₀) → M₀) 0 : M₀)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : Distrib R
x x_1 x_2 : ULift.{u_1, u} R
⊢ Eq.{u + 1} (α := R) ((Equiv.ulift : (a : ULift R) → R) (x * (x_1 + x_2)) : R)
    ((Equiv.ulift : (a : ULift R) → R) (x * x_1 + x * x_2) : R)

Tactic:
simp [left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : Distrib R
x x_1 x_2 : ULift.{u_1, u} R
⊢ Eq.{u + 1} (α := R) ((Equiv.ulift : (a : ULift R) → R) ((x + x_1) * x_2) : R)
    ((Equiv.ulift : (a : ULift R) → R) (x * x_2 + x_1 * x_2) : R)

Tactic:
simp [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : NatCast R
n : ℕ
⊢ Eq (α := ULift.{u_1, u} R) { down := (↑n : R) } (↑n : ULift R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq (α := ULift.{u_1, u} R) { down := OfNat.ofNat n } (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : IntCast R
n : ℤ
⊢ Eq (α := ULift.{u_1, u} R) { down := (↑n : R) } (↑n : ULift R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : NatCast R
n : ℕ
⊢ Eq.{u + 1} (α := R) (down.{u_1, u} (↑n : ULift R)) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (down.{u_1, u} (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u
inst : IntCast R
n : ℤ
⊢ Eq.{u + 1} (α := R) (down.{u_1, u} (↑n : ULift R)) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : ULift.{u₁, u_1} R
⊢ Eq (α := ULift.{u_3, u_2} S) ((ulift.{u₁, u_3, u_1, u_2} f : (a : ULift R) → ULift S) x : ULift.{u_3, u_2} S)
    ({ down := (f : (a : R) → S) x.down } : ULift.{u_3, u_2} S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : ULift.{u₁, u_1} R
⊢ Eq.{u_2 + 1} (α := S) (ULift.down.{u_3, u_2} ((ulift.{u₁, u_3, u_1, u_2} f : (a : ULift R) → ULift S) x) : S)
    ((f : (a : R) → S) x.down : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.ULift
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ comp (RingEquiv.toRingHom ULift.ringEquiv)
      ((ulift.{u₁, u₂, u_1, u_2} f).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv))) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
β : Type v
R : Type x
inst : Monoid α
inst_1 : HasDistribNeg α
u : αˣ
⊢ -(↑u : α) * -(↑u⁻¹ : α) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
β : Type v
R : Type x
inst : Monoid α
inst_1 : HasDistribNeg α
u : αˣ
⊢ -(↑u⁻¹ : α) * -(↑u : α) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
u : αˣ
⊢ (↑(-u) : α) = -(↑u : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
⊢ Eq.{u + 1} (α := α) (↑(-1) : α) (-1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
a : αˣ
rw : (↑a : α) = (↑(-1) : α) ↔ a = -1
rw₁ rw₂ : a = -1 ↔ a = -1
⊢ (↑a : α) = -1 ↔ a = -1

Tactic:
rw [← Units.coe_neg_one, val_inj]

Premises used: Units.coe_neg_one, Units.val_inj
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u

Tactic:
simp only [divp, neg_mul]

Premises used: divp, neg_mul
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Semiring α
a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u

Tactic:
simp only [divp, add_mul]

Premises used: add_mul, divp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Semiring α
a b : α
u : αˣ
⊢ a + b /ₚ u = (a * (↑u : α) + b) /ₚ u

Tactic:
simp only [divp, add_mul, Units.mul_inv_cancel_right]

Premises used: add_mul, Units.mul_inv_cancel_right, divp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Semiring α
a b : α
u : αˣ
⊢ a /ₚ u + b = (a + b * (↑u : α)) /ₚ u

Tactic:
simp only [divp, add_mul, Units.mul_inv_cancel_right]

Premises used: add_mul, Units.mul_inv_cancel_right, divp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : a /ₚ u + -(b /ₚ u) = (a - b) /ₚ u
rw₁ : a /ₚ u + -(b /ₚ u) = (a + -b) /ₚ u
rw₂ : a /ₚ u + -b /ₚ u = (a + -b) /ₚ u
rw₃ rw₄ : (a + -b) /ₚ u = (a + -b) /ₚ u
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]

Premises used: sub_eq_add_neg, Units.divp_add_divp_same, Units.neg_divp
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
⊢ a - b /ₚ u = (a * (↑u : α) - b) /ₚ u

Tactic:
simp only [divp, sub_mul, Units.mul_inv_cancel_right]

Premises used: Units.mul_inv_cancel_right, divp, sub_mul
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
simp : b = b * (↑u : α) * (↑u⁻¹ : α)
⊢ a /ₚ u - b = (a - b * (↑u : α)) /ₚ u

Tactic:
simp only [divp, sub_mul, sub_right_inj]

Premises used: sub_right_inj, divp, sub_mul