awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
ι : Sort u_1
f : K →+* L
s : ι → Subfield K
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: Subfield.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
s t : Subfield K
f : K →+* L
⊢ map f (s ⊓ t) = map f s ⊓ map f t

Tactic:
SetLike.coe_injective (Set.image_inter f.injective)

Premises used: Set.image_inter, SetLike.coe_injective, RingHom.injective
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
ι : Sort u_1
inst_2 : Nonempty ι
f : K →+* L
s : ι → Subfield K
a : (↑(map f (iInf s)) : Set L) = (↑(⨅ (i : ι), map f (s i)) : Set L)
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
ι : Sort u_1
inst_2 : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ (↑(map f (iInf s)) : Set L) = (↑(⨅ (i : ι), map f (s i)) : Set L)

Tactic:
simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, RingHom.injective, Set.injOn_of_injective
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
s t : Subfield L
f : K →+* L
⊢ comap f (s ⊓ t) = comap f s ⊓ comap f t

Tactic:
(gc_map_comap f).u_inf

Premises used: Subfield.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
ι : Sort u_1
f : K →+* L
s : ι → Subfield L
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: GaloisConnection.u_iInf, Subfield.gc_map_comap
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Subfield.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: Subfield.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := Subring.copy (⨆ (i : ι), (S i).toSubring) (⋃ (i : ι), (↑(S i).toSubring : Set K)) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ iSup S = s

Tactic:
have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := Subring.copy (⨆ (i : ι), (S i).toSubring) (⋃ (i : ι), (↑(S i).toSubring : Set K)) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
this : iSup S = s
⊢ Membership.mem (γ := Subfield K) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
this ▸ Set.mem_iUnion

Premises used: Set.Mem, Set.mem_iUnion, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := Subring.copy (⨆ (i : ι), (S i).toSubring) (⋃ (i : ι), (↑(S i).toSubring : Set K)) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
this : iSup S = s
⊢ Membership.mem (γ := Subfield K) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
exact this ▸ Set.mem_iUnion
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set K) ↔ Membership.mem (γ := Set K) (⋃ (i : ι), (↑(S i) : Set K)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Subfield.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
⊢ Nonempty.{u + 1} (↑S : Type u)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
this : Nonempty.{u + 1} (↑S : Type u)
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Premises used: Subtype.exists, exists_prop, DirectedOn.directed_val, Subfield.mem_iSup_of_directed, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
⊢ x ∈ (↑(sSup S) : Set K) ↔ Membership.mem (γ := Set K) (⋃ s ∈ S, (↑s : Set K)) x

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Premises used: Subfield.mem_sSup_of_directedOn
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
x : K
⊢ Eq.{v + 1} (α := L) ((↑((f.rangeRestrictField : (a : K) → ↥f.fieldRange) x) : L) : L) ((f : (a : K) → L) x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ Function.Bijective.{u + 1, v + 1} (α := K) (β := ↥f.fieldRange) (⇑f.rangeRestrictField : (a : K) → ↥f.fieldRange)

Tactic:
(Equiv.ofInjective f f.injective).bijective

Premises used: Equiv.bijective, Set.Mem, setOf, RingHom.injective, Equiv.ofInjective, Set.range, DFunLike.coe
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
rw :
  (↑((f.rangeRestrictFieldEquiv : (a : K) → ↥f.fieldRange)
          ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x)) :
      L) =
    (↑x : L)
rw₁ rw₂ : (↑x : L) = (↑x : L)
⊢ (f : (a : K) → L) ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x : K) = (↑x : L)

Tactic:
rw [← rangeRestrictFieldEquiv_apply_coe, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, RingHom.rangeRestrictFieldEquiv_apply_coe
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
L : Type v
inst_1 : Semiring L
f g : K →+* L
x : K
⊢ x ∈ f.eqLocusField g ↔ Eq.{v + 1} (α := L) ((f : (a : K) → L) x : L) ((g : (a : K) → L) x : L)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
L : Type v
inst_1 : Semiring L
f g : K →+* L
s : Set K
h : Set.EqOn.{u, v} (β := L) (⇑f : (a : K) → L) (⇑g : (a : K) → L) s
⊢ Set.EqOn.{u, v} (β := L) (⇑f : (a : K) → L) (⇑g : (a : K) → L) (↑(closure s) : Set K)

Tactic:
show closure s ≤ f.eqLocusField g from closure_le.2 h

Premises used: Iff.mpr, Subfield.closure_le, Set.Mem, setOf, Set.EqOn
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
L : Type v
inst_1 : Semiring L
f g : K →+* L
h : Set.EqOn.{u, v} (β := L) (⇑f : (a : K) → L) (⇑g : (a : K) → L) (↑⊤ : Set K)
⊢ f = g

Tactic:
ext fun _ => h trivial

Premises used: trivial, RingHom.ext
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
L : Type v
inst_1 : Semiring L
s : Set K
hs : Eq (α := Subfield K) (closure s) ⊤
f g : K →+* L
h : Set.EqOn.{u, v} (β := L) (⇑f : (a : K) → L) (⇑g : (a : K) → L) s
⊢ f = g

Tactic:
eq_of_eqOn_subfield_top <| hs ▸ eqOn_field_closure h

Premises used: RingHom.eq_of_eqOn_subfield_top, RingHom.eqOn_field_closure, Eq.rec
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Set L
⊢ closure ((⇑f : (a : K) → L) ⁻¹' s) ≤ comap f (closure s)

Tactic:
closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, Subfield.closure_le, SetLike.mem_coe, Subfield.subset_closure, Subfield.mem_comap
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Set K
⊢ map f (closure s) = closure ((⇑f : (a : K) → L) '' s)

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subfield.gi L).gc (Subfield.gi K).gc
    fun _ ↦ rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Subfield.gc_map_comap, Set.image_preimage, rfl, Subfield.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ s.subtype.fieldRange = s

Tactic:
SetLike.ext' <| (coe_rangeS _).trans Subtype.range_coe

Premises used: Subtype.range_coe, SetLike.ext', Eq.trans, RingHom.coe_rangeS
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Subfield K
m : Multiset K
⊢ (∀ a ∈ m, a ∈ s) → m.prod ∈ s

Tactic:
multiset_prod_mem m

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Subfield K
ι : Type u_1
t : Finset ι
f : ι → K
h : ∀ c ∈ t, f c ∈ s
⊢ ∏ i ∈ t, f i ∈ s

Tactic:
prod_mem h

Premises used: prod_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : Field K
s : Subfield K
⊢ algebraMap (↥s) K = s.subtype

Tactic:
rfl

Premises used: rfl
-- 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
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) 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))

Tactic:
⟨nx * ny, Subring.mul_mem _ hnx hny, dx * dy, Subring.mul_mem _ hdx hdy,
      (div_mul_div_comm _ _ _ _).symm⟩

Premises used: HMul.hMul, Set.Mem, div_mul_div_comm, setOf, And.intro, Exists.intro, Eq.symm, Subring.mul_mem
-- 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
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) 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))

Tactic:
exact ⟨nx * ny, Subring.mul_mem _ hnx hny, dx * dy, Subring.mul_mem _ hdx hdy,
      (div_mul_div_comm _ _ _ _).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
a b : K
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}
    a
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}
    b
obtain :
  ∀ (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)),
    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 + b)
⊢ 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}
    (a + b)

Tactic:
obtain ⟨nx, hnx, dx, hdx, rfl⟩ := id x_mem

Premises used: id, rfl
-- 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
b : K
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}
    b
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)
obtain :
  ∀ (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)),
    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 + b)

Tactic:
obtain ⟨ny, hny, dy, hdy, rfl⟩ := id y_mem

Premises used: id, rfl
-- 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)
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)
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)
⊢ 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
-- 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
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)
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)
pos₂ pos₃ pos₄ 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}
    (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)

Tactic:
rwa [hx0, div_zero, zero_add]

Premises used: zero_add, div_zero
-- 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
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)
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)
⊢ 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
-- 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
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)
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)
pos₂ pos₃ pos₄ 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)
⊢ 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:
rwa [hy0, div_zero, add_zero]

Premises used: add_zero, div_zero
-- 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:
⟨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⟩

Premises used: HMul.hMul, Subring.add_mem, Set.Mem, setOf, HAdd.hAdd, div_add_div, And.intro, Exists.intro, Eq.symm, Subring.mul_mem