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'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₁ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₂ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = Subalgebra.map f a₂.toSubalgebra), a₁ = a₂
rwa₃ : ∀ (h : a₁.toSubalgebra = a₂.toSubalgebra), a₁ = a₂
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : a₁ = a₂), a₁ = a₂
⊢ a₁ = a₂

Tactic:
rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

Premises used: IntermediateField.toSubalgebra_map, Function.Injective.eq_iff, RingHom.injective, Subalgebra.map_injective, IntermediateField.toSubalgebra_injective, AlgHom.toRingHom, IntermediateField.toSubalgebra_inj
-- 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
⊢ Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L) ⊆ (↑S : Set L)

Tactic:
S.toSubalgebra.range_subset

Premises used: Subalgebra.range_subset, 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
x : L
hx : Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L)) x
rwa : ∃ (y : K), (algebraMap K L : (a : K) → L) y = x
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L)) x
⊢ Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) x

Tactic:
rwa [Set.mem_range, ← RingHom.mem_fieldRange]

Premises used: Set.mem_range, RingHom.mem_fieldRange
-- 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 S' : IntermediateField K L
⊢ S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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 S' : IntermediateField K L
⊢ S.toSubalgebra < S'.toSubalgebra ↔ S < S'

Tactic:
Iff.rfl

Premises used: Iff.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
F : IntermediateField K L
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := IntermediateField K ↥F) lift

Tactic:
map_injective F.val

Premises used: IntermediateField.lift, IntermediateField.map_injective, IntermediateField.val
-- 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 : IntermediateField K L
E E' : IntermediateField K ↥F
⊢ lift E = lift E' ↔ E = E'

Tactic:
(lift_injective F).eq_iff

Premises used: Function.Injective.eq_iff, IntermediateField.lift_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 : IntermediateField K L
E : IntermediateField K ↥F
x : ↥F
left : x ∈ (↑E.toSubsemiring : Set ↥F)
⊢ Membership.mem (α := L) F (((↑F.val : ↥F →+* L) : (a : ↥F) → L) x : L)

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- 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 : IntermediateField K L
E : IntermediateField K ↥F
x : ↥F
left : x ∈ (↑E.toSubsemiring : Set ↥F)
⊢ Membership.mem (α := L) F (((↑F.val : ↥F →+* L) : (a : ↥F) → L) x : L)

Tactic:
exact x.2

Premises used: Subtype.property
-- 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 : IntermediateField K L
E : IntermediateField K ↥F
x : ↥F
⊢ (↑x : L) ∈ lift E ↔ x ∈ E

Tactic:
Subtype.val_injective.mem_set_image

Premises used: Set.Mem, Subtype.val_injective, setOf, Set.image, Function.Injective.mem_set_image
-- 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
F : IntermediateField K ↥E
x : ↥F
⊢ (↑((liftAlgEquiv F : (a : ↥F) → ↥(lift F)) x) : L) = (↑(↑x : ↥E) : 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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
E : IntermediateField L' L
⊢ (↑(restrictScalars K E) : Set L) = (↑E : Set 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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
E : IntermediateField L' L
⊢ Eq (α := Subalgebra K L) (toSubalgebra (restrictScalars K E)) (Subalgebra.restrictScalars K E.toSubalgebra)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, 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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
E : IntermediateField L' L
⊢ toSubfield (restrictScalars K E) = E.toSubfield

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, 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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
E : IntermediateField L' L
x : L
⊢ Membership.mem (γ := IntermediateField K L) (restrictScalars K E) x ↔ x ∈ E

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
U V : IntermediateField L' L
H : Eq (α := IntermediateField K L) (restrictScalars K U) (restrictScalars K V)
x : L
rw : Membership.mem (γ := IntermediateField K L) (restrictScalars K U) x ↔ x ∈ V
rw₁ : Membership.mem (γ := IntermediateField K L) (restrictScalars K V) x ↔ x ∈ V
rw₂ rw₃ : x ∈ V ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V

Tactic:
rw [← mem_restrictScalars K, H, mem_restrictScalars]

Premises used: IntermediateField.mem_restrictScalars
-- 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'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
E E' : IntermediateField L' L
⊢ Eq (α := IntermediateField K L) (restrictScalars K E) (restrictScalars K E') ↔ E = E'

Tactic:
(restrictScalars_injective K).eq_iff

Premises used: Function.Injective.eq_iff, IntermediateField.restrictScalars_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'
S F_1 E_1 F : IntermediateField K L
E : IntermediateField (↥F) L
⊢ Algebra.{u_1, u_2} K ↥E

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
S T : IntermediateField F E
h : S = T
⊢ (equivOfEq h).symm = equivOfEq ⋯

Tactic:
rfl

Premises used: AlgEquiv.symm, Set.Mem, Subalgebra.equivOfEq, IntermediateField.equivOfEq, Equiv.symm, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
⊢ Eq.{u_5 + 1} (α := ↥S ≃ₐ[F] ↥S) (equivOfEq ⋯) AlgEquiv.refl

Tactic:
AlgEquiv.ext fun _ ↦ rfl

Premises used: AlgEquiv.ext, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
S T U : IntermediateField F E
hST : S = T
hTU : T = U
⊢ (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq ⋯

Tactic:
rfl

Premises used: Set.Mem, Equiv.trans, Subalgebra.equivOfEq, IntermediateField.equivOfEq, AlgEquiv.trans, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
rw : (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
rw₁ : (f.comp L.val).range = Subalgebra.map f L.toSubalgebra
rw₂ : Subalgebra.map f L.val.range = Subalgebra.map f L.toSubalgebra
rw₃ rw₄ : Subalgebra.map f L.toSubalgebra = Subalgebra.map f L.toSubalgebra
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra

Tactic:
rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]

Premises used: AlgHom.fieldRange_toSubalgebra, IntermediateField.toSubalgebra_map, IntermediateField.range_val, AlgHom.range_comp
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
x : ↥L
⊢ Eq.{u_6 + 1} (α := K) ((↑((L.equivMap f : (a : ↥L) → ↥(map f L)) x) : K) : K) ((f : (a : E) → K) (↑x : E) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E : Subfield L
h : F ≤ E
⊢ (↑(extendScalars h) : Set L) = (↑E : Set L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E : Subfield L
h : F ≤ E
⊢ (extendScalars h).toSubfield = E

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E : Subfield L
h : F ≤ E
x : L
⊢ x ∈ extendScalars h ↔ x ∈ E

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E E' : Subfield L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ≤ extendScalars h' ↔ E ≤ E'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E : Subfield L
h : F ≤ E
E' : IntermediateField (↥F) L
⊢ extendScalars h ≤ E' ↔ E ≤ E'.toSubfield

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F E : Subfield L
h : F ≤ E
E' : IntermediateField (↥F) L
⊢ E' ≤ extendScalars h ↔ E'.toSubfield ≤ E

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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 E_1 E'_1 : Subfield L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : Subfield L // F ≤ E }
simp : extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
⊢ LE.le (α := IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : Subfield L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : Subfield L) ↦ F ≤ E) E.toSubfield ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : Subfield L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : Subfield L // F ≤ E }) → IntermediateField (↥F) L)
          E :
        IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : Subfield L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : Subfield L) ↦ F ≤ E) E.toSubfield ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : Subfield L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : Subfield L // F ≤ E }) → IntermediateField (↥F) L)
          E' :
        IntermediateField (↥F) L) ↔
    E ≤ E'

Tactic:
simp only [Equiv.coe_fn_mk]

Premises used: Equiv.coe_fn_mk
-- 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 E_1 E'_1 : Subfield L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : Subfield L // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
extendScalars_le_extendScalars_iff _ _

Premises used: Subfield.extendScalars_le_extendScalars_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 : IntermediateField K L
F E_1 E'_1 : Subfield L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : Subfield L // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
exact extendScalars_le_extendScalars_iff _ _

Premises used: Subfield.extendScalars_le_extendScalars_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
L : Type u_2
inst : Field L
F : Subfield L
⊢ Function.Injective (β := IntermediateField (↥F) L) fun (E : { E : Subfield L // F ≤ E }) ↦ extendScalars ⋯

Tactic:
(extendScalars.orderIso F).injective

Premises used: Subfield.extendScalars.orderIso, OrderIso.injective, Subfield.extendScalars, Subfield.toIntermediateField
-- 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
h : F ≤ E
⊢ (↑(extendScalars h) : Set L) = (↑E : 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
F E : IntermediateField K L
h : F ≤ E
⊢ (extendScalars h).toSubfield = E.toSubfield

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, 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
F E : IntermediateField K L
h : F ≤ E
x : L
⊢ x ∈ extendScalars h ↔ x ∈ E

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
F E : IntermediateField K L
h : F ≤ E
⊢ restrictScalars K (extendScalars h) = E

Tactic:
rfl

Premises used: IntermediateField.restrictScalars, 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
F E E' : IntermediateField K L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ≤ extendScalars h' ↔ E ≤ E'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
F E : IntermediateField K L
h : F ≤ E
E' : IntermediateField (↥F) L
⊢ extendScalars h ≤ E' ↔ E ≤ restrictScalars K E'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
F E : IntermediateField K L
h : F ≤ E
E' : IntermediateField (↥F) L
⊢ E' ≤ extendScalars h ↔ restrictScalars K E' ≤ E

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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 F E_1 E'_1 : IntermediateField K L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : IntermediateField K L // F ≤ E }
simp : extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
⊢ LE.le (α := IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : IntermediateField K L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : IntermediateField K L) ↦ F ≤ E) (restrictScalars K E) ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : IntermediateField K L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : IntermediateField K L // F ≤ E }) → IntermediateField (↥F) L)
          E :
        IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : IntermediateField K L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : IntermediateField K L) ↦ F ≤ E) (restrictScalars K E) ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : IntermediateField K L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : IntermediateField K L // F ≤ E }) → IntermediateField (↥F) L)
          E' :
        IntermediateField (↥F) L) ↔
    E ≤ E'

Tactic:
simp only [Equiv.coe_fn_mk]

Premises used: Equiv.coe_fn_mk
-- 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 F E_1 E'_1 : IntermediateField K L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : IntermediateField K L // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
extendScalars_le_extendScalars_iff _ _

Premises used: IntermediateField.extendScalars_le_extendScalars_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 F E_1 E'_1 : IntermediateField K L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : IntermediateField K L // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
exact extendScalars_le_extendScalars_iff _ _

Premises used: IntermediateField.extendScalars_le_extendScalars_iff
-- 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 : IntermediateField K L
⊢ Function.Injective (β := IntermediateField (↥F) L) fun (E : { E : IntermediateField K L // F ≤ E }) ↦ extendScalars ⋯

Tactic:
(extendScalars.orderIso F).injective

Premises used: IntermediateField.extendScalars, IntermediateField.extendScalars.orderIso, OrderIso.injective, Subfield.extendScalars, Subfield.toIntermediateField
-- 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
h : F ≤ E
x : ↥E
⊢ x ∈ restrict h ↔ (↑x : L) ∈ F

Tactic:
Set.ext_iff.mp (Set.range_inclusion h) x

Premises used: Set.range_inclusion, Set.Mem, setOf, Iff.mp, Set.ext_iff, 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
F E : IntermediateField K L
h : F ≤ E
h₁ : ∀ (x : L), x ∈ lift (restrict h) ↔ x ∈ F
⊢ lift (restrict h) = F

Tactic:
ext x
-- 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
h : F ≤ E
x : L
⊢ x ∈ lift (restrict h) ↔ x ∈ F

Tactic:
⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- 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
h : F ≤ E
x : L
h₁ : ∀ (hx : x ∈ lift (restrict h)), x ∈ F
h₂ : ∀ (hx : x ∈ F), x ∈ lift (restrict h)
⊢ x ∈ lift (restrict h) ↔ x ∈ F

Tactic:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := Subtype.mk (p := fun (x : L) ↦ x ∈ E) x ⋯
⊢ x ∈ F

Tactic:
(mem_restrict h y).1 ((mem_lift y).1 hx)

Premises used: Set.Mem, IntermediateField.mem_lift, Iff.mp, IntermediateField.mem_restrict
-- 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
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := Subtype.mk (p := fun (x : L) ↦ x ∈ E) x ⋯
⊢ x ∈ F

Tactic:
exact (mem_restrict h y).1 ((mem_lift y).1 hx)

Premises used: IntermediateField.mem_lift, Iff.mp, IntermediateField.mem_restrict
-- 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
h : F ≤ E
x : L
hx : x ∈ F
y : ↥E := Subtype.mk (p := fun (x : L) ↦ x ∈ E) x ⋯
⊢ x ∈ lift (restrict h)

Tactic:
(mem_lift y).2 ((mem_restrict h y).2 hx)

Premises used: Iff.mpr, Set.Mem, IntermediateField.mem_lift, IntermediateField.mem_restrict
-- 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
h : F ≤ E
x : L
hx : x ∈ F
y : ↥E := Subtype.mk (p := fun (x : L) ↦ x ∈ E) x ⋯
⊢ x ∈ lift (restrict h)

Tactic:
exact (mem_lift y).2 ((mem_restrict h y).2 hx)

Premises used: Iff.mpr, IntermediateField.mem_lift, IntermediateField.mem_restrict
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
a : ↥F
⊢ Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M)) a :
          ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
a : ↥F
⊢ Eq.{u_3 + 1} (α := M)
    ((↑(((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M)) a) :
        M) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
a : ↥(F.extendRight M)
rw :
  (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      (((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
              (a : ↥(F.extendRight M)) → ↥F)
            a) :
        ↥(F.extendRight M)) =
    (↑a : M)
rw₁ : (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M) a = (↑a : M)
rw₂ rw₃ : (↑a : M) = (↑a : M)
⊢ (algebraMap (↥F) M : (a : ↥F) → M)
      (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a :
        ↥F) =
    (↑a : M)

Tactic:
rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]

Premises used: AlgEquiv.apply_symm_apply, IntermediateField.algebraMap_extendRightEquiv, IntermediateField.algebraMap_apply