awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
have this : Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
  ((f : (a : A) → B) 1 : B)
Tactic: have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
-- 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
have h : (f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)
Tactic: convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
-- 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
⊢ (f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)
have h : (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)
Tactic: rw [algebraMap_eq_smul_one]
-- 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) x : B)
have mem : ∀ (a : A) (ha : a ∈ s),
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) a : B)
Tactic: induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz
Cleared hypotheses: 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
mem :
  ∀ (a : A) (ha : a ∈ s),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) a : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) x : B)
have algebraMap : ∀ (r : R),
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
Tactic: induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz
Cleared hypotheses: 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
mem :
  ∀ (a : A) (ha : a ∈ s),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) a : B)
algebraMap :
  ∀ (r : R),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) ((Algebra.algebraMap R A : (a : R) → A) r : A) : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) x : B)
have add : ∀ (y z : A),
  Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) z →
      ∀
        (hy :
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) y : B))
        (hz :
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) z : B)),
        Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
          ((f : (a : A) → B) (y + z) : B)
Tactic: induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz
Cleared hypotheses: 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
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
mem :
  ∀ (a : A) (ha : a ∈ s),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) a : B)
algebraMap :
  ∀ (r : R),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) ((Algebra.algebraMap R A : (a : R) → A) r : A) : B)
add :
  ∀ (y z : A),
    Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
      Membership.mem (γ := Subalgebra R A) (adjoin R s) z →
        ∀
          (hy :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) y : B))
          (hz :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) z : B)),
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) (y + z) : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) x : B)
have mul : ∀ (y z : A),
  Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) z →
      ∀
        (hy :
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) y : B))
        (hz :
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) z : B)),
        Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
          ((f : (a : A) → B) (y * z) : B)
Tactic: induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ Commute a b
have algebraMap : ∀ (r : R), Commute a ((algebraMap R A : (a : R) → A) r)
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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)
⊢ Commute a b
have 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)
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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)
⊢ Commute a b
have 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)
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s 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)
have 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)))
Tactic: rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s 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)))
have e_s : ∀ (z : A),
  z ∈ (↑(Submonoid.closure (s ∪ t)) : Set A) ↔ z ∈ (↑(Submonoid.closure s) : Set A) * (↑(Submonoid.closure t) : Set A)
Tactic: congr 1 with z
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
s : Set A
x : A
⊢ 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
have 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
Tactic: rw [← Subalgebra.mem_toSubring, adjoin_eq_ring_closure]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
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
⊢ 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
have 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
Tactic: rw [← Subalgebra.mem_toSubring, adjoin_eq_ring_closure]
-- 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
e : A →ₐ[R] B
x : A
⊢ Subalgebra.map e R[x] = R[((e : (a : A) → B) x : B)]
have rw : Eq (α := Subalgebra R B) (adjoin R (Set.image (α := A) (⇑e : (a : A) → B) {x})) R[((e : (a : A) → B) x : B)]
Tactic: rw [map_adjoin, Set.image_singleton]
-- 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
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)]
⊢ Subalgebra.map e R[x] = R[((e : (a : A) → B) x : B)]
have rw₁ : Eq (α := Subalgebra R B) R[((e : (a : A) → B) x : B)] R[((e : (a : A) → B) x : B)]
Tactic: rw [map_adjoin, Set.image_singleton]
-- 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 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
⊢ 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
have this : ∀ (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
-- 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) =
  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: 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) ⋯) =
    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)
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) =
  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: convert! congr_arg₂ (· + ·) h₁ h₂