awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
⊢ Field α
have div₁ : ∀ (x y : α), (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ Field α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
⊢ Field α
have zsmul : ∀ (n : ℤ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
⊢ Field α
have nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
⊢ Field α
have qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
⊢ Field α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ Field α
have zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ Field α
have natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
natCast : ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
⊢ Field α
have intCast : ∀ (n : ℤ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑n : α) : β) ((↑n : β) : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (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 : β) : β)
⊢ Field α
have nnratCast₁ : ∀ (q : ℚ≥0), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ 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 : β)
inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((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 : β)
nnqsmul₁ : ∀ (q : ℚ≥0) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
qsmul₁ : ∀ (q : ℚ) (x : α), (e : (a : α) → β) (q • x) = HSMul.hSMul (β := β) q ((e : (a : α) → β) x : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (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 : β) : β)
nnratCast₁ : ∀ (q : ℚ≥0), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
⊢ Field α
have ratCast₁ : ∀ (q : ℚ), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
Tactic: apply e.injective.field _
-- Lean 4 proof step from Mathlib.Algebra.Field.ZMod (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1
have obtain : ∀ (k : ℕ) (h : Ne (α := ZMod p) (↑k : ZMod p) 0), HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)⁻¹ = 1
Tactic: obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Field.ZMod (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
⊢ HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)⁻¹ = 1
have h₁ : k.Coprime p
Tactic: apply coe_mul_inv_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Field.ZMod (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
⊢ k.Coprime p
have h₁ : p.Coprime k
Tactic: apply Nat.Coprime.symm
-- Lean 4 proof step from Mathlib.Algebra.Field.ZMod (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
⊢ p.Coprime k
have h₁ : ¬p ∣ k
Tactic: rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
-- Lean 4 proof step from Mathlib.Algebra.Field.ZMod (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
h₁ : ¬p ∣ k
⊢ p.Coprime k
have h₂ : ¬Eq (α := ZMod p) (↑k : ZMod p) 0
Tactic: rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ Set.Finite.{u_1} (α := α) (mulSupport (M := M × M') fun (a : α) ↦ (f a, g a))
have rw : (mulSupport f ∪ mulSupport g).Finite
Tactic: rw [mulSupport_prodMk f g]
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
⊢ (mulSupport f).Finite
have refine : ∀ (i : ι) (hi : i ∈ mulSupport f),
  Membership.mem (γ := Set ι) (⋃ (i : α), mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x i) i
Tactic: refine (Set.finite_iUnion hf).subset fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
i : ι
hi : i ∈ mulSupport f
⊢ Membership.mem (γ := Set ι) (⋃ (i : α), mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x i) i
have simp : ∀ (hi : f i ≠ 1), ∃ (i_1 : α), f i i_1 ≠ 1
Tactic: simp only [mem_mulSupport, Set.mem_iUnion] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.FiniteSupport.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a)
have refine : ∀ (a : α)
  (ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a) a),
  Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
Tactic: refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_