awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
⊢ (φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 + x_3) ⋯) =
    HAdd.hAdd (α := B) (β := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
        B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
        B)
have h₃ : Eq.{uB + 1} (α := B)
  ((φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 + x_3) sorry) :
    B)
  ((φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1 +
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
    B)
Tactic: rw [← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
⊢ (φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 + x_3) ⋯) =
    HAdd.hAdd (α := B) (β := B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
        B)
have h₃ : Eq.{uB + 1} (α := B)
  ((φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 + x_3) sorry) :
    B)
  ((φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1 +
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
    B)
Tactic: rw [← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
⊢ Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) :
      B)
have h₃ : (φ₁ : (a : ↥(adjoin R s)) → B)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) sorry) =
  HMul.hMul (α := B) (β := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
Tactic: convert! congr_arg₂ (· * ·) h₁ h₂
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
h₃ :
  (φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := B) (β := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
        B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
        B)
⊢ Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) :
      B)
have h₄ : (φ₂ : (a : ↥(adjoin R s)) → B)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) sorry) =
  HMul.hMul (α := B) (β := B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
Tactic: convert! congr_arg₂ (· * ·) h₁ h₂
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
⊢ (φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := B) (β := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
        B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
        B)
have h₃ : Eq.{uB + 1} (α := B)
  ((φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) sorry) :
    B)
  ((φ₁ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1 *
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
    B)
Tactic: rw [← map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
        B)
x_1 : ↥(adjoin R s)
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
x_2 x_3 : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_2
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_3
h₁ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
      B)
h₂ :
  Eq.{uB + 1} (α := B)
    ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
    ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)
⊢ (φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) ⋯) =
    HMul.hMul (α := B) (β := B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1) :
        B)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
        B)
have h₃ : Eq.{uB + 1} (α := B)
  ((φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x_2 * x_3) sorry) :
    B)
  ((φ₂ : (a : ↥(adjoin R s)) → B)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1 *
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
    B)
Tactic: rw [← map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
S : Subalgebra R A
s : Set A
hS : S = adjoin R s
φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥S) B
h :
  ∀ (x : A) (hx : x ∈ s),
    Eq.{uB + 1} (α := B) ((φ₁ : (a : ↥S) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) x ⋯) : B)
      ((φ₂ : (a : ↥S) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) x ⋯) : B)
⊢ φ₁ = φ₂
have subst : ∀ ⦃φ₁ φ₂ : AlgHom.{uR, uA, uB} R (↥(adjoin R s)) B⦄
  (h :
    ∀ (x : A) (hx : x ∈ s),
      Eq.{uB + 1} (α := B)
        ((φ₁ : (a : ↥(adjoin R s)) → B)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x sorry) :
          B)
        ((φ₂ : (a : ↥(adjoin R s)) → B)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x sorry) :
          B)),
  φ₁ = φ₂
Tactic: subst hS
Cleared hypotheses: S, hS, φ₁, φ₂, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : CommSemiring E
inst_1 : Semiring K
inst_2 : SMul F E
inst_3 : Algebra E K
inst_4 : Semiring F
inst_5 : Module F K
inst_6 : IsScalarTower F E K
L : Submonoid K
S : Set K
h : (↑L : Set K) = (↑(span F S) : Set K)
⊢ Eq (α := Submodule E K) ((toSubmodule : (a : Subalgebra E K) → Submodule E K) (adjoin E (↑L : Set K)) : Submodule E K)
    (span E S : Submodule E K)
have rw : Eq (α := Submodule E K) (span E (↑(span F S) : Set K)) (span E S)
Tactic: rw [adjoin_eq_span, L.closure_eq, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have a : comap f (map f S) ≤ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
a : comap f (map f S) ≤ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
⊢ comap f (map f S) = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have a₁ : S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ comap f (map f S)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have hx₁ : ∃ x_1 ∈ S, Eq.{uB + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) x : B)
Tactic: rw [mem_comap, mem_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : ∃ x_1 ∈ S, Eq.{uB + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) x : B)
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have a : ∀ (y : A) (hy : y ∈ S) (hxy : Eq.{uB + 1} (α := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)),
  x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
Tactic: obtain ⟨y, hy, hxy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Eq.{uB + 1} (α := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have hxy₁ : Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)
Tactic: replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have a : Membership.mem (γ := Subalgebra R A) (adjoin R ((↑S : Set A) ∪ Set.preimage (β := B) (⇑f : (a : A) → B) {0}))
  (y + (x - y))
Tactic: rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ comap f (map f S)
have a : map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) ≤
  map f S
Tactic: rw [← map_le, Algebra.map_sup, f.map_adjoin]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) ≤
    map f S
have a : map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) =
  map f S
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) =
    map f S
have a : Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ⊆ (↑(map f S) : Set B)
Tactic: rw [sup_eq_left, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
⊢ comap f (map f S) = S
have h₁ : S = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
Tactic: convert! comap_map_eq f S
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
⊢ S = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
have h₁ : adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ S
Tactic: rwa [left_eq_sup, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R Aᵐᵒᵖ) (Subalgebra.op (Algebra.adjoin R s)) (Algebra.adjoin R (MulOpposite.unop ⁻¹' s))
have a : Eq (α := Subsemiring Aᵐᵒᵖ) (toSubsemiring (Subalgebra.op (Algebra.adjoin R s)))
  (toSubsemiring (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)))
Tactic: apply toSubsemiring_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subsemiring Aᵐᵒᵖ) (toSubsemiring (Subalgebra.op (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)))
have a : Eq (α := Subsemiring Aᵐᵒᵖ)
  (Subsemiring.closure
    (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ MulOpposite.unop ⁻¹' s))
  (Subsemiring.closure
    (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s))
Tactic: simp_rw [Algebra.adjoin, op_toSubsemiring, Subsemiring.op_closure, Set.preimage_union]