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
s : Set E
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x : E
h : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
⊢ p ((Algebra.algebraMap F E : (a : F) → E) 1) ⋯

Tactic:
algebraMap 1

Premises used: OfNat.ofNat
-- 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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x : E
h : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
⊢ p ((Algebra.algebraMap F E : (a : F) → E) 1) ⋯

Tactic:
exact algebraMap 1

Premises used: OfNat.ofNat
-- 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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x_1 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_1
x : E
h_2 :
  Membership.mem (γ := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(Algebra.algebraMap F E) : (a : F) → E) ∪ s)) x
h : p x h_2
simp_rw : p (HMul.hMul (α := E) ((Algebra.algebraMap F E : (a : F) → E) (-1) : E) x) ⋯
⊢ p (-x) ⋯

Tactic:
simp_rw [← neg_one_smul F x, Algebra.smul_def]

Premises used: neg_one_smul, Algebra.smul_def
-- 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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x_1 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_1
x : E
h_2 :
  Membership.mem (γ := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(Algebra.algebraMap F E) : (a : F) → E) ∪ s)) x
h : p x h_2
⊢ p (HMul.hMul (α := E) ((Algebra.algebraMap F E : (a : F) → E) (-1) : E) x) ⋯

Tactic:
mul _ _ _ _ (algebraMap _) h
-- 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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x_1 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_1
x : E
h_2 :
  Membership.mem (γ := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(Algebra.algebraMap F E) : (a : F) → E) ∪ s)) x
h : p x h_2
⊢ p (HMul.hMul (α := E) ((Algebra.algebraMap F E : (a : F) → E) (-1) : E) x) ⋯

Tactic:
exact mul _ _ _ _ (algebraMap _) h
-- 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)
    ((fun (x1 x2 : K) ↦ x1 + x2)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1))
      ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2)))
    ((fun (x1 x2 : K) ↦ x1 + x2)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1))
      ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2)))

Tactic:
congr_arg₂ (· + ·) h₁ h₂

Premises used: HAdd.hAdd, 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₃ :
  (φ₁ : (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)
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)

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

Premises used: HAdd.hAdd, 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) ⋯) =
    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:
rw [← map_add]

Premises used: map_add
-- 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) ⋯) =
    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:
rw [← map_add]

Premises used: map_add
-- 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 : 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)
    ((fun (x1 x2 : K) ↦ x1 * x2)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1))
      ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2)))
    ((fun (x1 x2 : K) ↦ x1 * x2)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1))
      ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2)))

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

Premises used: HMul.hMul, congr_arg₂