awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
A : Type u_1
R : Type u_2
inst : Semiring A
inst_1 : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid Nₗ
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
inst_9 : Module A Pₗ
inst_10 : SMulCommClass R A Pₗ
inst_11 : Module R A
inst_12 : Module A M
inst_13 : Module A Qₗ
inst_14 : SMulCommClass R A Qₗ
inst_15 : IsScalarTower R A Qₗ
inst_16 : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
m : M
n : Nₗ
⊢ Eq.{u_10 + 1} (α := Qₗ) ((((f.compr₂ g : (a : M) → Nₗ →ₗ[R] Qₗ) m : Nₗ →ₗ[R] Qₗ) : (a : Nₗ) → Qₗ) n : Qₗ)
    ((g : (a : Pₗ) → Qₗ) ((((f : (a : M) → Nₗ →ₗ[R] Pₗ) m : Nₗ →ₗ[R] Pₗ) : (a : Nₗ) → Pₗ) n : Pₗ) : Qₗ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
A : Type u_1
R : Type u_2
inst : Semiring A
inst_1 : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid Nₗ
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R Nₗ
inst_6 : Module R Pₗ
inst_7 : Module A Pₗ
inst_8 : SMulCommClass R A Pₗ
inst_9 : Module R A
inst_10 : Module A M
inst_11 : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
⊢ f.compr₂ id = f

Tactic:
rfl

Premises used: LinearMap.compr₂, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
A : Type u_1
R : Type u_2
inst : Semiring A
inst_1 : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid Nₗ
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
inst_9 : Module A Pₗ
inst_10 : SMulCommClass R A Pₗ
Tₗ : Type u_14
inst_11 : AddCommMonoid Tₗ
inst_12 : Module R Tₗ
inst_13 : Module A Tₗ
inst_14 : Module R A
inst_15 : Module A M
inst_16 : Module A Qₗ
inst_17 : SMulCommClass R A Qₗ
inst_18 : SMulCommClass R A Tₗ
inst_19 : IsScalarTower R A Qₗ
inst_20 : IsScalarTower R A Pₗ
inst_21 : IsScalarTower R A Tₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
h : Qₗ →ₗ[A] Tₗ
⊢ Eq (α := M →ₗ[A] Nₗ →ₗ[R] Tₗ) (f.compr₂ (h ∘ₗ g)) (compr₂ (f.compr₂ g) h)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, LinearMap.compr₂, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : AddCommMonoid Qₗ
inst_5 : Module R M
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[R] Qₗ
hf : Injective (α := M) (β := Nₗ →ₗ[R] Pₗ) (⇑f : (a : M) → Nₗ →ₗ[R] Pₗ)
hg : Injective.{u_9 + 1, u_10 + 1} (α := Pₗ) (β := Qₗ) (⇑g : (a : Pₗ) → Qₗ)
⊢ Injective (α := M) (β := Nₗ →ₗ[R] Qₗ) (⇑(f.compr₂ g) : (a : M) → Nₗ →ₗ[R] Qₗ)

Tactic:
hg.injective_linearMapComp_left.comp hf

Premises used: Function.Injective.injective_linearMapComp_left, Function.Injective.comp
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : AddCommMonoid Qₗ
inst_5 : Module R M
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[R] Qₗ
hf : Surjective (α := M) (β := Nₗ →ₗ[R] Pₗ) (⇑f : (a : M) → Nₗ →ₗ[R] Pₗ)
hg : ∃ (g' : Qₗ →ₗ[R] Pₗ), g ∘ₗ g' = id
⊢ Surjective (α := M) (β := Nₗ →ₗ[R] Qₗ) (⇑(f.compr₂ g) : (a : M) → Nₗ →ₗ[R] Qₗ)

Tactic:
(surjective_comp_left_of_exists_rightInverse hg).comp hf

Premises used: Function.Surjective.comp, LinearMap.surjective_comp_left_of_exists_rightInverse
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : AddCommMonoid Qₗ
inst_5 : Module R M
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ ≃ₗ[R] Qₗ
hf : Surjective (α := M) (β := Nₗ →ₗ[R] Pₗ) (⇑f : (a : M) → Nₗ →ₗ[R] Pₗ)
⊢ (↑g : Pₗ →ₗ[R] Qₗ) ∘ₗ (↑g.symm : Qₗ →ₗ[R] Pₗ) = id

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : AddCommMonoid Qₗ
inst_5 : Module R M
inst_6 : Module R Nₗ
inst_7 : Module R Pₗ
inst_8 : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ ≃ₗ[R] Qₗ
hf : Bijective (α := M) (β := Nₗ →ₗ[R] Pₗ) (⇑f : (a : M) → Nₗ →ₗ[R] Pₗ)
⊢ Bijective (α := M) (β := Nₗ →ₗ[R] Qₗ) (⇑(f.compr₂ (↑g : Pₗ →ₗ[R] Qₗ)) : (a : M) → Nₗ →ₗ[R] Qₗ)

Tactic:
⟨injective_compr₂_of_injective f g.toLinearMap hf.1 g.bijective.1,
  surjective_compr₂_of_equiv f g hf.2⟩

Premises used: LinearMap.injective_compr₂_of_injective, LinearEquiv.bijective, LinearMap.surjective_compr₂_of_equiv, LinearEquiv.toLinearMap, And.right, And.left, And.intro, Function.Bijective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
M : Type u_17
N : Type u_18
P : Type u_19
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R₂ N
inst_8 : Module R₃ P
σ₁₂ : R →+* R₂
σ₁₃ : R →+* R₃
σ₂₃ : R₂ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : N →ₛₗ[σ₂₃] P
g : M →ₛₗ[σ₁₂] N
x : M
⊢ Eq.{u_19 + 1} (α := P)
    ((((((llcomp R₃ M N P : (a : N →ₛₗ[σ₂₃] P) → (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P) f :
                  (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P) :
                (a : M →ₛₗ[σ₁₂] N) → M →ₛₗ[σ₁₃] P)
              g :
            M →ₛₗ[σ₁₃] P) :
          (a : M) → P)
        x :
      P)
    ((f : (a : N) → P) ((g : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
M : Type u_17
N : Type u_18
P : Type u_19
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R₂ N
inst_8 : Module R₃ P
σ₁₂ : R →+* R₂
σ₁₃ : R →+* R₃
σ₂₃ : R₂ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : N →ₛₗ[σ₂₃] P
g : M →ₛₗ[σ₁₂] N
⊢ (((llcomp R₃ M N P : (a : N →ₛₗ[σ₂₃] P) → (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P) f :
          (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P) :
        (a : M →ₛₗ[σ₁₂] N) → M →ₛₗ[σ₁₃] P)
      g =
    f ∘ₛₗ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P →ₛₗ[σ₃₄] Q
m : M
n : N
⊢ Eq.{u_20 + 1} (α := Q) ((((f.compr₂ₛₗ g : (a : M) → N →ₛₗ[σ₂₄] Q) m : N →ₛₗ[σ₂₄] Q) : (a : N) → Q) n : Q)
    ((g : (a : P) → Q) ((((f : (a : M) → N →ₛₗ[σ₂₃] P) m : N →ₛₗ[σ₂₃] P) : (a : N) → P) n : P) : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
M : Type u_17
N : Type u_18
P : Type u_19
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R₂ N
inst_8 : Module R₃ P
σ₁₃ : R →+* R₃
σ₂₃ : R₂ →+* R₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
⊢ f.compr₂ₛₗ id = f

Tactic:
rfl

Premises used: LinearMap.compr₂ₛₗ, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
Q' : Type u_21
R₅ : Type u_22
inst_14 : CommSemiring R₅
inst_15 : AddCommMonoid Q'
inst_16 : Module R₅ Q'
σ₁₅ : R →+* R₅
σ₂₅ : R₂ →+* R₅
σ₃₅ : R₃ →+* R₅
σ₄₅ : R₄ →+* R₅
inst_17 : RingHomCompTriple σ₁₃ σ₃₅ σ₁₅
inst_18 : RingHomCompTriple σ₁₄ σ₄₅ σ₁₅
inst_19 : RingHomCompTriple σ₂₃ σ₃₅ σ₂₅
inst_20 : RingHomCompTriple σ₂₄ σ₄₅ σ₂₅
inst_21 : RingHomCompTriple σ₃₄ σ₄₅ σ₃₅
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P →ₛₗ[σ₃₄] Q
h : Q →ₛₗ[σ₄₅] Q'
⊢ f.compr₂ₛₗ (h ∘ₛₗ g) = (f.compr₂ₛₗ g).compr₂ₛₗ h

Tactic:
rfl

Premises used: LinearMap.compr₂ₛₗ, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P →ₛₗ[σ₃₄] Q
hf : Injective (α := M) (β := N →ₛₗ[σ₂₃] P) (⇑f : (a : M) → N →ₛₗ[σ₂₃] P)
hg : Injective.{u_19 + 1, u_20 + 1} (α := P) (β := Q) (⇑g : (a : P) → Q)
⊢ Injective (α := M) (β := N →ₛₗ[σ₂₄] Q) (⇑(f.compr₂ₛₗ g) : (a : M) → N →ₛₗ[σ₂₄] Q)

Tactic:
hg.injective_linearMapComp_left.comp hf

Premises used: Function.Injective.injective_linearMapComp_left, Function.Injective.comp
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_15 : RingHomInvPair σ₃₄ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P →ₛₗ[σ₃₄] Q
hf : Surjective (α := M) (β := N →ₛₗ[σ₂₃] P) (⇑f : (a : M) → N →ₛₗ[σ₂₃] P)
hg : ∃ (g' : Q →ₛₗ[σ₄₃] P), g ∘ₛₗ g' = id
⊢ Surjective (α := M) (β := N →ₛₗ[σ₂₄] Q) (⇑(f.compr₂ₛₗ g) : (a : M) → N →ₛₗ[σ₂₄] Q)

Tactic:
(surjective_comp_left_of_exists_rightInverse hg).comp hf

Premises used: Function.Surjective.comp, LinearMap.surjective_comp_left_of_exists_rightInverse
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_15 : RingHomInvPair σ₃₄ σ₄₃
inst_16 : RingHomInvPair σ₄₃ σ₃₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P ≃ₛₗ[σ₃₄] Q
hf : Surjective (α := M) (β := N →ₛₗ[σ₂₃] P) (⇑f : (a : M) → N →ₛₗ[σ₂₃] P)
⊢ (↑g : P →ₛₗ[σ₃₄] Q) ∘ₛₗ (↑g.symm : Q →ₛₗ[σ₄₃] P) = id

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : CommSemiring R₄
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : AddCommMonoid Q
inst_8 : Module R M
inst_9 : Module R₂ N
inst_10 : Module R₃ P
inst_11 : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_15 : RingHomInvPair σ₃₄ σ₄₃
inst_16 : RingHomInvPair σ₄₃ σ₃₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P ≃ₛₗ[σ₃₄] Q
hf : Bijective (α := M) (β := N →ₛₗ[σ₂₃] P) (⇑f : (a : M) → N →ₛₗ[σ₂₃] P)
⊢ Bijective (α := M) (β := N →ₛₗ[σ₂₄] Q) (⇑(f.compr₂ₛₗ (↑g : P →ₛₗ[σ₃₄] Q)) : (a : M) → N →ₛₗ[σ₂₄] Q)

Tactic:
⟨injective_compr₂ₛₗ_of_injective f g.toLinearMap hf.1 g.bijective.1,
  surjective_compr₂ₛₗ_of_equiv f g hf.2⟩

Premises used: LinearEquiv.bijective, LinearMap.injective_compr₂ₛₗ_of_injective, LinearEquiv.toLinearMap, And.right, And.left, And.intro, LinearMap.surjective_compr₂ₛₗ_of_equiv, Function.Bijective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring A
inst_1 : CommSemiring R
inst_2 : Semiring R₁
inst_3 : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid Mₗ
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid Nₗ
inst_8 : AddCommMonoid Pₗ
inst_9 : AddCommMonoid Qₗ
inst_10 : AddCommMonoid Qₗ'
inst_11 : Module R M
inst_12 : Module R Mₗ
inst_13 : Module R₁ Mₗ
inst_14 : Module R₂ N
inst_15 : Module R Nₗ
inst_16 : Module R Pₗ
inst_17 : Module R₂ Pₗ
inst_18 : Module R₁ Pₗ
inst_19 : Module R Qₗ
inst_20 : Module R₁ Qₗ
inst_21 : Module R Qₗ'
inst_22 : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst_23 : AddCommMonoid Tₗ
inst_24 : AddCommMonoid Tₗ'
inst_25 : Module R₁ Tₗ
inst_26 : Module R₂ Tₗ'
inst_27 : Module A Pₗ
inst_28 : SMulCommClass R A Pₗ
r s : R
m : M
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) s (r • m) = HSMul.hSMul (β := M) r ((fun (x1 : R) (x2 : M) ↦ x1 • x2) s m)

Tactic:
simp only [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ Eq.{u_5 + 1} (α := M →ₗ[R] M) ((lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M)
    (DistribSMul.toLinearMap R M r : M →ₗ[R] M)

Tactic:
rfl

Premises used: DistribSMul.toLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_2
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
⊢ (((lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) m = r • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : R
hx : x ≠ 0
⊢ Injective.{u_2 + 1, u_2 + 1} (α := M) (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) x : M →ₗ[R] M) : (a : M) → M)

Tactic:
smul_right_injective _ hx

Premises used: smul_right_injective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
a : R
ha : a ≠ 0
⊢ Eq.{u_2 + 1} (α := Submodule R M)
    (ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((lsmul R M : (a : R) → M →ₗ[R] M) a)) ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective (LinearMap.lsmul_injective ha)

Premises used: LinearMap.lsmul_injective, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
⊢ Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((k ∘ₗ
            codLift
              ((↑S :
                    {S_1 : Type u_1} →
                      {M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring S] →
                            [inst_15 : Semiring S_1] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [inst_20 : Module S_1 M] →
                                        [inst_21 : Module S_1 M₂] →
                                          [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  f ∘ₗ
                i)
              k hk hf :
          (a : M') → P)
        m :
      P)

Tactic:
have : k (restrictScalarsRange i k hk f hf m) =
      (k ∘ₗ ((f.restrictScalars S).comp i).codLift k hk hf) m :=
    rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
p : P'
rw :
  p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
    Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
rw₁ rw₂ :
  p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔ p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m
⊢ p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
    Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)

Tactic:
rw [← restrictScalarsRange_apply i k hk f hf m, hk.eq_iff]

Premises used: Function.Injective.eq_iff, LinearMap.restrictScalarsRange_apply
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
rw :
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
      ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
rw₁ :
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
⊢ Eq.{u_6 + 1} (α := P') ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') (0 : P') ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)

Tactic:
rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]

Premises used: Function.Injective.eq_iff, map_zero, LinearMap.restrictScalarsRange_apply
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S M
inst_10 : Module S N
inst_11 : Module S P
inst_12 : IsScalarTower S R M
inst_13 : IsScalarTower S R N
inst_14 : IsScalarTower S R P
inst_15 : AddCommMonoid M'
inst_16 : Module S M'
inst_17 : AddCommMonoid N'
inst_18 : Module S N'
inst_19 : AddCommMonoid P'
inst_20 : Module S P'
inst_21 : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective.{u_8 + 1, u_5 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
B : M →ₗ[R] N →ₗ[R] P
hB :
  ∀ (m : M') (n : N'),
    Membership.mem (α := P) k.range
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
m : M'
n : N'
⊢ Eq.{u_5 + 1} (α := P)
    ((k : (a : P') → P)
        ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P') :
      P)
    ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)

Tactic:
simp [restrictScalarsRange₂]

Premises used: LinearMap.restrictScalarsRange₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S M
inst_10 : Module S N
inst_11 : Module S P
inst_12 : IsScalarTower S R M
inst_13 : IsScalarTower S R N
inst_14 : IsScalarTower S R P
inst_15 : AddCommMonoid M'
inst_16 : Module S M'
inst_17 : AddCommMonoid N'
inst_18 : Module S N'
inst_19 : AddCommMonoid P'
inst_20 : Module S P'
inst_21 : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective.{u_8 + 1, u_5 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
B : M →ₗ[R] N →ₗ[R] P
hB :
  ∀ (m : M') (n : N'),
    Membership.mem (α := P) k.range
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
m : M'
n : N'
p : P'
rw :
  p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((k : (a : P') → P)
          ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P') :
        P)
rw₁ rw₂ :
  p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n
⊢ p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)

Tactic:
rw [← restrictScalarsRange₂_apply i j k hk B hB m n, hk.eq_iff]

Premises used: LinearMap.restrictScalarsRange₂_apply, Function.Injective.eq_iff