awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
p : Submodule R M
q : Submodule S N
x : ↥p
y : ↥q
⊢ Eq.{u_9 + 1} (α := P)
    ((((f.domRestrict₁₂ p q : (a : ↥p) → ↥q →ₛₗ[σ₁₂] P) x : LinearMap.{u_3, u_4, u_7, u_9} σ₁₂ (↥q) P) : (a : ↥q) → P)
        y :
      P)
    ((((f : (a : M) → N →ₛₗ[σ₁₂] P) (↑x : M) : N →ₛₗ[σ₁₂] P) : (a : N) → P) (↑y : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : 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 P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst_30 : Semiring R'
inst_31 : Semiring S'
inst_32 : Module R' M
inst_33 : Module S' N
inst_34 : Module R' Pₗ
inst_35 : Module S' Pₗ
inst_36 : SMulCommClass S' R' Pₗ
inst_37 : SMul S' S
inst_38 : IsScalarTower S' S N
inst_39 : IsScalarTower S' S Pₗ
inst_40 : SMul R' R
inst_41 : IsScalarTower R' R M
inst_42 : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x : N
dsimp :
  (((B : (a : M) → N →ₗ[S] Pₗ) (r' • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
⊢ (fun (x1 : M) (x2 : N) ↦ ((((B : (a : M) → N →ₗ[S] Pₗ) x1 : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x2 : Pₗ)) (r' • m) x =
    HSMul.hSMul (β := Pₗ) r'
      ((fun (x1 : M) (x2 : N) ↦ ((((B : (a : M) → N →ₗ[S] Pₗ) x1 : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x2 : Pₗ)) m x)

Tactic:
dsimp only
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : 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 P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst_30 : Semiring R'
inst_31 : Semiring S'
inst_32 : Module R' M
inst_33 : Module S' N
inst_34 : Module R' Pₗ
inst_35 : Module S' Pₗ
inst_36 : SMulCommClass S' R' Pₗ
inst_37 : SMul S' S
inst_38 : IsScalarTower S' S N
inst_39 : IsScalarTower S' S Pₗ
inst_40 : SMul R' R
inst_41 : IsScalarTower R' R M
inst_42 : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x : N
rw :
  (((B : (a : M) → N →ₗ[S] Pₗ) (HSMul.hSMul (β := R) r' 1 • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
rw₁ :
  HSMul.hSMul (β := Pₗ) (HSMul.hSMul (β := R) r' 1)
      ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ) =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
rw₂ rw₃ :
  HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ) =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
⊢ (((B : (a : M) → N →ₗ[S] Pₗ) (r' • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)

Tactic:
rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul]

Premises used: smul_one_smul, LinearMap.map_smul₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
N : Type u_7
Pₗ : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R M
inst_6 : Module S N
inst_7 : Module R Pₗ
inst_8 : Module S Pₗ
inst_9 : SMulCommClass S R Pₗ
R' : Type u_14
S' : Type u_15
inst_10 : Semiring R'
inst_11 : Semiring S'
inst_12 : Module R' M
inst_13 : Module S' N
inst_14 : Module R' Pₗ
inst_15 : Module S' Pₗ
inst_16 : SMulCommClass S' R' Pₗ
inst_17 : SMul S' S
inst_18 : IsScalarTower S' S N
inst_19 : IsScalarTower S' S Pₗ
inst_20 : SMul R' R
inst_21 : IsScalarTower R' R M
inst_22 : IsScalarTower R' R Pₗ
⊢ Injective (α := M →ₗ[R] N →ₗ[S] Pₗ) (β := M →ₗ[R'] N →ₗ[S'] Pₗ) (restrictScalars₁₂ R' S')

Tactic:
fun _ _ h ↦ ext₂ (congr_fun₂ h :)

Premises used: LinearMap.congr_fun₂, LinearMap.ext₂, Function.Injective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
N : Type u_7
Pₗ : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R M
inst_6 : Module S N
inst_7 : Module R Pₗ
inst_8 : Module S Pₗ
inst_9 : SMulCommClass S R Pₗ
R' : Type u_14
S' : Type u_15
inst_10 : Semiring R'
inst_11 : Semiring S'
inst_12 : Module R' M
inst_13 : Module S' N
inst_14 : Module R' Pₗ
inst_15 : Module S' Pₗ
inst_16 : SMulCommClass S' R' Pₗ
inst_17 : SMul S' S
inst_18 : IsScalarTower S' S N
inst_19 : IsScalarTower S' S Pₗ
inst_20 : SMul R' R
inst_21 : IsScalarTower R' R M
inst_22 : IsScalarTower R' R Pₗ
B B' : M →ₗ[R] N →ₗ[S] Pₗ
⊢ Eq (α := M →ₗ[R'] N →ₗ[S'] Pₗ) (restrictScalars₁₂ R' S' B) (restrictScalars₁₂ R' S' B') ↔ B = B'

Tactic:
(restrictScalars₁₂_injective R' S').eq_iff

Premises used: Function.Injective.eq_iff, LinearMap.restrictScalars₁₂_injective
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R₀ : Type u_14
inst_12 : Semiring R₀
inst_13 : Module R₀ P
inst_14 : SMulCommClass S₂ R₀ P
inst_15 : SMulCommClass R₂ R₀ P
⊢ Eq (α := (N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P) ≃ₗ[R₀] M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (LinearEquiv.symm lflip) lflip

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearMap.mk₂'ₛₗ, LinearMap.lflip, LinearMap.flip, rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R₀ : Type u_14
inst_12 : Semiring R₀
inst_13 : Module R₀ P
inst_14 : SMulCommClass S₂ R₀ P
inst_15 : SMulCommClass R₂ R₀ P
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
⊢ (lflip : (a : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) → N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P) f = f.flip

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.flip, 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : Module R M
inst_5 : Module R Nₗ
inst_6 : Module R Pₗ
f : M → Nₗ → Pₗ
H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n
H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n
H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂
H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n
m : M
n : Nₗ
⊢ (((mk₂ R f H1 H2 H3 H4 : (a : M) → Nₗ →ₗ[R] Pₗ) m : Nₗ →ₗ[R] Pₗ) : (a : Nₗ) → Pₗ) n = f m n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
x : Qₗ
y : Qₗ'
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ g g' : (a : Qₗ) → Qₗ' →ₗ[R₂] Pₗ) x : Qₗ' →ₗ[R₂] Pₗ) : (a : Qₗ') → Pₗ) y : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
        ((g' : (a : Qₗ') → N) y : N) :
      Pₗ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R₁ Mₗ
inst_6 : Module R₂ N
inst_7 : Module R₂ Pₗ
inst_8 : Module R₁ Pₗ
inst_9 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
h :
  ∀ (x : Mₗ) (x_1 : N),
    Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ id id : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
      ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
⊢ f.compl₁₂ id id = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R₁ Mₗ
inst_6 : Module R₂ N
inst_7 : Module R₂ Pₗ
inst_8 : Module R₁ Pₗ
inst_9 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
x : Mₗ
x_1 : N
h :
  Eq.{u_9 + 1} (α := Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((id : (a : Mₗ) → Mₗ) x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
        ((id : (a : N) → N) x_1 : N) :
      Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
h₁ :
  Eq.{u_9 + 1} (α := Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) (_root_.id x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) (_root_.id x_1) : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ id id : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)

Tactic:
simp_rw [compl₁₂_apply, id_coe, _root_.id]

Premises used: LinearMap.id_coe, id, LinearMap.compl₁₂_apply
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
Tₗ : Type u_12
inst_13 : AddCommMonoid Tₗ
inst_14 : Module R₁ Tₗ
inst_15 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
h : Tₗ →ₗ[R₁] Qₗ
⊢ f.compl₁₂ (g ∘ₗ h) g' = f.compl₁₂ g g' ∘ₗ h

Tactic:
rfl

Premises used: LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
Tₗ' : Type u_13
inst_13 : AddCommMonoid Tₗ'
inst_14 : Module R₂ Tₗ'
inst_15 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
h' : Tₗ' →ₗ[R₂] Qₗ'
⊢ f.compl₁₂ g (g' ∘ₗ h') = (f.compl₁₂ g g').compl₂ h'

Tactic:
rfl

Premises used: LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst_13 : AddCommMonoid Tₗ
inst_14 : AddCommMonoid Tₗ'
inst_15 : Module R₁ Tₗ
inst_16 : Module R₂ Tₗ'
inst_17 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
h : Tₗ →ₗ[R₁] Qₗ
h' : Tₗ' →ₗ[R₂] Qₗ'
⊢ f.compl₁₂ (g ∘ₗ h) (g' ∘ₗ h') = (f.compl₁₂ g g').compl₁₂ h h'

Tactic:
rfl

Premises used: LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
mp : f₁.compl₁₂ g g' = f₂.compl₁₂ g g' → f₁ = f₂
mpr : f₁ = f₂ → f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
mp :
  ∀ (x : Mₗ) (y : N),
    Eq.{u_9 + 1} (α := Pₗ) ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
      ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
⊢ f₁ = f₂

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : N
mp :
  ∀ (x' : Qₗ),
    Eq.{u_9 + 1} (α := Pₗ)
      ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
      ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)

Tactic:
obtain ⟨x', rfl⟩ := hₗ x

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : N
x' : Qₗ
mp :
  ∀ (y' : Qₗ'),
    Eq.{u_9 + 1} (α := Pₗ)
      ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
          ((g' : (a : Qₗ') → N) y' : N) :
        Pₗ)
      ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
          ((g' : (a : Qₗ') → N) y' : N) :
        Pₗ)
⊢ Eq.{u_9 + 1} (α := Pₗ)
    ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)

Tactic:
obtain ⟨y', rfl⟩ := hᵣ y

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f₁.compl₁₂ g g' : (a : Qₗ) → Qₗ' →ₗ[R₂] Pₗ) x' : Qₗ' →ₗ[R₂] Pₗ) : (a : Qₗ') → Pₗ) y' : Pₗ)
    ((((f₂.compl₁₂ g g' : (a : Qₗ) → Qₗ' →ₗ[R₂] Pₗ) x' : Qₗ' →ₗ[R₂] Pₗ) : (a : Qₗ') → Pₗ) y' : Pₗ)

Tactic:
LinearMap.congr_fun₂ h x' y'

Premises used: LinearMap.congr_fun₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁ = f₂
mpr : f₁.compl₁₂ g g' = f₁.compl₁₂ g g'
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
⊢ f₁.compl₁₂ g g' = f₁.compl₁₂ g g'

Tactic:
rfl
-- 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ₗ
inst_29 : Module R A
inst_30 : Module A M
inst_31 : Module A Qₗ
inst_32 : SMulCommClass R A Qₗ
inst_33 : IsScalarTower R A Qₗ
inst_34 : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x : A
x_1 : M
x_2 : Nₗ
⊢ Eq.{u_10 + 1} (α := Qₗ)
    (((↑R :
                {S : Type u_1} →
                  {M : Type u_9} →
                    {M₂ : Type u_10} →
                      [inst : Semiring R] →
                        [inst_35 : Semiring S] →
                          [inst_36 : AddCommMonoid M] →
                            [inst_37 : AddCommMonoid M₂] →
                              [inst_38 : Module R M] →
                                [inst_39 : Module R M₂] →
                                  [inst_40 : Module S M] →
                                    [inst_41 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              g ∘ₗ
            (f : (a : M) → Nₗ →ₗ[R] Pₗ) (x • x_1) :
          (a : Nₗ) → Qₗ)
        x_2 :
      Qₗ)
    ((HSMul.hSMul (α := A) (β := Nₗ →ₗ[R] Qₗ) ((RingHom.id A : (a : A) → A) x : A)
            ((↑R :
                  {S : Type u_1} →
                    {M : Type u_9} →
                      {M₂ : Type u_10} →
                        [inst : Semiring R] →
                          [inst_35 : Semiring S] →
                            [inst_36 : AddCommMonoid M] →
                              [inst_37 : AddCommMonoid M₂] →
                                [inst_38 : Module R M] →
                                  [inst_39 : Module R M₂] →
                                    [inst_40 : Module S M] →
                                      [inst_41 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                g ∘ₗ
              (f : (a : M) → Nₗ →ₗ[R] Pₗ) x_1) :
          (a : Nₗ) → Qₗ)
        x_2 :
      Qₗ)

Tactic:
simp