awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 h_1 +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
    ((fun (x1 x2 : B) ↦ x1 * x2)
      ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1))
      ((φ₁ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2)))
    ((fun (x1 x2 : B) ↦ x1 * x2)
      ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_2 h_1))
      ((φ₂ : (a : ↥(adjoin R s)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2)))

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

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
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)

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

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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₃ :
  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 h_1 *
          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)

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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₃ :
  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 h_1 *
          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)

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 h_1 *
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 h_1 *
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_3 h_2) :
      B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
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 ⋯) :
            B)
          ((φ₂ : (a : ↥(adjoin R s)) → B)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x ⋯) :
            B)),
    φ₁ = φ₂
⊢ φ₁ = φ₂

Tactic:
subst hS
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
⊢ φ₁ = φ₂

Tactic:
adjoin_ext h

Premises used: AlgHom.adjoin_ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
⊢ φ₁ = φ₂

Tactic:
exact adjoin_ext h

Premises used: AlgHom.adjoin_ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set A
M : Type u_1
inst_3 : Monoid M
inst_4 : MulSemiringAction M A
inst_5 : SMulCommClass M R A
m : M
⊢ (∀ (x : A), Membership.mem (γ := Subalgebra R A) (adjoin R S) x → m • x = x) ↔ ∀ x ∈ S, m • x = x

Tactic:
AlgHom.eqOn_adjoin_iff (φ := MulSemiringAction.toAlgHom R A m) (ψ := .id R A)

Premises used: Set.EqOn, AlgHom.eqOn_adjoin_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ Eq (α := Subalgebra ℕ R) (adjoin ℕ s) (subalgebraOfSubsemiring (closure s))

Tactic:
le_antisymm (adjoin_le Subsemiring.subset_closure)
    (Subsemiring.closure_le.2 subset_adjoin : Subsemiring.closure s ≤ (adjoin ℕ s).toSubsemiring)

Premises used: Iff.mpr, Subsemiring.closure_le, Algebra.subset_adjoin, Subsemiring.subset_closure, le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
inst : Ring R
s : Set R
⊢ Eq (α := Subalgebra ℤ R) (adjoin ℤ s) (subalgebraOfSubring (Subring.closure s))

Tactic:
le_antisymm (adjoin_le Subring.subset_closure)
    (Subring.closure_le.2 subset_adjoin : Subring.closure s ≤ (adjoin ℤ s).toSubring)

Premises used: Iff.mpr, Algebra.subset_adjoin, Subring.subset_closure, le_antisymm, Algebra.adjoin_le, Subring.closure_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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)
rw : Eq (α := Submodule E K) (span E (↑(span F S) : Set K)) (span E S)
⊢ 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)

Tactic:
rw [adjoin_eq_span, L.closure_eq, h]

Premises used: Submonoid.closure_eq, Algebra.adjoin_eq_span
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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) (span E (↑(span F S) : Set K)) (span E S)

Tactic:
(span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)

Premises used: Iff.mpr, Submodule.span_subset_span, LE.le.antisymm, Submodule.span_mono, Submodule.subset_span, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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) (span E (↑(span F S) : Set K)) (span E S)

Tactic:
exact (span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)

Premises used: Iff.mpr, Submodule.span_subset_span, LE.le.antisymm, Submodule.span_mono, Submodule.subset_span, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 : CommSemiring F
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
L : Subalgebra F K
S : Set K
h :
  Eq (α := Submodule F K) ((toSubmodule : (a : Subalgebra F K) → Submodule F K) L : Submodule F K)
    (span F S : Submodule F 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)

Tactic:
L.toSubmonoid.adjoin_eq_span_of_eq_span F E (congr_arg ((↑) : _ → Set K) h)

Premises used: Submonoid.adjoin_eq_span_of_eq_span, Set.Mem, setOf, Subalgebra.toSubsemiring, Subsemiring.toSubmonoid
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := NonUnitalSubalgebra R A) (adjoin R s) (Subalgebra.toNonUnitalSubalgebra (Algebra.adjoin R s))

Tactic:
adjoin_le Algebra.subset_adjoin

Premises used: NonUnitalAlgebra.adjoin_le, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(NonUnitalAlgebra.adjoin R s) : Set A)) (adjoin R s)

Tactic:
le_antisymm
    (adjoin_le <| NonUnitalAlgebra.adjoin_le_algebra_adjoin R s)
    (adjoin_le <| (NonUnitalAlgebra.subset_adjoin R).trans subset_adjoin)

Premises used: NonUnitalAlgebra.adjoin_le_algebra_adjoin, NonUnitalAlgebra.subset_adjoin, Algebra.subset_adjoin, HasSubset.Subset.trans, le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ ∀ {a b : Subalgebra R A},
    LE.le (α := NonUnitalSubalgebra R A)
        (({ toFun := toNonUnitalSubalgebra, inj' := ⋯ } : (a : Subalgebra R A) → NonUnitalSubalgebra R A) a :
          NonUnitalSubalgebra R A)
        (({ toFun := toNonUnitalSubalgebra, inj' := ⋯ } : (a : Subalgebra R A) → NonUnitalSubalgebra R A) b :
          NonUnitalSubalgebra R A) ↔
      a ≤ b

Tactic:
simp [SetLike.le_def]

Premises used: SetLike.le_def
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
⊢ S.toNonUnitalSubalgebra ≤ T.toNonUnitalSubalgebra ↔ S ≤ T

Tactic:
toNonUnitalSubalgebraOrderEmbedding.le_iff_le

Premises used: Subalgebra.toNonUnitalSubalgebraOrderEmbedding, Set.Mem, OrderEmbedding.le_iff_le