awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
⊢ Eq.{u_2 + 1} (α := Subsemiring T) (subsemiringClosure (square T)) (Subsemiring.closure {x : T | IsSquare x})

Tactic:
simp [Submonoid.subsemiringClosure_eq_closure]

Premises used: Submonoid.subsemiringClosure_eq_closure
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
T : Type u_2
inst : CommSemiring T
⊢ 1 ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (NonUnitalSubsemiring.toAddSubmonoid (NonUnitalSubsemiring.sumSq T)))

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
⊢ Eq (α := NonUnitalSubsemiring T) (toNonUnitalSubsemiring (sumSq T)) (NonUnitalSubsemiring.sumSq T)

Tactic:
rfl

Premises used: iInf, NonUnitalSubsemiring.sumSq, Set.iInter, AddSubmonoid.closure, rfl, Subsemigroup.nonUnitalSubsemiringClosure
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
s : T
⊢ Membership.mem (γ := Subsemiring T) (sumSq T) s ↔ IsSumSq s

Tactic:
simp [← Subsemiring.mem_toNonUnitalSubsemiring]

Premises used: Subsemiring.mem_toNonUnitalSubsemiring
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
h : ∀ (x : T), x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x
⊢ (↑(sumSq T) : Set T) = {s : T | IsSumSq s}

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
x : T
⊢ x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subsemiring T) toNonUnitalSubsemiring

Tactic:
toNonUnitalSubsemiring_injective

Premises used: Subsemiring.toNonUnitalSubsemiring_injective
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
apply_fun :
  Eq (α := NonUnitalSubsemiring T) (toNonUnitalSubsemiring (closure {x : T | IsSquare x}))
    (toNonUnitalSubsemiring (sumSq T))
⊢ Eq (α := Subsemiring T) (closure {x : T | IsSquare x}) (sumSq T)

Tactic:
apply_fun toNonUnitalSubsemiring using toNonUnitalSubsemiring_injective

Premises used: Subsemiring.toNonUnitalSubsemiring, Subsemiring.toNonUnitalSubsemiring_injective
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : CommSemiring T
⊢ Eq (α := NonUnitalSubsemiring T) (toNonUnitalSubsemiring (closure {x : T | IsSquare x}))
    (toNonUnitalSubsemiring (sumSq T))

Tactic:
simp [← Submonoid.square_subsemiringClosure]

Premises used: _private.0.Submonoid.square_subsemiringClosure
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ ∀ c ∈ I, Membership.mem (γ := Subsemiring R) (Subsemiring.sumSq R) (x c)

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ IsSumSq.{u_1} (R := R) (∏ i ∈ I, x i)

Tactic:
simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)

Premises used: prod_mem
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : R
⊢ LE.le.{u_2} (α := R) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s x s_1 : R
hx : IsSquare x
hs : IsSumSq s_1
h : 0 ≤ s_1
⊢ 0 ≤ x + s_1

Tactic:
add_nonneg (IsSquare.nonneg hx) h

Premises used: add_nonneg, IsSquare.nonneg
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s x s_1 : R
hx : IsSquare x
hs : IsSumSq s_1
h : 0 ≤ s_1
⊢ 0 ≤ x + s_1

Tactic:
exact add_nonneg (IsSquare.nonneg hx) h

Premises used: add_nonneg, IsSquare.nonneg
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : R
hs : IsSumSq s
zero : LE.le.{u_2} (α := R) 0 0
sq_add : ∀ {x s : R} (hx : IsSquare x), IsSumSq s → ∀ (h : 0 ≤ s), 0 ≤ x + s
⊢ 0 ≤ s

Tactic:
induction hs using IsSumSq.rec' with
  | zero          => simp
  | sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h

Premises used: IsSumSq.zero, IsSumSq.sq_add, IsSumSq.rec'
-- Module: Mathlib.Algebra.Ring.Torsion
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ n • a) a) ((fun (a : R) ↦ n • a) b)
⊢ a = b ∨ n = 0

Tactic:
simp only [nsmul_eq_mul, mul_eq_mul_left_iff, Nat.cast_eq_zero] at w

Premises used: mul_eq_mul_left_iff, Nat.cast_eq_zero, nsmul_eq_mul
-- Module: Mathlib.Algebra.Ring.Torsion
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : a = b ∨ n = 0
⊢ a = b

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Torsion
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (HPow.hPow (α := R) (-1) (Nat.succ 1)) : M) (1 : M)
rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) 1 : M) (1 : M)
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 1 1
⊢ HPow.hPow (α := M) ((f : (a : R) → M) (-1) : M) (Nat.succ 1) = 1

Tactic:
rw [← map_pow, neg_one_sq, map_one]

Premises used: neg_one_sq, map_pow, map_one
-- Module: Mathlib.Algebra.Ring.Torsion
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-1 * x) : M) ((f : (a : R) → M) x : M)
rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : R) → M) (-1) : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
rw₂ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
rw₃ rw₄ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) x : M) ((f : (a : R) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-x) : M) ((f : (a : R) → M) x : M)

Tactic:
rw [← neg_one_mul, map_mul, map_neg_one, one_mul]

Premises used: neg_one_mul, map_mul, MonoidHom.map_neg_one, one_mul
-- Module: Mathlib.Algebra.Ring.Torsion
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x y : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-(x - y)) : M) ((f : (a : R) → M) (y - x) : M)
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (y - x) : M) ((f : (a : R) → M) (y - x) : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (x - y) : M) ((f : (a : R) → M) (y - x) : M)

Tactic:
rw [← map_neg, neg_sub]

Premises used: neg_sub, MonoidHom.map_neg
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e_1 e : α ≃ β
inst : Add β
inst_1 : Mul β
add : Add α := e.add
mul : Mul α := e.mul
⊢ Type (max u_2 u_1)

Tactic:
exact α ≃+* β
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e_1 e : α ≃ β
inst : Add β
inst_1 : Mul β
add : Add α := e.add
mul : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp [mul_def]

Premises used: Equiv.mul_def
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e_1 e : α ≃ β
inst : Add β
inst_1 : Mul β
add : Add α := e.add
mul : Mul α := e.mul
x y : α
⊢ e.toFun (x + y) = e.toFun x + e.toFun y

Tactic:
simp [add_def]

Premises used: Equiv.add_def
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e_1 e : α ≃ β
inst : Add β
inst_1 : Mul β
add : Add α := e.add
mul : Mul α := e.mul
⊢ α ≃+* β

Tactic:
exact
    { e with
      map_add' := fun x y => by
        simp [add_def]
      map_mul' := fun x y => by
        simp [mul_def] }
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Add β
inst_1 : Mul β
a : α
⊢ Eq.{u_2 + 1} (α := β) ((e.ringEquiv : (a : α) → β) a : β) ((e : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e_1 e : α ≃ β
inst : Add β
inst_1 : Mul β
b : β
this_1 : Add α := e.add
this : Mul α := e.mul
⊢ Prop

Tactic:
exact (ringEquiv e).symm b = e.symm b

Premises used: Equiv.ringEquiv, Equiv.symm, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Add β
inst_1 : Mul β
b : β
⊢ Eq.{u_1 + 1} (α := α) ((RingEquiv.symm e.ringEquiv : (a : β) → α) b : α) ((e.symm : (a : β) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : β)
nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
⊢ NonUnitalNonAssocSemiring α

Tactic:
apply e.injective.nonUnitalNonAssocSemiring _

Premises used: Function.Injective.nonUnitalNonAssocSemiring, Equiv.injective
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : β)
nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
⊢ NonUnitalSemiring α

Tactic:
apply e.injective.nonUnitalSemiring _

Premises used: Function.Injective.nonUnitalSemiring, Equiv.injective
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : 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 : AddMonoidWithOne β
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ((e.symm : (a : β) → α) (↑0 : β) : α) : β) ((e : (a : α) → β) 0 : β)

Tactic:
simp [zero_def]

Premises used: Equiv.zero_def
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : AddMonoidWithOne β
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ((e.symm : (a : β) → α) (↑(n + 1) : β) : α) : β)
    ((e : (a : α) → β) (HAdd.hAdd (α := α) (β := α) ((e.symm : (a : β) → α) (↑n : β) : α) (1 : α)) : β)

Tactic:
simp [add_def, one_def]

Premises used: Equiv.add_def, Equiv.one_def
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : AddGroupWithOne β
n : ℕ
simp : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) (↑n : β) : α) ((↑n : α) : α)
⊢ Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) (↑(↑n : ℤ) : β) : α) ((↑n : α) : α)

Tactic:
simp only [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : AddGroupWithOne β
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) (↑n : β) : α) ((↑n : α) : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : β)
nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
⊢ NonAssocSemiring α

Tactic:
apply e.injective.nonAssocSemiring _

Premises used: Function.Injective.nonAssocSemiring, Equiv.injective
-- Module: Mathlib.Algebra.Ring.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ 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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ 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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ 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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ 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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
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 : β)
nsmul : ∀ (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 : β) : β)
⊢ Semiring α

Tactic:
apply e.injective.semiring _

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

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply