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 : Ring β
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 : β) : β)
⊢ Ring α
have intCast : ∀ (n : ℤ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.ring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ NonUnitalCommRing α
have zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have add₁ : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have neg₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have sub₁ : ∀ (x y : α), (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have nsmul₁ : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ NonUnitalCommRing α
have zsmul₁ : ∀ (n : ℤ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.nonUnitalCommRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ CommRing α
have zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have add : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have neg : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have sub : ∀ (x y : α), (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have zsmul : ∀ (n : ℤ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β)
⊢ CommRing α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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
⊢ CommRing α
have natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
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 : β) : β)
⊢ CommRing α
have intCast : ∀ (n : ℤ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.commRing _
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
a : αˣ
⊢ (↑a : α) = -1 ↔ a = -1
have rw : (↑a : α) = (↑(-1) : α) ↔ a = -1
Tactic: rw [← Units.coe_neg_one, val_inj]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
a : αˣ
rw : (↑a : α) = (↑(-1) : α) ↔ a = -1
⊢ (↑a : α) = -1 ↔ a = -1
have rw₁ : a = -1 ↔ a = -1
Tactic: rw [← Units.coe_neg_one, val_inj]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
have rw : a /ₚ u + -(b /ₚ u) = (a - b) /ₚ u
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : a /ₚ u + -(b /ₚ u) = (a - b) /ₚ u
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
have rw₁ : a /ₚ u + -(b /ₚ u) = (a + -b) /ₚ u
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : a /ₚ u + -(b /ₚ u) = (a - b) /ₚ u
rw₁ : a /ₚ u + -(b /ₚ u) = (a + -b) /ₚ u
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
have rw₂ : a /ₚ u + -b /ₚ u = (a + -b) /ₚ u
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
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
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
have rw₃ : (a + -b) /ₚ u = (a + -b) /ₚ u
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * (↑u : α)) /ₚ u
have simp : b = b * (↑u : α) * (↑u⁻¹ : α)
Tactic: simp only [divp, sub_mul, sub_right_inj]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
⊢ b = b * (↑u : α) * (↑u⁻¹ : α)
have rw : b = b * ((↑u : α) * (↑u⁻¹ : α))
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : b = b * ((↑u : α) * (↑u⁻¹ : α))
⊢ b = b * (↑u : α) * (↑u⁻¹ : α)
have rw₁ : b = b * 1
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : b = b * ((↑u : α) * (↑u⁻¹ : α))
rw₁ : b = b * 1
⊢ b = b * (↑u : α) * (↑u⁻¹ : α)
have rw₂ : b = b
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * (↑u₂ : α) + (↑u₁ : α) * b) /ₚ (u₁ * u₂)
have simp : a * (↑u₁⁻¹ : α) + b * (↑u₂⁻¹ : α) =
  a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₁ : α) * b * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α))
Tactic: simp only [divp, add_mul, mul_inv_rev, val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * (↑u₁⁻¹ : α) + b * (↑u₂⁻¹ : α) =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₁ : α) * b * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α))
have rw : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
  a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
Tactic: rw [mul_comm (↑u₁ * b), mul_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
  a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₁ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
  a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₂ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
  a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₃ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
  a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₃ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₄ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]