awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x : ↥(AlgHom.range (toAlgHom F E K₁))
suffices : Subalgebra.map ϕ (AlgHom.range (toAlgHom F E K₁)) ≤ AlgHom.range (toAlgHom F E K₂)
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) ((ϕ : (a : K₁) → K₂) (↑x : K₁) : K₂)

Tactic:
suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
rw :
  Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂))
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
⊢ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x

Tactic:
rw [← hx, ← hy]
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
hx₁ :
  degree
      (minpoly.{u_6, u_4} E (B := K₂)
        (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)) =
    1
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂))
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)

Tactic:
apply minpoly.mem_range_of_degree_eq_one E

Premises used: minpoly.mem_range_of_degree_eq_one
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ Eq.{u_4 + 1} (α := K₂)
    (((aeval (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁)) :
            E[X] →ₐ[E] K₂) :
          (a : E[X]) → K₂)
        (map (algebraMap F E) (minpoly F z)) :
      K₂)
    (0 : K₂)

Tactic:
simp [aeval_algHom_apply]

Premises used: Polynomial.aeval_algHom_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
hx₁ :
  IsIntegral.{u_6, u_4} E (A := K₂)
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
⊢ degree
      (minpoly.{u_6, u_4} E (B := K₂)
        (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)) =
    1

Tactic:
refine ((h.splits z).of_dvd (map_ne_zero (minpoly.ne_zero (h.isIntegral z)))
        (minpoly.dvd E _ (by simp [aeval_algHom_apply]))).degree_eq_one_of_irreducible
        (minpoly.irreducible ?_)

Premises used: Normal.splits, Polynomial.Splits.degree_eq_one_of_irreducible, Normal.isIntegral, Polynomial.Splits.of_dvd, minpoly.dvd, Polynomial.map_ne_zero, minpoly.irreducible, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
hx₁ : IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
⊢ IsIntegral.{u_6, u_4} E (A := K₂)
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]

Premises used: AlgHom.coe_toRingHom, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
this : IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
⊢ IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)

Tactic:
this.tower_top

Premises used: IsIntegral.tower_top
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
this : IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
⊢ IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)

Tactic:
exact this.tower_top

Premises used: IsIntegral.tower_top
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
hx₁ : IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
⊢ IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)

Tactic:
suffices IsIntegral F _ by exact this.tower_top
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)

Tactic:
((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ

Premises used: IsScalarTower.toAlgHom, Normal.isIntegral, IsIntegral.map
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)

Tactic:
exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ

Premises used: IsScalarTower.toAlgHom, Normal.isIntegral, IsIntegral.map
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x y : ↥(AlgHom.range (toAlgHom F E K₁))
⊢ (↑(Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
          ((ϕ : (a : K₁) → K₂) (↑(x * y) : K₁)) ⋯) :
      K₂) =
    (↑(HMul.hMul (α := ↥(AlgHom.range (toAlgHom F E K₂))) (β := ↥(AlgHom.range (toAlgHom F E K₂)))
          (Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
              ((ϕ : (a : K₁) → K₂) (↑x : K₁)) ⋯ :
            ↥(AlgHom.range (toAlgHom F E K₂)))
          (Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
              ((ϕ : (a : K₁) → K₂) (↑y : K₁)) ⋯ :
            ↥(AlgHom.range (toAlgHom F E K₂)))) :
      K₂)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x y : ↥(AlgHom.range (toAlgHom F E K₁))
⊢ (↑(Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
          ((ϕ : (a : K₁) → K₂) (↑(x + y) : K₁)) ⋯) :
      K₂) =
    (↑(HAdd.hAdd (α := ↥(AlgHom.range (toAlgHom F E K₂))) (β := ↥(AlgHom.range (toAlgHom F E K₂)))
          (Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
              ((ϕ : (a : K₁) → K₂) (↑x : K₁)) ⋯ :
            ↥(AlgHom.range (toAlgHom F E K₂)))
          (Subtype.mk (p := fun (x : K₂) ↦ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x)
              ((ϕ : (a : K₁) → K₂) (↑y : K₁)) ⋯ :
            ↥(AlgHom.range (toAlgHom F E K₂)))) :
      K₂)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Algebra F K₁
inst_4 : Algebra F K₂
ϕ : K₁ →ₐ[F] K₂
E : Type u_6
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra E K₁
inst_8 : Algebra E K₂
inst_9 : IsScalarTower F E K₁
inst_10 : IsScalarTower F E K₂
inst_11 : Normal F E
x : E
⊢ Eq.{u_4 + 1} (α := K₂) ((algebraMap E K₂ : (a : E) → K₂) ((ϕ.restrictNormal E : (a : E) → E) x : E) : K₂)
    ((ϕ : (a : K₁) → K₂) ((algebraMap E K₁ : (a : E) → K₁) x : K₁) : K₂)

Tactic:
Subtype.ext_iff.mp
    (AlgEquiv.apply_symm_apply (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂))
      (ϕ.restrictNormalAux E ⟨IsScalarTower.toAlgHom F E K₁ x, x, rfl⟩))

Premises used: AlgEquiv.ofInjectiveField, AlgHom.restrictNormalAux, IsScalarTower.toAlgHom, AlgEquiv.apply_symm_apply, Subtype.ext_iff, Subtype.mk, Exists.intro, Iff.mp, Classical.choose, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
E : Type u_6
inst_7 : Field E
inst_8 : Algebra F E
inst_9 : Algebra E K₁
inst_10 : Algebra E K₂
inst_11 : Algebra E K₃
inst_12 : IsScalarTower F E K₁
inst_13 : IsScalarTower F E K₂
inst_14 : IsScalarTower F E K₃
inst_15 : Normal F E
x : E
⊢ Eq.{u_5 + 1} (α := K₃)
    (((algebraMap E K₃ : E →+* K₃) : (a : E) → K₃)
        ((comp (ψ.restrictNormal E) (ϕ.restrictNormal E) : (a : E) → E) x : E) :
      K₃)
    (((algebraMap E K₃ : E →+* K₃) : (a : E) → K₃) (((ψ.comp ϕ).restrictNormal E : (a : E) → E) x : E) : K₃)

Tactic:
simp only [AlgHom.comp_apply, AlgHom.restrictNormal_commutes]

Premises used: AlgHom.comp_apply, AlgHom.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Algebra F K₁
inst_4 : Algebra F K₂
χ : K₁ ≃ₐ[F] K₂
E : Type u_6
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra E K₁
inst_8 : Algebra E K₂
inst_9 : IsScalarTower F E K₁
inst_10 : IsScalarTower F E K₂
inst_11 : Normal F E
x : E
⊢ Eq.{u_4 + 1} (α := K₂) ((algebraMap E K₂ : (a : E) → K₂) ((χ.restrictNormal E : (a : E) → E) x : E) : K₂)
    ((χ : (a : K₁) → K₂) ((algebraMap E K₁ : (a : E) → K₁) x : K₁) : K₂)

Tactic:
χ.toAlgHom.restrictNormal_commutes E x

Premises used: AlgEquiv.toAlgHom, Classical.choose, AlgHom.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
L : IntermediateField F K₁
inst_3 : Normal.{u_1, u_3} F ↥L
σ : Gal(K₁/F)
x : ↥L
⊢ Eq (α := K₁) ((↑((σ.restrictNormal ↥L : (a : ↥L) → ↥L) x) : K₁) : K₁) ((σ : (a : K₁) → K₁) (↑x : K₁) : K₁)

Tactic:
AlgEquiv.restrictNormal_commutes σ L x

Premises used: Membership.mem, Subtype, AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
L : IntermediateField F K₁
inst_3 : Normal.{u_1, u_3} F ↥L
σ : Gal(K₁/F)
⊢ Eq (α := Gal(↥L/F)) (σ.restrictNormal ↥L) 1 ↔ ∀ x ∈ L, (σ : (a : K₁) → K₁) x = x

Tactic:
simp [AlgEquiv.ext_iff, Subtype.ext_iff, AlgEquiv.restrictNormal_apply]

Premises used: AlgEquiv.ext_iff, Subtype.ext_iff, AlgEquiv.restrictNormal_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
χ : K₁ ≃ₐ[F] K₂
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_7 : Field E
inst_8 : Algebra F E
inst_9 : Algebra E K₁
inst_10 : Algebra E K₂
inst_11 : Algebra E K₃
inst_12 : IsScalarTower F E K₁
inst_13 : IsScalarTower F E K₂
inst_14 : IsScalarTower F E K₃
inst_15 : Normal F E
x : E
⊢ Eq.{u_5 + 1} (α := K₃)
    (((algebraMap E K₃ : E →+* K₃) : (a : E) → K₃) (((χ.trans ω).restrictNormal E : (a : E) → E) x : E) : K₃)
    (((algebraMap E K₃ : E →+* K₃) : (a : E) → K₃)
        ((trans (χ.restrictNormal E) (ω.restrictNormal E) : (a : E) → E) x : E) :
      K₃)

Tactic:
simp only [AlgEquiv.trans_apply, AlgEquiv.restrictNormal_commutes]

Premises used: AlgEquiv.restrictNormal_commutes, AlgEquiv.trans_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
L : IntermediateField F K₁
inst_3 : Normal.{u_1, u_3} F ↥L
σ : Gal(K₁/F)
x : ↥L
⊢ Eq (α := K₁) ((↑((((restrictNormalHom ↥L : (a : Gal(K₁/F)) → Gal(↥L/F)) σ : Gal(↥L/F)) : (a : ↥L) → ↥L) x) : K₁) : K₁)
    ((σ : (a : K₁) → K₁) (↑x : K₁) : K₁)

Tactic:
AlgEquiv.restrictNormal_commutes σ L x

Premises used: Membership.mem, Subtype, AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : E →ₐ[F] K₁
H :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := K₁)
      (((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁))
              ((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F))) σ) :
            (a : E) → K₁)
          x :
        K₁)
      ((σ : (a : E) → K₁) x : K₁)
⊢ (fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁))
      ((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F))) σ) =
    σ

Tactic:
ext
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : E →ₐ[F] K₁
x : E
⊢ Eq.{u_3 + 1} (α := K₁)
    (((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁))
            ((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F))) σ) :
          (a : E) → K₁)
        x :
      K₁)
    ((σ : (a : E) → K₁) x : K₁)

Tactic:
simp [AlgHom.restrictNormal']

Premises used: AlgHom.restrictNormal'
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
h :
  ∀ (a : E),
    Eq (α := E)
      (((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
              ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) :
            (a : E) → E)
          a :
        E)
      ((σ : (a : E) → E) a : E)
⊢ (fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
      ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) =
    σ

Tactic:
ext
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
a : E
h :
  Eq (α := E) ((AlgHom.restrictNormal (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E)) E : (a : E) → E) a : E)
    ((σ : (a : E) → E) a : E)
⊢ Eq (α := E)
    (((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
            ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) :
          (a : E) → E)
        a :
      E)
    ((σ : (a : E) → E) a : E)

Tactic:
simp only [AlgHom.restrictNormal', AlgEquiv.coe_ofBijective]

Premises used: AlgEquiv.coe_ofBijective, AlgHom.restrictNormal'