-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_inl_union_inr_eq_prod (s) (t) :
    adjoin R (LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1})) =
      (adjoin R s).prod (adjoin R t)

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
  mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
  mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
let P := adjoin R (LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}))

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
replace Hb : ((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
Hb : (0, b) ∈ P
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) = (adjoin R s).prod (adjoin R t)

Tactic:
apply le_antisymm

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) ≤ (adjoin R s).prod (adjoin R t)

case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ (adjoin R s).prod (adjoin R t) ≤ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ (adjoin R s).prod (adjoin R t) ≤ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩

Result:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))