awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
x : A
hx : x ∈ s
⊢ Commute a x

Tactic:
h x hx
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
x : A
hx : x ∈ s
⊢ Commute a x

Tactic:
exact h x hx
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
r : R
⊢ Commute a ((algebraMap R A : (a : R) → A) r)

Tactic:
commutes r a |>.symm

Premises used: SemiconjBy, Commute, Eq.symm, Algebra.commutes
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
r : R
⊢ Commute a ((algebraMap R A : (a : R) → A) r)

Tactic:
exact commutes r a |>.symm

Premises used: Eq.symm, Algebra.commutes
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy : Commute a y
hz : Commute a z
⊢ Commute a (y + z)

Tactic:
hy.add_right hz

Premises used: Commute.add_right
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy : Commute a y
hz : Commute a z
⊢ Commute a (y + z)

Tactic:
exact hy.add_right hz

Premises used: Commute.add_right
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy : Commute a y
hz : Commute a z
⊢ Commute a (y * z)

Tactic:
hy.mul_right hz

Premises used: Commute.mul_right
-- 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
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy : Commute a y
hz : Commute a z
⊢ Commute a (y * z)

Tactic:
exact hy.mul_right hz

Premises used: Commute.mul_right
-- 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
a b : A
s : Set A
hb : Membership.mem (γ := Subalgebra R A) (adjoin R s) b
h mem : ∀ (x : A) (hx : x ∈ s), Commute a x
algebraMap : ∀ (r : R), Commute a ((Algebra.algebraMap R A : (a : R) → A) r)
add :
  ∀ (y z : A),
    Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
      Membership.mem (γ := Subalgebra R A) (adjoin R s) z → ∀ (hy : Commute a y) (hz : Commute a z), Commute a (y + z)
mul :
  ∀ (y z : A),
    Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
      Membership.mem (γ := Subalgebra R A) (adjoin R s) z → ∀ (hy : Commute a y) (hz : Commute a z), Commute a (y * z)
⊢ Commute a b

Tactic:
induction hb using adjoin_induction with
  | mem x hx => exact h x hx
  | algebraMap r => exact commutes r a |>.symm
  | add y z _ _ hy hz => exact hy.add_right hz
  | mul y z _ _ hy hz => exact hy.mul_right hz

Premises used: Algebra.algebraMap, Submodule.mul, Submodule.add
-- 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
a b c : A
hc : Membership.mem (γ := Subalgebra R A) R[b] c
h : Commute a b
⊢ ∀ (b_1 : A), Membership.mem (γ := Set A) {b} b_1 → Commute a b_1

Tactic:
simpa
-- 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
a b : A
hb : Membership.mem (γ := Subalgebra R A) R[a] b
⊢ Commute a b

Tactic:
commute_of_mem_adjoin_singleton_of_commute hb rfl

Premises used: Algebra.commute_of_mem_adjoin_singleton_of_commute, rfl
-- 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
x : A
⊢ Membership.mem (γ := Subalgebra R A) R[x] x

Tactic:
Algebra.subset_adjoin (Set.mem_singleton_iff.mpr rfl)

Premises used: Iff.mpr, Algebra.subset_adjoin, Set.mem_singleton_iff, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
rw :
  Eq (α := Submodule R A) (span R (↑(Submonoid.closure (s ∪ t)) : Set A))
    (span R ((↑(Submonoid.closure s) : Set A) * (↑(Submonoid.closure t) : Set A)))
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)) =
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R t) : Submodule R A)

Tactic:
rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]

Premises used: Submodule.span_mul_span, Algebra.adjoin_eq_span
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
e_s :
  ∀ (z : A),
    z ∈ (↑(Submonoid.closure (s ∪ t)) : Set A) ↔ z ∈ (↑(Submonoid.closure s) : Set A) * (↑(Submonoid.closure t) : Set A)
⊢ Eq (α := Submodule R A) (span R (↑(Submonoid.closure (s ∪ t)) : Set A))
    (span R ((↑(Submonoid.closure s) : Set A) * (↑(Submonoid.closure t) : Set A)))

Tactic:
congr 1 with z
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
z : A
⊢ z ∈ (↑(Submonoid.closure (s ∪ t)) : Set A) ↔ z ∈ (↑(Submonoid.closure s) : Set A) * (↑(Submonoid.closure t) : Set A)

Tactic:
simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]

Premises used: Submonoid.mem_sup, Submonoid.closure_union, Set.mem_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
n : ℤ
⊢ Eq (α := Subalgebra R A) R[(↑n : A)] ⊥

Tactic:
simpa using adjoin_singleton_algebraMap A (n : R)

Premises used: Int.cast, Algebra.adjoin_singleton_algebraMap
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
n : ℤ
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (insert (↑n : A) s)) (adjoin R s)

Tactic:
simpa using adjoin_insert_algebraMap (n : R) s

Premises used: Int.cast, Algebra.adjoin_insert_algebraMap
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
s : Set A
⊢ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ⊆ (↑(Subalgebra.toSubring (adjoin R s)) : Set A)

Tactic:
simp [adjoin]

Premises used: Algebra.adjoin
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
s : Set A
x : A
rw :
  Membership.mem (γ := Subring A) (Subalgebra.toSubring (adjoin R s)) x ↔
    Membership.mem (γ := Subring A)
      (Subring.closure (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)) x
rw₁ rw₂ :
  Membership.mem (γ := Subring A)
      (Subring.closure (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)) x ↔
    Membership.mem (γ := Subring A)
      (Subring.closure (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)) x
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R s) x ↔
    Membership.mem (γ := Subring A)
      (Subring.closure (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)) x

Tactic:
rw [← Subalgebra.mem_toSubring, adjoin_eq_ring_closure]

Premises used: Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring
-- 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
φ : A →ₐ[R] B
s : Set A
⊢ Subalgebra.map φ (adjoin R s) = adjoin R ((⇑φ : (a : A) → B) '' s)

Tactic:
(adjoin_image _ _ _).symm

Premises used: Algebra.adjoin_image, Eq.symm
-- 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
e : A →ₐ[R] B
x : A
rw : Eq (α := Subalgebra R B) (adjoin R (Set.image (α := A) (⇑e : (a : A) → B) {x})) R[((e : (a : A) → B) x : B)]
rw₁ rw₂ : Eq (α := Subalgebra R B) R[((e : (a : A) → B) x : B)] R[((e : (a : A) → B) x : B)]
⊢ Subalgebra.map e R[x] = R[((e : (a : A) → B) x : B)]

Tactic:
rw [map_adjoin, Set.image_singleton]

Premises used: Set.image_singleton, AlgHom.map_adjoin
-- 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
φ₁ φ₂ : A →ₐ[R] B
s : Set A
h : Set.EqOn.{uA, uB} (β := B) (⇑φ₁ : (a : A) → B) (⇑φ₂ : (a : A) → B) s
⊢ LE.le (α := Subalgebra R A) (adjoin R s) (equalizer φ₁ φ₂)

Tactic:
adjoin_le h

Premises used: Algebra.adjoin_le
-- 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
h : Eq (α := Subalgebra R A) (adjoin R s) ⊤
φ₁ φ₂ : A →ₐ[R] B
hs : Set.EqOn.{uA, uB} (β := B) (⇑φ₁ : (a : A) → B) (⇑φ₂ : (a : A) → B) s
⊢ φ₁ = φ₂

Tactic:
ext fun _x => adjoin_le_equalizer φ₁ φ₂ hs <| h.symm ▸ trivial

Premises used: trivial, Eq.rec, AlgHom.ext, AlgHom.adjoin_le_equalizer, Eq.symm
-- 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
φ ψ : A →ₐ[R] B
s : Set A
⊢ ∀ (S : Set A), S ≤ (↑(equalizer φ ψ) : Set A) ↔ Set.EqOn.{uA, uB} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) S

Tactic:
have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.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
φ ψ : A →ₐ[R] B
s : Set A
this :
  ∀ (S : Set A), S ≤ (↑(equalizer φ ψ) : Set A) ↔ Set.EqOn.{uA, uB} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) S
⊢ Set.EqOn.{uA, uB} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑(adjoin R s) : Set A) ↔
    Set.EqOn.{uA, uB} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) s

Tactic:
simp only [← this, Set.le_eq_subset, SetLike.coe_subset_coe, adjoin_le_iff]

Premises used: Set.le_eq_subset, SetLike.coe_subset_coe, Algebra.adjoin_le_iff
-- 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: HAdd.hAdd, 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) ⋯) =
    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)
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) ⋯) =
    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)
⊢ 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: HAdd.hAdd, 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) ⋯) =
    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)

Tactic:
rw [← map_add]

Premises used: map_add
-- 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) ⋯) =
    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)

Tactic:
rw [← map_add]

Premises used: map_add
-- 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