awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalNonAssocSemiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalNonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalNonAssocSemiring α
have nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalNonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ NonUnitalSemiring α
have zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonUnitalSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalSemiring α
have add₁ : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalSemiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalSemiring α
have nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : AddGroupWithOne β
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) (↑(↑n : ℤ) : β) : α) ((↑n : α) : α)
have simp : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) (↑n : β) : α) ((↑n : α) : α)
Tactic: simp only [Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ NonAssocSemiring α
have zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonAssocSemiring α
have one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonAssocSemiring α
have add : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonAssocSemiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonAssocSemiring α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonAssocSemiring α
have natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.nonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ Semiring α
have zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ Semiring α
have one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ Semiring α
have add : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ Semiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ Semiring α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ Semiring α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ Semiring α
have natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.semiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalCommSemiring α
have zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonUnitalCommSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommSemiring β
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 : β)
⊢ NonUnitalCommSemiring α
have add₁ : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalCommSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommSemiring β
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 : β)
⊢ NonUnitalCommSemiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalCommSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalCommSemiring β
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 : β)
⊢ NonUnitalCommSemiring α
have nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalCommSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommSemiring α
have zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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 : β)
⊢ CommSemiring α
have one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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 : β)
⊢ CommSemiring α
have add : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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 : β)
⊢ CommSemiring α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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 : β)
⊢ CommSemiring α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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 : β)
⊢ CommSemiring α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : CommSemiring β
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
⊢ CommSemiring α
have natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.commSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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
⊢ NonUnitalNonAssocRing α
have zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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 : β)
⊢ NonUnitalNonAssocRing α
have add₁ : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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 : β)
⊢ NonUnitalNonAssocRing α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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 : β)
⊢ NonUnitalNonAssocRing α
have neg₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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 : β)
⊢ NonUnitalNonAssocRing α
have sub₁ : ∀ (x y : α), (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocRing β
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 : β)
⊢ NonUnitalNonAssocRing α
have nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalNonAssocRing _