awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
neg : ∀ (y : ↥S) (hy : Subtype.mk (p := fun (x : L) ↦ x ∈ S) x hx * y = 1), x⁻¹ ∈ S
⊢ x⁻¹ ∈ S

Tactic:
obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)

Premises used: Iff.mp, Subtype.coe_ne_coe, IsField.mul_inv_cancel
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ S) x hx * y = 1
⊢ x⁻¹ = (↑y : L)

Tactic:
rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy

Premises used: Subtype.coe_mk, Subalgebra.coe_one, mul_eq_one_iff_inv_eq₀, Subalgebra.coe_mul, Subtype.ext_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : x⁻¹ = (↑y : L)
⊢ x⁻¹ ∈ S

Tactic:
hy.symm ▸ y.2

Premises used: Set.Mem, Eq.rec, Eq.symm, Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : x⁻¹ = (↑y : L)
⊢ x⁻¹ ∈ S

Tactic:
exact hy.symm ▸ y.2
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
h : ∀ (x : L), x ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x ∈ S
⊢ (S.toIntermediateField' hS).toSubalgebra = S

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
⊢ x ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x ∈ S

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
h : ∀ (x : L), x ∈ S.toIntermediateField' ⋯ ↔ x ∈ S
⊢ S.toIntermediateField' ⋯ = S

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
⊢ x ∈ S.toIntermediateField' ⋯ ↔ x ∈ S

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subfield L
algebra_map_mem : ∀ (x : K), Membership.mem (α := L) S ((algebraMap K L : (a : K) → L) x : L)
⊢ (S.toIntermediateField algebra_map_mem).toSubfield = S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subfield L
algebra_map_mem : ∀ (x : K), Membership.mem (α := L) S ((algebraMap K L : (a : K) → L) x : L)
⊢ (↑(S.toIntermediateField algebra_map_mem) : Set L) = (↑S : Set L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst_3 : Fintype ι
f : ι → ↥S
⊢ Eq.{u_2 + 1} (α := L) (↑(∑ i : ι, f i) : L) (∑ i : ι, (↑(f i) : L))

Tactic:
AddSubmonoidClass.coe_finsetSum f Finset.univ

Premises used: Finset.univ, Set.Mem, AddSubmonoidClass.coe_finsetSum
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst_3 : Fintype ι
f : ι → ↥S
⊢ Eq.{u_2 + 1} (α := L) (↑(∏ i : ι, f i) : L) (∏ i : ι, (↑(f i) : L))

Tactic:
SubmonoidClass.coe_finsetProd f Finset.univ

Premises used: SubmonoidClass.coe_finsetProd, Finset.univ, Set.Mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
X : Type u_4
inst_3 : SMul L X
F : IntermediateField K L
g : ↥F
m : X
⊢ g • m = (↑g : L) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : Type u_5
Y : Type u_4
inst_5 : SMul L Y
inst_6 : SMul X Y
inst_7 : SMulCommClass L X Y
F : IntermediateField K L
⊢ SMulCommClass.{u_2, u_5, u_4} (↥F) X Y

Tactic:
inferInstanceAs (SMulCommClass F.toSubfield X Y)

Premises used: _private.0.IntermediateField.smulCommClass_left._proof_1
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : Type u_4
Y : Type u_5
inst_5 : SMul X Y
inst_6 : SMul L Y
inst_7 : SMulCommClass X L Y
F : IntermediateField K L
⊢ SMulCommClass.{u_4, u_2, u_5} X (↥F) Y

Tactic:
inferInstanceAs (SMulCommClass X F.toSubfield Y)

Premises used: _private.0.IntermediateField.smulCommClass_right._proof_1
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : Type u_4
Y : Type u_5
inst_5 : SMul X Y
inst_6 : SMul L X
inst_7 : SMul L Y
inst_8 : IsScalarTower L X Y
F : IntermediateField K L
⊢ IsScalarTower.{u_2, u_4, u_5} (↥F) X Y

Tactic:
inferInstanceAs (IsScalarTower F.toSubfield X Y)

Premises used: _private.0.IntermediateField.instIsScalarTowerSubtypeMem._proof_1
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : Type u_4
Y : ?m.9
inst_5 : SMul L X
inst_6 : FaithfulSMul L X
F : IntermediateField K L
⊢ FaithfulSMul.{u_2, u_4} (↥F) X

Tactic:
inferInstanceAs (FaithfulSMul F.toSubfield X)

Premises used: _private.0.IntermediateField.instFaithfulSMulSubtypeMem._proof_1
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : ?m.8
Y : ?m.9
R : Type u_4
inst_5 : Semiring R
inst_6 : SMul R K
inst_7 : Module R L
inst_8 : IsScalarTower R K L
⊢ IsScalarTower.{u_4, u_1, u_2} R K ↥S

Tactic:
inferInstanceAs (IsScalarTower R K S.toSubalgebra)

Premises used: _private.0.IntermediateField.isScalarTower._proof_1
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
R : Type u_4
inst_3 : SMul R K
inst_4 : SMul R L
inst_5 : IsScalarTower R K L
r : R
x : ↥S
⊢ (↑(r • x) : L) = r • (↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ (algebraMap (↥S) L : (a : ↥S) → L) x = (↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : K
⊢ Eq.{u_2 + 1} (α := L) ((↑((algebraMap K ↥S : (a : K) → ↥S) x) : L) : L) ((algebraMap K L : (a : K) → L) x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : ?m.8
Y : ?m.9
R : Type u_4
inst_5 : Semiring R
inst_6 : Algebra L R
⊢ IsScalarTower (↥S) L R

Tactic:
IsScalarTower.subalgebra _ _ _ S.toSubalgebra

Premises used: Set.Mem, IsScalarTower.subalgebra, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : ?m.8
Y : ?m.9
R : Type u_4
inst_5 : Semiring R
inst_6 : Algebra L R
inst_7 : Algebra K R
inst_8 : IsScalarTower K L R
⊢ IsScalarTower.{u_1, u_2, u_4} K (↥S) R

Tactic:
IsScalarTower.subalgebra' _ _ _ S.toSubalgebra

Premises used: Set.Mem, IsScalarTower.subalgebra', IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : ?m.8
Y : ?m.9
⊢ IsScalarTower K (↥S) L

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
X : ?m.8
Y : ?m.9
E : Type u_4
inst_5 : Field E
inst_6 : Algebra L E
T : IntermediateField.{u_2, u_4} (↥S) E
inst_7 : Algebra K E
inst_8 : IsScalarTower K L E
⊢ IsScalarTower.{u_1, u_2, u_4} K ↥S ↥T

Tactic:
T.isScalarTower

Premises used: IntermediateField.isScalarTower, Set.Mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
rw : Membership.mem (α := L') S (((f : (a : L) → L') x)⁻¹ : L')
⊢ Membership.mem (α := L') S ((f : (a : L) → L') x⁻¹ : L')

Tactic:
rw [map_inv₀ f x]

Premises used: map_inv₀
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ Membership.mem (α := L') S (((f : (a : L) → L') x)⁻¹ : L')

Tactic:
S.inv_mem hx

Premises used: Set.Mem, IntermediateField.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ Membership.mem (α := L') S (((f : (a : L) → L') x)⁻¹ : L')

Tactic:
exact S.inv_mem hx

Premises used: IntermediateField.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L
x : L
hx : x ∈ (↑S.toSubsemiring : Set L)
⊢ Membership.mem (α := L') (Subalgebra.map f S.toSubalgebra).carrier ((((↑f : L →+* L') : (a : L) → L') x)⁻¹ : L')

Tactic:
⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩

Premises used: Set.Mem, setOf, map_inv₀, Inv.inv, And.intro, Exists.intro, Set.image, IntermediateField.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L
x : L
hx : x ∈ (↑S.toSubsemiring : Set L)
⊢ Membership.mem (α := L') (Subalgebra.map f S.toSubalgebra).carrier ((((↑f : L →+* L') : (a : L) → L') x)⁻¹ : L')

Tactic:
exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
⊢ (↑(map f S) : Set L') = (⇑f : (a : L) → L') '' (↑S : Set L)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
⊢ (map f S).toSubalgebra = Subalgebra.map f S.toSubalgebra

Tactic:
rfl

Premises used: Subalgebra.map, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
⊢ (map f S).toSubfield = Subfield.map (↑f : L →+* L') S.toSubfield

Tactic:
rfl

Premises used: Subring.map, Subsemiring.map, rfl, Subfield.map
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ map (AlgHom.id K L) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
y : L'
⊢ y ∈ map f S ↔ ∃ x ∈ S, (f : (a : L) → L') x = y

Tactic:
Set.mem_image f S y

Premises used: Set.Mem, setOf, Set.mem_image, SetLike.coe, Set.image, DFunLike.coe
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
x : L
⊢ Membership.mem (α := L') (↑(map f S) : Set L') ((f : (a : L) → L') x : L') ↔ x ∈ S

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

Premises used: RingHom.injective, AlgHom.toRingHom, Function.Injective.mem_set_image
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_4
L₁ : Type u_5
L₂ : Type u_6
L₃ : Type u_7
inst : Field K
inst_1 : Field L₁
inst_2 : Algebra K L₁
inst_3 : Field L₂
inst_4 : Algebra K L₂
inst_5 : Field L₃
inst_6 : Algebra K L₃
E : IntermediateField K L₁
f : L₁ →ₐ[K] L₂
g : L₂ →ₐ[K] L₃
⊢ map g (map f E) = map (g.comp f) E

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
S T : IntermediateField K L
h : S ≤ T
⊢ map f S ≤ map f T

Tactic:
SetLike.coe_mono (Set.image_mono h)

Premises used: Set.image_mono, Set.Subset, SetLike.coe_mono
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
s : IntermediateField K L
t : IntermediateField K 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.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: IntermediateField.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
e : L ≃ₐ[K] L'
E : IntermediateField K L
a : ↥E
⊢ Eq.{u_3 + 1} (α := L') ((↑((intermediateFieldMap e E : (a : ↥E) → ↥(map (↑e : L →ₐ[K] L') E)) a) : L') : L')
    ((e : (a : L) → L') (↑a : L) : L')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
e : L ≃ₐ[K] L'
E : IntermediateField K L
a : ↥(map (↑e : L →ₐ[K] L') E)
⊢ Eq.{u_2 + 1} (α := L) ((↑(((intermediateFieldMap e E).symm : (a : ↥(map (↑e : L →ₐ[K] L') E)) → ↥E) a) : L) : L)
    ((e.symm : (a : L') → L) (↑a : L') : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
⊢ (↑f.fieldRange : Set L') = Set.range.{u_3, u_2 + 1} (ι := L) (⇑f : (a : L) → L')

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
⊢ f.fieldRange.toSubfield = RingHom.fieldRange (↑f : L →+* L')

Tactic:
rfl

Premises used: Subfield.copy, RingHom.fieldRange, Subsemiring.copy, rfl, RingHom.rangeS
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
y : L'
⊢ y ∈ f.fieldRange ↔ ∃ (x : L), (f : (a : L) → L') x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ Eq (α := (a : ↥S) → L) (⇑S.val : (a : ↥S) → L) (Subtype.val (p := fun (x : L) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ (S.val : (a : ↥S) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ S) x hx) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ S.val.range = S.toSubalgebra

Tactic:
S.toSubalgebra.range_val

Premises used: Set.Mem, Subalgebra.range_val, IntermediateField.val, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ S.val.fieldRange = S

Tactic:
SetLike.ext' Subtype.range_val

Premises used: Subtype.range_val, SetLike.ext'
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
R : Type u_4
inst_3 : CommSemiring R
inst_4 : Algebra R K
inst_5 : Algebra R L
inst_6 : IsScalarTower R K L
x : ↥S
P : R[X]
⊢ Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : R[X]) → L) P : L) ((↑((aeval x : (a : R[X]) → ↥S) P) : L) : L)

Tactic:
aeval_algHom_apply (S.val.restrictScalars R) x P

Premises used: AlgHom.restrictScalars, IntermediateField.val, Polynomial.aeval_algHom_apply
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E F : IntermediateField K L
hEF : E ≤ F
⊢ Function.Injective (α := ↥E) (β := ↥F) (⇑(inclusion hEF) : (a : ↥E) → ↥F)

Tactic:
Subalgebra.inclusion_injective hEF

Premises used: Set.Mem, Subalgebra.inclusion_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
⊢ inclusion ⋯ = AlgHom.id K ↥E

Tactic:
Subalgebra.inclusion_self

Premises used: Set.Mem, Subalgebra.inclusion_self, IntermediateField.inclusion
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E F G : IntermediateField K L
hEF : E ≤ F
hFG : F ≤ G
x : ↥E
⊢ Eq (α := ↥G) ((inclusion hFG : (a : ↥F) → ↥G) ((inclusion hEF : (a : ↥E) → ↥F) x) : ↥G)
    ((inclusion ⋯ : (a : ↥E) → ↥G) x : ↥G)

Tactic:
Subalgebra.inclusion_inclusion hEF hFG x

Premises used: Set.Mem, Subalgebra.inclusion_inclusion
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E F : IntermediateField K L
hEF : E ≤ F
e : ↥E
⊢ (↑((inclusion hEF : (a : ↥E) → ↥F) e) : L) = (↑e : L)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ : IntermediateField K L
_ : ∀ ⦃a₂ : IntermediateField K L⦄, a₁.toSubalgebra = a₂.toSubalgebra → a₁ = a₂
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, a₁.toSubalgebra = a₂.toSubalgebra → a₁ = a₂

Tactic:
_
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubalgebra = a₂.toSubalgebra
h₁ : ∀ (x : L), x ∈ a₁ ↔ x ∈ a₂
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ : IntermediateField K L
_ : ∀ ⦃a₂ : IntermediateField K L⦄, a₁.toSubfield = a₂.toSubfield → a₁ = a₂
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, a₁.toSubfield = a₂.toSubfield → a₁ = a₂

Tactic:
_
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubfield = a₂.toSubfield
h₁ : ∀ (x : L), x ∈ a₁ ↔ x ∈ a₂
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubfield = a₂.toSubfield
x : L
h₁ : x ∈ a₁.toSubfield ↔ x ∈ a₂.toSubfield
⊢ x ∈ a₁ ↔ x ∈ a₂

Tactic:
simp_rw [← mem_toSubfield, h]

Premises used: IntermediateField.mem_toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
⊢ F.toSubalgebra = E.toSubalgebra ↔ F = E

Tactic:
toSubalgebra_injective.eq_iff

Premises used: Function.Injective.eq_iff, IntermediateField.toSubalgebra_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
⊢ F.toSubfield = E.toSubfield ↔ F = E

Tactic:
toSubfield_injective.eq_iff

Premises used: Function.Injective.eq_iff, IntermediateField.toSubfield_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ : IntermediateField K L
_ : ∀ ⦃a₂ : IntermediateField K L⦄, map f a₁ = map f a₂ → a₁ = a₂
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, map f a₁ = map f a₂ → a₁ = a₂

Tactic:
_