awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Field.Subfield.Basic
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)

Tactic:
exact
      ⟨nx * dy + dx * ny, Subring.add_mem _ (Subring.mul_mem _ hnx hdy) (Subring.mul_mem _ hdx hny),
        dx * dy, Subring.mul_mem _ hdx hdy, (div_add_div nx ny hx0 hy0).symm⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
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
x y : K
hy : Membership.mem (γ := Subring K) (Subring.closure s) y
z : K
hz : Membership.mem (γ := Subring K) (Subring.closure s) z
x_eq : y / z = x
⊢ 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}
    (-x)

Tactic:
⟨-y, Subring.neg_mem _ hy, z, hz, x_eq ▸ neg_div _ _⟩

Premises used: neg_div, Set.Mem, setOf, Subring.neg_mem, Eq.rec, And.intro, Exists.intro, Neg.neg
-- Module: Mathlib.Algebra.Field.Subfield.Basic
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
x y : K
hy : Membership.mem (γ := Subring K) (Subring.closure s) y
z : K
hz : Membership.mem (γ := Subring K) (Subring.closure s) z
x_eq : y / z = x
⊢ 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}
    (-x)

Tactic:
exact ⟨-y, Subring.neg_mem _ hy, z, hz, x_eq ▸ neg_div _ _⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
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
x y : K
hy : Membership.mem (γ := Subring K) (Subring.closure s) y
z : K
hz : Membership.mem (γ := Subring K) (Subring.closure s) z
x_eq : y / z = x
⊢ 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}
    x⁻¹

Tactic:
⟨z, hz, y, hy, x_eq ▸ (inv_div _ _).symm⟩

Premises used: Set.Mem, setOf, Eq.rec, And.intro, Exists.intro, inv_div, Eq.symm
-- Module: Mathlib.Algebra.Field.Subfield.Basic
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
x y : K
hy : Membership.mem (γ := Subring K) (Subring.closure s) y
z : K
hz : Membership.mem (γ := Subring K) (Subring.closure s) z
x_eq : y / z = x
⊢ 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}
    x⁻¹

Tactic:
exact ⟨z, hz, y, hy, x_eq ▸ (inv_div _ _).symm⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Set K
⊢ Eq (α := Subfield K) (commClosure s) (closure s)

Tactic:
le_antisymm
    (fun _ ⟨_, hy, _, hz, eq⟩ ↦ eq ▸ div_mem (subring_closure_le s hy) (subring_closure_le s hz))
    (closure_le.mpr fun x hx ↦ ⟨x, Subring.subset_closure hx, 1, Subring.one_mem _, div_one x⟩)

Premises used: Iff.mpr, Subfield.closure_le, Subring.subset_closure, le_antisymm, And.intro, Exists.intro, OfNat.ofNat, div_one, Subring.closure, Subring.one_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Set K
x : K
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
⊢ 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

Tactic:
rw [← commClosure_eq_closure]

Premises used: _private.0.Subfield.commClosure_eq_closure
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Set K
x : K
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Subfield L
⊢ map f (comap f s) = s ⊓ f.fieldRange

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Subfield L
h : s ≤ f.fieldRange
⊢ map f (comap f s) = s

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f s

Premises used: inf_of_le_left, Subfield.map_comap_eq
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
hf : Function.Surjective.{u + 1, v + 1} (α := K) (β := L) (⇑f : (a : K) → L)
s : Subfield L
⊢ map f (comap f s) = s

Tactic:
SetLike.coe_injective (Set.image_preimage_eq _ hf)

Premises used: Set.image_preimage_eq, SetLike.coe_injective
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Subfield K
⊢ comap f (map f s) = s

Tactic:
SetLike.coe_injective (Set.preimage_image_eq _ f.injective)

Premises used: SetLike.coe_injective, RingHom.injective, Set.preimage_image_eq
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
X : Type u_1
inst_1 : SMul K X
F : Subfield K
g : ↥F
m : X
⊢ g • m = (↑g : K) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
X : Type u_2
Y : Type u_1
inst_3 : SMul K Y
inst_4 : SMul X Y
inst_5 : SMulCommClass K X Y
F : Subfield K
⊢ SMulCommClass.{u, u_2, u_1} (↥F) X Y

Tactic:
inferInstanceAs (SMulCommClass F.toSubsemiring X Y)

Premises used: _private.0.Subfield.smulCommClass_left._proof_1
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
X : Type u_1
Y : Type u_2
inst_3 : SMul X Y
inst_4 : SMul K Y
inst_5 : SMulCommClass X K Y
F : Subfield K
⊢ SMulCommClass.{u_1, u, u_2} X (↥F) Y

Tactic:
inferInstanceAs (SMulCommClass X F.toSubsemiring Y)

Premises used: _private.0.Subfield.smulCommClass_right._proof_1
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
X : Type u_1
Y : Type u_2
inst_3 : SMul X Y
inst_4 : SMul K X
inst_5 : SMul K Y
inst_6 : IsScalarTower K X Y
F : Subfield K
⊢ IsScalarTower.{u, u_1, u_2} (↥F) X Y

Tactic:
inferInstanceAs (IsScalarTower F.toSubsemiring X Y)

Premises used: _private.0.Subfield.instIsScalarTowerSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
X : Type u_1
Y : ?m.2
inst_3 : SMul K X
inst_4 : FaithfulSMul K X
F : Subfield K
⊢ FaithfulSMul.{u, u_1} (↥F) X

Tactic:
inferInstanceAs (FaithfulSMul F.toSubsemiring X)

Premises used: _private.0.Subfield.instFaithfulSMulSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
S : Type u_1
inst_3 : SetLike S K
h : SubfieldClass S K
⊢ SubgroupClass S K

Tactic:
{ h with }

Premises used: SubgroupClass.mk
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
⊢ (↑q : K) ∈ s

Tactic:
simpa only [NNRat.cast_def] using div_mem (natCast_mem s q.num) (natCast_mem s q.den)

Premises used: NNRat.cast_def, div_mem, natCast_mem, NNRat.num, NNRat.den
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ
⊢ (↑q : K) ∈ s

Tactic:
simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den)

Premises used: Rat.num, intCast_mem, div_mem, natCast_mem, Rat.den, Rat.cast_def
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
⊢ Eq.{u + 1} (α := K) (↑(↑q : ↥s) : K) (↑q : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
x : ℚ
⊢ Eq.{u + 1} (α := K) (↑(↑x : ↥s) : K) (↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ≥0
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
simpa only [NNRat.smul_def] using mul_mem (nnratCast_mem _ _) hx

Premises used: SubfieldClass.nnratCast_mem, NNRat.smul_def, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx

Premises used: SubfieldClass.ratCast_mem, Rat.smul_def, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
b : Bool
n m : ℕ
⊢ OfScientific.ofScientific n b m ∈ s

Tactic:
SubfieldClass.nnratCast_mem s (OfScientific.ofScientific n b m)

Premises used: Set.Mem, OfScientific.ofScientific, SubfieldClass.nnratCast_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
x : ↥s
⊢ (↑(q • x) : K) = q • (↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Type u_1
inst_1 : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ
x : ↥s
⊢ (↑(q • x) : K) = q • (↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
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)
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
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Field.Subfield.Defs
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)
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 }
⊢ { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Field.Subfield.Defs
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 })
mk : toSubring = toSubring_1
⊢ { toSubring := toSubring, inv_mem' := inv_mem' : Subfield K } = { toSubring := toSubring_1, inv_mem' := inv_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Field.Subfield.Defs
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_1

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Field.Subfield.Defs
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_1

Tactic:
exact SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Subring K
x : K
h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier
⊢ x ∈ { toSubring := S, inv_mem' := h : Subfield K } ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Subring K
h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier
⊢ (↑{ toSubring := S, inv_mem' := h : Subfield K } : Set K) = (↑S : Set K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S S' : Subring K
h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier
h' : ∀ (x : K), x ∈ S'.carrier → x⁻¹ ∈ S'.carrier
⊢ { toSubring := S, inv_mem' := h : Subfield K } ≤ { toSubring := S', inv_mem' := h' } ↔ S ≤ S'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S T : Subfield K
h : ∀ (x : K), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Subfield K
s : Set K
hs : s = (↑S : Set K)
⊢ (↑(S.copy s hs) : Set K) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Subfield K
s : Set K
hs : s = (↑S : Set K)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ (↑s.toSubring : Set K) = (↑s : Set K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s.toSubring ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ 1 ∈ s

Tactic:
one_mem s

Premises used: Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ 0 ∈ s

Tactic:
zero_mem s

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : K
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : K
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s → -x ∈ s

Tactic:
neg_mem

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : K
⊢ x ∈ s → y ∈ s → x - y ∈ s

Tactic:
sub_mem

Premises used: sub_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s → x⁻¹ ∈ s

Tactic:
inv_mem

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : K
⊢ x ∈ s → y ∈ s → x / y ∈ s

Tactic:
div_mem

Premises used: div_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
n : ℕ
⊢ x ^ n ∈ s

Tactic:
pow_mem hx n

Premises used: pow_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
n : ℤ
⊢ n • x ∈ s

Tactic:
zsmul_mem hx n

Premises used: zsmul_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
n : ℤ
⊢ (↑n : K) ∈ s

Tactic:
intCast_mem s n

Premises used: intCast_mem, Set.Mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
n : ℤ
⊢ x ^ n ∈ s

Tactic:
zpow_mem hx n

Premises used: zpow_mem
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : ↥s
⊢ (↑(x + y) : K) = (↑x : K) + (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : ↥s
⊢ (↑(x - y) : K) = (↑x : K) - (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : ↥s
⊢ (↑(-x) : K) = -(↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : ↥s
⊢ (↑(x * y) : K) = (↑x : K) * (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x y : ↥s
⊢ (↑(x / y) : K) = (↑x : K) / (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : ↥s
⊢ (↑x⁻¹ : K) = (↑x : K)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ Eq.{u + 1} (α := K) (↑0 : K) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ Eq.{u + 1} (α := K) (↑1 : K) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : ↥s
⊢ (s.subtype : (a : ↥s) → K) x = (↑x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ Function.Injective (α := ↥s) (β := K) (⇑s.subtype : (a : ↥s) → K)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ Eq (α := (a : ↥s) → K) (⇑s.subtype : (a : ↥s) → K) (Subtype.val (p := fun (x : K) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
S : Subfield K
⊢ S.subtype = S.subtype

Tactic:
rfl

Premises used: Subfield.subtype, Set.Mem, Subring.subtype, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s.toSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ (↑s.toSubmonoid : Set K) = (↑s : Set K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
x : K
⊢ x ∈ s.toAddSubgroup ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Field.Subfield.Defs
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ (↑s.toAddSubgroup : Set K) = (↑s : Set K)

Tactic:
rfl

Premises used: rfl