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
f : K →+* L
s : Subfield K
y : L
⊢ Membership.mem (γ := Subfield L)
      (let __src : Subring L := Subring.map f s.toSubring;
      { toSubring := __src, inv_mem' := ⋯ })
      y ↔
    ∃ x ∈ s, (f : (a : K) → L) x = y

Tactic:
simp only [mem_mk, Subring.mem_map, mem_toSubring]

Premises used: Subfield.mem_toSubring, Subring.mem_map, Subfield.mem_mk
-- 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
x : K
⊢ Membership.mem (α := L) (↑(map f s) : Set L) ((f : (a : K) → L) x : L) ↔ x ∈ s

Tactic:
simp [Function.Injective.mem_set_image (f := f) f.injective]

Premises used: RingHom.injective, Function.Injective.mem_set_image
-- 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
s : Subfield K
g : L →+* M
f : K →+* L
⊢ map g (map f s) = map (g.comp f) s

Tactic:
SetLike.ext' <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.ext'
-- 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
t : Subfield L
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: Subfield.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ (↑f.fieldRange : Set L) = Set.range.{v, u + 1} (ι := K) (⇑f : (a : K) → L)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
y : L
⊢ y ∈ f.fieldRange ↔ ∃ (x : K), (f : (a : K) → L) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
h : ∀ (x : L), x ∈ f.fieldRange ↔ x ∈ Subfield.map f ⊤
⊢ f.fieldRange = Subfield.map f ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
x : L
⊢ x ∈ f.fieldRange ↔ x ∈ Subfield.map f ⊤

Tactic:
simp
-- 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
g : L →+* M
f : K →+* L
⊢ Subfield.map g f.fieldRange = (g.comp f).fieldRange

Tactic:
simpa only [fieldRange_eq_map] using (⊤ : Subfield K).map_map g f

Premises used: Subfield.map_map, RingHom.fieldRange_eq_map, Top.top
-- 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
⊢ Membership.mem (α := L) f.fieldRange ((f : (a : K) → L) x : L)

Tactic:
exists_apply_eq_apply _ _

Premises used: Set.Mem, setOf, Set.range, exists_apply_eq_apply
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ f.fieldRange = ⊤ ↔ Function.Surjective.{u + 1, v + 1} (α := K) (β := L) (⇑f : (a : K) → L)

Tactic:
SetLike.ext'_iff.trans Set.range_eq_univ

Premises used: Set.range_eq_univ, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
p p' : Subfield K
⊢ (↑(p ⊓ p') : Set K) = p.carrier ∩ p'.carrier

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
p p' : Subfield K
x : K
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- 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
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
apply : ∀ p ∈ toSubring '' S, x⁻¹ ∈ p
⊢ x⁻¹ ∈ (sInf (toSubring '' S)).carrier

Tactic:
apply Subring.mem_sInf.mpr

Premises used: Iff.mpr, Subring.mem_sInf
-- 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
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
p : Subfield K
p_mem : p ∈ S
⊢ x⁻¹ ∈ p.toSubring

Tactic:
p.inv_mem (Subring.mem_sInf.mp hx p.toSubring ⟨p, p_mem, rfl⟩)

Premises used: Set.Mem, Subfield.inv_mem, And.intro, Exists.intro, Iff.mp, Subring.mem_sInf, Subfield.toSubring, 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
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
p : Subfield K
p_mem : p ∈ S
⊢ x⁻¹ ∈ p.toSubring

Tactic:
exact p.inv_mem (Subring.mem_sInf.mp hx p.toSubring ⟨p, p_mem, rfl⟩)

Premises used: Subfield.inv_mem, And.intro, Exists.intro, Iff.mp, Subring.mem_sInf, Subfield.toSubring, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
⊢ (↑(sInf (toSubring '' S)) : Set K) = ⋂ s ∈ S, (↑s : Set K)

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
x : K
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simpa only [Set.mem_iInter] using Set.ext_iff.1 (coe_sInf S) x

Premises used: Set.mem_iInter, Subfield.coe_sInf, Iff.mp, Set.ext_iff
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
S : ι → Subfield K
⊢ (↑(⨅ (i : ι), S i) : Set K) = ⋂ (i : ι), (↑(S i) : Set K)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Subfield.coe_sInf, Set.biInter_range
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
S : ι → Subfield K
x : K
⊢ Membership.mem (γ := Subfield K) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: Subfield.mem_sInf, iInf, Set.forall_mem_range
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set (Subfield K)
h : ∀ (x : K), x ∈ (sInf s).toSubring ↔ Membership.mem (γ := Subring K) (⨅ t ∈ s, t.toSubring) x
⊢ (sInf s).toSubring = ⨅ t ∈ s, t.toSubring

Tactic:
ext x
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set (Subfield K)
x : K
⊢ x ∈ (sInf s).toSubring ↔ Membership.mem (γ := Subring K) (⨅ t ∈ s, t.toSubring) x

Tactic:
simp [mem_sInf]

Premises used: Subfield.mem_sInf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
⊢ ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t

Tactic:
simp [SetLike.coe_subset_coe]

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
⊢ ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t

Tactic:
have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ IsGLB S (sInf S)

Tactic:
IsGLB.of_image this ?_

Premises used: IsGLB.of_image
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
refine : IsGLB ((fun {x : Subfield K} ↦ (↑x : Set K)) '' S) (↑(sInf S) : Set K)
⊢ IsGLB S (sInf S)

Tactic:
refine IsGLB.of_image this ?_

Premises used: IsGLB.of_image
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ IsGLB (SetLike.coe '' S) (⨅ x ∈ S, (↑x : Set K))

Tactic:
isGLB_biInf (s := S) (f := SetLike.coe)

Premises used: isGLB_biInf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
h : (↑(sInf S) : Set K) = ⨅ x ∈ S, (↑x : Set K)
⊢ IsGLB ((fun {x : Subfield K} ↦ (↑x : Set K)) '' S) (↑(sInf S) : Set K)

Tactic:
convert! isGLB_biInf (s := S) (f := SetLike.coe)

Premises used: isGLB_biInf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ (↑(sInf S) : Set K) = ⨅ x ∈ S, (↑x : Set K)

Tactic:
coe_sInf _

Premises used: Set.iInter, Subfield.coe_sInf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ (↑(sInf S) : Set K) = ⨅ x ∈ S, (↑x : Set K)

Tactic:
exact coe_sInf _

Premises used: Subfield.coe_sInf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
x : K
s : Set K
⊢ Membership.mem (γ := Subfield K) (closure s) x ↔ ∀ (S : Subfield K), s ⊆ (↑S : Set K) → x ∈ S

Tactic:
mem_sInf

Premises used: Subfield.mem_sInf, Set.Mem, setOf
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
⊢ s ⊆ (↑(closure s) : Set K)

Tactic:
fun _ hx => mem_closure.2 fun _ hS => hS hx

Premises used: Iff.mpr, Subfield.mem_closure, Set.Subset
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
x : K
hx : x ∈ s
⊢ Membership.mem (γ := Subfield K) (closure s) x

Tactic:
subset_closure hx

Premises used: Subfield.subset_closure
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
⊢ LE.le (α := Subring K) (Subring.closure s) (toSubring (closure s))

Tactic:
Subring.closure_le.mpr subset_closure

Premises used: Iff.mpr, Subfield.subset_closure, Subring.closure_le
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
P : K
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: Subfield.subset_closure, Not
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
t : Subfield K
⊢ closure s ≤ t ↔ s ⊆ (↑t : Set K)

Tactic:
⟨Set.Subset.trans subset_closure, fun h _ hx => mem_closure.mp hx t h⟩

Premises used: Subfield.mem_closure, Set.Subset.trans, Iff.intro, Iff.mp, Subfield.subset_closure
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s t : Set K
h : s ⊆ t
⊢ LE.le (α := Subfield K) (closure s) (closure t)

Tactic:
closure_le.2 <| Set.Subset.trans h subset_closure

Premises used: Iff.mpr, Subfield.closure_le, Set.Subset.trans, Subfield.subset_closure
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
t : Subfield K
h₁ : s ⊆ (↑t : Set K)
h₂ : t ≤ closure s
⊢ closure s = t

Tactic:
le_antisymm (closure_le.2 h₁) h₂

Premises used: Iff.mpr, Subfield.closure_le, le_antisymm
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
a b : K
w : Membership.mem (γ := Subfield K) (closure s) a
hx : p a w
w_1 : Membership.mem (γ := Subfield K) (closure s) b
hy : p b w_1
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (a * b)

Tactic:
⟨_, mul _ _ _ _ hx hy⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
a b : K
w : Membership.mem (γ := Subfield K) (closure s) a
hx : p a w
w_1 : Membership.mem (γ := Subfield K) (closure s) b
hy : p b w_1
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (a * b)

Tactic:
exact ⟨_, mul _ _ _ _ hx hy⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
a b : K
w : Membership.mem (γ := Subfield K) (closure s) a
hx : p a w
w_1 : Membership.mem (γ := Subfield K) (closure s) b
hy : p b w_1
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (a + b)

Tactic:
⟨_, add _ _ _ _ hx hy⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
a b : K
w : Membership.mem (γ := Subfield K) (closure s) a
hx : p a w
w_1 : Membership.mem (γ := Subfield K) (closure s) b
hy : p b w_1
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (a + b)

Tactic:
exact ⟨_, add _ _ _ _ hx hy⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
simp_rw : p (HAdd.hAdd (α := K) 1 (-1)) ⋯
⊢ p 0 ⋯

Tactic:
simp_rw [← @add_neg_cancel K _ 1]

Premises used: add_neg_cancel, OfNat.ofNat
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
⊢ p (HAdd.hAdd (α := K) 1 (-1)) ⋯

Tactic:
add _ _ _ _ one (neg _ _ one)
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
⊢ p (HAdd.hAdd (α := K) 1 (-1)) ⋯

Tactic:
exact add _ _ _ _ one (neg _ _ one)
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
x_1 : K
w : Membership.mem (γ := Subfield K) (closure s) x_1
hx : p x_1 w
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (-x_1)

Tactic:
⟨_, neg _ _ hx⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
x_1 : K
w : Membership.mem (γ := Subfield K) (closure s) x_1
hx : p x_1 w
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} (-x_1)

Tactic:
exact ⟨_, neg _ _ hx⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
x_1 : K
w : Membership.mem (γ := Subfield K) (closure s) x_1
hx : p x_1 w
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} x_1⁻¹

Tactic:
⟨_, inv _ _ hx⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
x_1 : K
w : Membership.mem (γ := Subfield K) (closure s) x_1
hx : p x_1 w
⊢ Membership.mem (γ := Set K) {x : K | ∃ (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx} x_1⁻¹

Tactic:
exact ⟨_, inv _ _ hx⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
⊢ closure (↑s : Set K) = s

Tactic:
(Subfield.gi K).l_u_eq s

Premises used: GaloisInsertion.l_u_eq, Subfield.gi
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
⊢ Eq.{u + 1} (α := Subfield K) (closure ∅) ⊥

Tactic:
(Subfield.gi K).gc.l_bot

Premises used: GaloisConnection.l_bot, Subfield.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
⊢ Eq.{u + 1} (α := Subfield K) (closure Set.univ) ⊤

Tactic:
@coe_top K _ ▸ closure_eq ⊤

Premises used: Subfield.coe_top, Eq.rec, Subfield.closure_eq, Top.top
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s t : Set K
⊢ Eq (α := Subfield K) (closure (s ∪ t)) (closure s ⊔ closure t)

Tactic:
(Subfield.gi K).gc.l_sup

Premises used: GaloisConnection.l_sup, Subfield.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
s : ι → Set K
⊢ Eq.{u + 1} (α := Subfield K) (closure (⋃ (i : ι), s i)) (⨆ (i : ι), closure (s i))

Tactic:
(Subfield.gi K).gc.l_iSup

Premises used: GaloisConnection.l_iSup, Set.iUnion, Subfield.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Set (Set K)
⊢ Eq (α := Subfield K) (closure (⋃₀ s)) (⨆ t ∈ s, closure t)

Tactic:
(Subfield.gi K).gc.l_sSup

Premises used: Set.sUnion, GaloisConnection.l_sSup, Subfield.gi, GaloisInsertion.gc
-- 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:
(gc_map_comap f).l_sup

Premises used: Subfield.gc_map_comap, GaloisConnection.l_sup