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
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
r : R
⊢ p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯

Tactic:
exact algebraMap_left _ _ hz
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 + y_1) z ⋯ ⋯

Tactic:
add_left _ _ _ _ _ _ h₁ h₂
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 + y_1) z ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : ∀ (r : R), p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯
mem₂ :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯), p (x * y) z ⋯ ⋯
mem₃ :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯), p (x + y) z ⋯ ⋯
⊢ p x z hx ⋯

Tactic:
induction hx using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂

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
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r : R
x_1 : A
h : x_1 ∈ s
⊢ p x_1 ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
algebraMap_right _ _ h
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r : R
x_1 : A
h : x_1 ∈ s
⊢ p x_1 ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
exact algebraMap_right _ _ h
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r r_1 : R
⊢ p ((algebraMap R A : (a : R) → A) r_1) ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
algebraMap_both _ _
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r r_1 : R
⊢ p ((algebraMap R A : (a : R) → A) r_1) ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
exact algebraMap_both _ _
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r : R
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 ((algebraMap R A : (a : R) → A) r) hx ⋯
h₂ : p y_1 ((algebraMap R A : (a : R) → A) r) hy ⋯
⊢ p (x_1 * y_1) ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂
-- 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
p :
  (x y : A) →
    Membership.mem (γ := Subalgebra R A) (adjoin R s) x → Membership.mem (γ := Subalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := Subalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r : R
x_1 y_1 : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := Subalgebra R A) (adjoin R s) y_1
h₁ : p x_1 ((algebraMap R A : (a : R) → A) r) hx ⋯
h₂ : p y_1 ((algebraMap R A : (a : R) → A) r) hy ⋯
⊢ p (x_1 * y_1) ((algebraMap R A : (a : R) → A) r) ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂