-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem map (H : M.LinearDisjoint N) {T : Type w} [Semiring T] [Algebra R T]
    {F : Type*} [FunLike F S T] [AlgHomClass F R S T] (f : F) (hf : Function.Injective f) :
    (M.map f).LinearDisjoint (N.map f)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
⊢ (Submodule.map f M).LinearDisjoint (Submodule.map f N)

Tactic:
rw [linearDisjoint_iff] at H ⊢

Result:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
this :
  (Submodule.map f M).mulMap (Submodule.map f N) ∘ₗ
      ↑(TensorProduct.congr (equivMapOfInjective f hf M) (equivMapOfInjective f hf N)) =
    ↑f ∘ₗ M.mulMap N
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))

Tactic:
replace H : Function.Injective ((f : S →ₗ[R] T) ∘ₗ mulMap M N) := hf.comp H

Result:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
this :
  (Submodule.map f M).mulMap (Submodule.map f N) ∘ₗ
      ↑(TensorProduct.congr (equivMapOfInjective f hf M) (equivMapOfInjective f hf N)) =
    ↑f ∘ₗ M.mulMap N
H : Function.Injective ⇑(↑f ∘ₗ M.mulMap N)
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
this :
  (Submodule.map f M).mulMap (Submodule.map f N) ∘ₗ
      ↑(TensorProduct.congr (equivMapOfInjective f hf M) (equivMapOfInjective f hf N)) =
    ↑f ∘ₗ M.mulMap N
H : Function.Injective ⇑(↑f ∘ₗ M.mulMap N)
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))

Tactic:
simpa only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] using H

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))

Tactic:
have : _ ∘ₗ
  (TensorProduct.congr (M.equivMapOfInjective f hf) (N.equivMapOfInjective f hf)).toLinearMap
    = _ := M.mulMap_map_comp_eq N f

Result:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
hf : Function.Injective ⇑f
this :
  (Submodule.map f M).mulMap (Submodule.map f N) ∘ₗ
      ↑(TensorProduct.congr (equivMapOfInjective f hf M) (equivMapOfInjective f hf N)) =
    ↑f ∘ₗ M.mulMap N
⊢ Function.Injective ⇑((Submodule.map f M).mulMap (Submodule.map f N))