awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
pos :
  ∀ (hx0 : dx = 0),
    Membership.mem (γ := Set K)
      {z : K |
        ∃ (x : K),
          Membership.mem (γ := Subring K) (Subring.closure s) x ∧
            ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
      (nx / dx + ny / dy)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have neg : ∀ (hx0 : ¬dx = 0),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
Tactic: by_cases hx0 : dx = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : dx = 0
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos : Membership.mem (γ := Set K)
  {z : K |
    ∃ (x : K),
      Membership.mem (γ := Subring K) (Subring.closure s) x ∧
        ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
  (nx / 0 + ny / dy)
Tactic: rwa [hx0, div_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : dx = 0
pos :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / 0 + ny / dy)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos₁ : Membership.mem (γ := Set K)
  {z : K |
    ∃ (x : K),
      Membership.mem (γ := Subring K) (Subring.closure s) x ∧
        ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
  (0 + ny / dy)
Tactic: rwa [hx0, div_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : ¬dx = 0
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos : ∀ (hy0 : dy = 0),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
Tactic: by_cases hy0 : dy = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : ¬dx = 0
pos :
  ∀ (hy0 : dy = 0),
    Membership.mem (γ := Set K)
      {z : K |
        ∃ (x : K),
          Membership.mem (γ := Subring K) (Subring.closure s) x ∧
            ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
      (nx / dx + ny / dy)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have neg : ∀ (hy0 : ¬dy = 0),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
Tactic: by_cases hy0 : dy = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : ¬dx = 0
hy0 : dy = 0
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos : Membership.mem (γ := Set K)
  {z : K |
    ∃ (x : K),
      Membership.mem (γ := Subring K) (Subring.closure s) x ∧
        ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
  (nx / dx + ny / 0)
Tactic: rwa [hy0, div_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
hx0 : ¬dx = 0
hy0 : dy = 0
pos :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / 0)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos₁ : Membership.mem (γ := Set K)
  {z : K |
    ∃ (x : K),
      Membership.mem (γ := Subring K) (Subring.closure s) x ∧
        ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
  (nx / dx + 0)
Tactic: rwa [hy0, div_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
inst : Field K
s : Set K
x : K
⊢ Membership.mem (γ := Subfield K) (closure s) x ↔
    ∃ (y : K),
      Membership.mem (γ := Subring K) (Subring.closure s) y ∧
        ∃ (z : K), Membership.mem (γ := Subring K) (Subring.closure s) z ∧ y / z = x
have rw : Membership.mem (γ := Subfield K) (commClosure s) x ↔
  ∃ (y : K),
    Membership.mem (γ := Subring K) (Subring.closure s) y ∧
      ∃ (z : K), Membership.mem (γ := Subring K) (Subring.closure s) z ∧ y / z = x
Tactic: rw [← commClosure_eq_closure]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Defs (goal)
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
p q : Subfield K
h : Eq.{u + 1} (α := Set K) ((fun (s : Subfield K) ↦ s.carrier) p) ((fun (s : Subfield K) ↦ s.carrier) q)
⊢ p = q
have mk : ∀ (toSubring : Subring K) (inv_mem' : ∀ (x : K), x ∈ toSubring.carrier → x⁻¹ ∈ toSubring.carrier)
  (h :
    Eq.{u + 1} (α := Set K) ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring, inv_mem' := inv_mem' })
      ((fun (s : Subfield K) ↦ s.carrier) q)),
  { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Defs (goal)
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
q : Subfield K
toSubring : Subring K
inv_mem' : ∀ (x : K), x ∈ toSubring.carrier → x⁻¹ ∈ toSubring.carrier
h :
  Eq.{u + 1} (α := Set K) ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring, inv_mem' := inv_mem' })
    ((fun (s : Subfield K) ↦ s.carrier) q)
⊢ { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = q
have mk : ∀ (toSubring_1 : Subring K) (inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier → x⁻¹ ∈ toSubring_1.carrier)
  (h :
    Eq.{u + 1} (α := Set K) ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring, inv_mem' := inv_mem' })
      ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring_1, inv_mem' := inv_mem'_1 })),
  { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = { toSubring := toSubring_1, inv_mem' := inv_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Defs (goal)
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
toSubring : Subring K
inv_mem' : ∀ (x : K), x ∈ toSubring.carrier → x⁻¹ ∈ toSubring.carrier
toSubring_1 : Subring K
inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier → x⁻¹ ∈ toSubring_1.carrier
h :
  Eq.{u + 1} (α := Set K) ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring, inv_mem' := inv_mem' })
    ((fun (s : Subfield K) ↦ s.carrier) { toSubring := toSubring_1, inv_mem' := inv_mem'_1 })
⊢ { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = { toSubring := toSubring_1, inv_mem' := inv_mem'_1 }
have mk : toSubring = toSubring_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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
⊢ DivisionRing α
have zero : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have one : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have add : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have neg : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (-x) : β) (-(e : (a : α) → β) x : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have sub : ∀ (x y : α), (e : (a : α) → β) (x - y) = HSub.hSub (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have inv₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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)⁻¹ : β)
⊢ DivisionRing α
have div₁ : ∀ (x y : α), (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.divisionRing _
-- Lean 4 proof step from Mathlib.Algebra.Field.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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 : β)
⊢ DivisionRing α
have nsmul : ∀ (n : ℕ) (x : α), (e : (a : α) → β) (n • x) = HSMul.hSMul (β := β) n ((e : (a : α) → β) x : β)
Tactic: apply e.injective.divisionRing _