awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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) ⋯) =
    HAdd.hAdd (α := 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)
have 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) sorry) =
  HAdd.hAdd (α := 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: convert! congr_arg₂ (· + ·) h₁ h₂
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ (φ₁ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 + x_3) ⋯) =
    HAdd.hAdd (α := 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)
have 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) sorry) :
    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: rw [← map_add]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ (φ₂ : (a : ↥(adjoin F s)) → K)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 + x_3) ⋯) =
    HAdd.hAdd (α := 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)
have 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) sorry) :
    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: rw [← map_add]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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 * x_3) ⋯) :
      K)
have 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) sorry) =
  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: convert! congr_arg₂ (· * ·) h₁ h₂
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ 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)
have 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) sorry) =
  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: convert! congr_arg₂ (· * ·) h₁ h₂
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ (φ₁ : (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)
have 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) sorry) :
    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: rw [← map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ (φ₂ : (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)
have 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) sorry) :
    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: rw [← map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ φ₁ = φ₂
have 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 sorry) :
          K)
        ((φ₂ : (a : ↥(adjoin F s)) → K)
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x sorry) :
          K)),
  φ₁ = φ₂
Tactic: subst hS
Cleared hypotheses: S, hS, φ₁, φ₂, h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Eq (α := IntermediateField F E) (⨆ x ∈ S, F⟮x⟯) (adjoin F S)
have rw : Eq (α := IntermediateField F E) (adjoin F (⨆ t ∈ S, {t})) (adjoin F S)
Tactic: rw [← iSup_subtype'', ← gc.l_iSup, iSup_subtype'']
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Eq (α := IntermediateField F E) (adjoin F (⨆ t ∈ S, {t})) (adjoin F S)
have e_S : ⨆ t ∈ S, {t} = S
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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⟯
⊢ 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)
have 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)
Tactic: rw [show (algebraMap B C) b = (Algebra.ofId B C).restrictScalars A b by rfl,
      ← Set.image_singleton, ← IntermediateField.adjoin_map A {b}]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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⟯
⊢ 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)
have 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)
Tactic: use x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊥ ↔ S ⊆ (↑⊥ : Set E)
have rw : LE.le (α := IntermediateField F E) (adjoin F S) ⊥ ↔ S ⊆ (↑⊥ : Set E)
Tactic: rw [eq_bot_iff, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
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)
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊥ ↔ S ⊆ (↑⊥ : Set E)
have rw₁ : S ⊆ (↑⊥ : Set E) ↔ S ⊆ (↑⊥ : Set E)
Tactic: rw [eq_bot_iff, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : IntermediateField F E
hS : S.FG
hT : T.FG
⊢ (S ⊔ T).FG
have obtain : ∀ (s : Finset E), (adjoin F (↑s : Set E) ⊔ T).FG
Tactic: obtain ⟨s, rfl⟩ := hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
T : IntermediateField F E
hT : T.FG
s : Finset E
⊢ (adjoin F (↑s : Set E) ⊔ T).FG
have obtain : ∀ (t : Finset E), FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))
Tactic: obtain ⟨t, rfl⟩ := hT
Cleared hypotheses: T, hT
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
⊢ FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))
have rw : FG (adjoin F (↑(s ∪ t) : Set E))
Tactic: rw [← adjoin_union, ← Finset.coe_union]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
⊢ FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))
have classical : FG (adjoin F (↑(s ∪ t) : Set E))
Tactic: classical rw [← adjoin_union, ← Finset.coe_union]