awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ productMap f g = AlgHom.comp (lmul' R) (map f g)
have ha : ∀ (x : A),
  Eq.{uS + 1} (α := S) (((productMap f g).comp includeLeft : (a : A) → S) x : S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
            (includeLeft : A →ₐ[R] A ⊗[R] B) :
          (a : A) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
ha :
  ∀ (x : A),
    Eq.{uS + 1} (α := S) (((productMap f g).comp includeLeft : (a : A) → S) x : S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
              (includeLeft : A →ₐ[R] A ⊗[R] B) :
            (a : A) → S)
          x :
        S)
⊢ productMap f g = AlgHom.comp (lmul' R) (map f g)
have hb : ∀ (x : B),
  Eq.{uS + 1} (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (productMap f g)) includeRight : (a : B) → S) x : S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
            includeRight :
          (a : B) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (productMap f g).range = f.range ⊔ g.range
have rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₂ : Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₃ : Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
    Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₄ : (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
    Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₅ : (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔ (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₆ : (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔ (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₇ : (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
  f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₇ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
    f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₈ : (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₇ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
    f.range ⊔ g.range
rw₈ :
  (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₉ : (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₇ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
    f.range ⊔ g.range
rw₈ :
  (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range = f.range ⊔ g.range
rw₉ : (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₁₀ : f.range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₇ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
    f.range ⊔ g.range
rw₈ :
  (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range = f.range ⊔ g.range
rw₉ : (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
rw₁₀ : f.range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range
have rw₁₁ : f.range ⊔ g.range = f.range ⊔ g.range
Tactic: rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
a b : A
f g : End R M
⊢ (tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) ((a * b) ⊗ₜ[R] (f * g)) =
    HMul.hMul (α := End A (A ⊗[R] M)) (β := End A (A ⊗[R] M))
      ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (a ⊗ₜ[R] f) : End A (A ⊗[R] M))
      ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (b ⊗ₜ[R] g) : End A (A ⊗[R] M))
have h : ∀ (x : A ⊗[R] M),
  Eq (α := A ⊗[R] M)
    ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) ((a * b) ⊗ₜ[R] (f * g)) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((HMul.hMul (α := End A (A ⊗[R] M)) (β := End A (A ⊗[R] M))
            ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (a ⊗ₜ[R] f) : End A (A ⊗[R] M))
            ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (b ⊗ₜ[R] g) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
Tactic: apply LinearMap.ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
⊢ Eq (α := End A (A ⊗[R] M))
    ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] 1) : End A (A ⊗[R] M))
    (1 : End A (A ⊗[R] M))
have h : ∀ (x : A ⊗[R] M),
  Eq (α := A ⊗[R] M)
    ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] 1) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((1 : (a : A ⊗[R] M) → A ⊗[R] M) x : A ⊗[R] M)
Tactic: apply LinearMap.ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
    (lmul' (ULift.{u₁, u_4} R))
    (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
      (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
        ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u_8, u_5} (S ⊗[R] S)))
have ha : ∀ (x : ULift.{u₂, u_5} S),
  Eq.{u_5 + 1} (α := S)
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (lmul' (ULift.{u₁, u_4} R)) includeLeft : (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S) x))
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
            (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
              (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                  ULift.{u_8, u_5} (S ⊗[R] S)))
            includeLeft :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))
Tactic: ext