awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
h₃ :
  (φ₁ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := K) (β := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
        K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
        K)
h₄ :
  (φ₂ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := K) (β := K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
        K)
⊢ Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)

Tactic:
convert! congr_arg₂ (· * ·) h₁ h₂

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
h₃ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1 *
          Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
⊢ (φ₁ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := K) (β := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
        K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
        K)

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
h₃ :
  Eq.{u_3 + 1} (α := K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1 *
          Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
⊢ (φ₂ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := K) (β := K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
        K)

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1 *
          Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 * x_3) ⋯) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1 *
          Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
S : IntermediateField F E
s : Set E
hS : S = adjoin F s
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥S) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K) ((φ₁ : (a : ↥S) → K) (Subtype.mk (p := fun (x : E) ↦ x ∈ S) x ⋯) : K)
      ((φ₂ : (a : ↥S) → K) (Subtype.mk (p := fun (x : E) ↦ x ∈ S) x ⋯) : K)
subst :
  ∀ ⦃φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K⦄
    (h :
      ∀ (x : E) (hx : x ∈ s),
        Eq.{u_3 + 1} (α := K)
          ((φ₁ : (a : ↥(adjoin F s)) → K)
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
            K)
          ((φ₂ : (a : ↥(adjoin F s)) → K)
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
            K)),
    φ₁ = φ₂
⊢ φ₁ = φ₂

Tactic:
subst hS
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
⊢ φ₁ = φ₂

Tactic:
adjoin_algHom_ext F h

Premises used: IntermediateField.adjoin_algHom_ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
⊢ φ₁ = φ₂

Tactic:
exact adjoin_algHom_ext F h

Premises used: IntermediateField.adjoin_algHom_ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Membership.mem (γ := IntermediateField F E) F⟮α⟯ α

Tactic:
subset_adjoin F {α} (Set.mem_singleton α)

Premises used: Set.mem_singleton, IntermediateField.subset_adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ (↑(gen F α) : E) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ (algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
f : F[X]
⊢ Eq.{u_2 + 1} (α := E) ((↑((aeval (gen F α) : (a : F[X]) → ↥F⟮α⟯) f) : E) : E) ((aeval α : (a : F[X]) → E) f : E)

Tactic:
Polynomial.coe_aeval_mk_apply ..

Premises used: Set.Mem, IntermediateField.AdjoinSimple.gen, Polynomial.coe_aeval_mk_apply, IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α β : E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥F⟮α⟯) (↥F⟮α⟯)⟮β⟯) F⟮α, β⟯

Tactic:
adjoin_adjoin_left _ _ _

Premises used: Set.insert, Set.Mem, setOf, Set.singleton, IntermediateField.adjoin_adjoin_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α β : E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥F⟮α⟯) (↥F⟮α⟯)⟮β⟯)
    (restrictScalars F (L' := ↥F⟮β⟯) (↥F⟮β⟯)⟮α⟯)

Tactic:
adjoin_adjoin_comm _ _ _

Premises used: IntermediateField.adjoin_adjoin_comm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : IntermediateField F E
⊢ F⟮α⟯ ≤ K ↔ α ∈ K

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
rw : Eq (α := IntermediateField F E) (adjoin F (⨆ t ∈ S, {t})) (adjoin F S)
⊢ Eq (α := IntermediateField F E) (⨆ x ∈ S, F⟮x⟯) (adjoin F S)

Tactic:
rw [← iSup_subtype'', ← gc.l_iSup, iSup_subtype'']

Premises used: iSup_subtype'', GaloisConnection.l_iSup, IntermediateField.gc
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
e_S : ⨆ t ∈ S, {t} = S
⊢ Eq (α := IntermediateField F E) (adjoin F (⨆ t ∈ S, {t})) (adjoin F S)

Tactic:
congr
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ ⨆ t ∈ S, {t} = S

Tactic:
S.biUnion_of_singleton

Premises used: Set.biUnion_of_singleton, Set.iUnion
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ ⨆ t ∈ S, {t} = S

Tactic:
exact S.biUnion_of_singleton

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : Field B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) b : C)
    ((AlgHom.restrictScalars A (Algebra.ofId B C) : (a : B) → C) b : C)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : Field B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
rw :
  Membership.mem (α := C) (γ := IntermediateField A C) (map (AlgHom.restrictScalars A (Algebra.ofId B C)) A⟮b⟯)
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (Algebra.ofId B C)) (val A⟮b⟯)) : ↥A⟮b⟯ →+* C) : (a : ↥A⟮b⟯) → C) x : C)
⊢ Membership.mem (α := C) (γ := IntermediateField A C) A⟮((algebraMap B C : (a : B) → C) b : C)⟯
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (Algebra.ofId B C)) (val A⟮b⟯)) : ↥A⟮b⟯ →+* C) : (a : ↥A⟮b⟯) → C) x : C)

Tactic:
rw [show (algebraMap B C) b = (Algebra.ofId B C).restrictScalars A b by rfl,
      ← Set.image_singleton, ← IntermediateField.adjoin_map A {b}]

Premises used: Set.image_singleton, IntermediateField.adjoin_map, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : Field B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
h :
  (↑x : B) ∈ (↑(Subalgebra.toSubsemiring (toSubalgebra A⟮b⟯)) : Set B) ∧
    Eq.{u_5 + 1} (α := C) (((↑(AlgHom.restrictScalars A (Algebra.ofId B C)) : B →+* C) : (a : B) → C) (↑x : B) : C)
      (((↑(AlgHom.comp (AlgHom.restrictScalars A (Algebra.ofId B C)) (val A⟮b⟯)) : ↥A⟮b⟯ →+* C) : (a : ↥A⟮b⟯) → C) x :
        C)
⊢ Membership.mem (α := C) (γ := IntermediateField A C) (map (AlgHom.restrictScalars A (Algebra.ofId B C)) A⟮b⟯)
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (Algebra.ofId B C)) (val A⟮b⟯)) : ↥A⟮b⟯ →+* C) : (a : ↥A⟮b⟯) → C) x : C)

Tactic:
use x
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : Field B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ (↑x : B) ∈ (↑(Subalgebra.toSubsemiring (toSubalgebra A⟮b⟯)) : Set B) ∧
    Eq.{u_5 + 1} (α := C) (((↑(AlgHom.restrictScalars A (Algebra.ofId B C)) : B →+* C) : (a : B) → C) (↑x : B) : C)
      (((↑(AlgHom.comp (AlgHom.restrictScalars A (Algebra.ofId B C)) (val A⟮b⟯)) : ↥A⟮b⟯ →+* C) : (a : ↥A⟮b⟯) → C) x :
        C)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : Field B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
⊢ Eq (α := RingHom.{u_4, u_5} (↥A⟮b⟯) C) (algebraMap (↥A⟮b⟯) C)
    (@RingHom.comp _ ↥A⟮((algebraMap B C : (a : B) → C) b : C)⟯ _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↥A⟮((algebraMap B C : (a : B) → C) b : C)⟯) C)
      (algebraMap ↥A⟮b⟯ ↥A⟮((algebraMap B C : (a : B) → C) b : C)⟯))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
rw : LE.le (α := IntermediateField F E) (adjoin F S) ⊥ ↔ S ⊆ (↑⊥ : Set E)
rw₁ rw₂ : S ⊆ (↑⊥ : Set E) ↔ S ⊆ (↑⊥ : Set E)
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊥ ↔ S ⊆ (↑⊥ : Set E)

Tactic:
rw [eq_bot_iff, adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff, eq_bot_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊥ ↔ Membership.mem (γ := IntermediateField F E) ⊥ α

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) F⟮0⟯ ⊥

Tactic:
adjoin_simple_eq_bot_iff.mpr (zero_mem ⊥)

Premises used: Iff.mpr, Bot.bot, IntermediateField.adjoin_simple_eq_bot_iff, ZeroMemClass.zero_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) F⟮1⟯ ⊥

Tactic:
adjoin_simple_eq_bot_iff.mpr (one_mem ⊥)

Premises used: Iff.mpr, Bot.bot, IntermediateField.adjoin_simple_eq_bot_iff, OneMemClass.one_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
n : ℤ
⊢ Eq (α := IntermediateField F E) F⟮(↑n : E)⟯ ⊥

Tactic:
adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n)

Premises used: Iff.mpr, intCast_mem, Bot.bot, IntermediateField.adjoin_simple_eq_bot_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
n : ℤ
⊢ Eq (α := IntermediateField F E) F⟮(↑n : E)⟯ ⊥

Tactic:
exact adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n)

Premises used: Iff.mpr, intCast_mem, Bot.bot, IntermediateField.adjoin_simple_eq_bot_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
n : ℕ
⊢ Eq (α := IntermediateField F E) F⟮(↑n : E)⟯ ⊥

Tactic:
adjoin_simple_eq_bot_iff.mpr (natCast_mem ⊥ n)

Premises used: Iff.mpr, IntermediateField.natCast_mem, Bot.bot, IntermediateField.adjoin_simple_eq_bot_iff