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
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₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
c : R
n : N
m : M
⊢ (fun (n : N) (m : M) ↦ ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)) n (c • m) =
    HSMul.hSMul.{u_2, u_9, u_9} (α := R₂) (β := P) ((ρ₁₂ : (a : R) → R₂) c : R₂)
      ((fun (n : N) (m : M) ↦ ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)) n m)

Tactic:
simp only [map_smulₛₗ _, smul_apply]

Premises used: LinearMap.smul_apply, MulActionSemiHomClass.map_smulₛₗ
-- 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
m : M
n : N
⊢ Eq.{u_9 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
    ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R_1 : Type u_1
R₂_1 : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R_1
inst_1 : Semiring R₂_1
inst_2 : Semiring S
inst_3 : Semiring S₂
M_1 : Type u_5
M₂ : Type u_6
N_1 : Type u_7
N₂ : Type u_8
P_1 : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M_1
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P_1
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R_1 M_1
inst_12 : Module R_1 M₂
inst_13 : Module S N_1
inst_14 : Module S N₂
inst_15 : Module R₂_1 P_1
inst_16 : Module S₂ P_1
inst_17 : Module R_1 P₂
inst_18 : Module S₂ P₂
inst_19 : Module R_1 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_1 M'
inst_24 : Module R₂_1 P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂_1 P_1
inst_27 : SMulCommClass S R_1 Pₗ
inst_28 : SMulCommClass S₂ R₂_1 P'
inst_29 : SMulCommClass S₂ R_1 P₂
ρ₁₂ : R_1 →+* R₂_1
σ₁₂_1 : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst_30 : Semiring R
inst_31 : Semiring R₂
inst_32 : Semiring R₃
inst_33 : Semiring R₄
inst_34 : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst_35 : AddCommMonoid M
inst_36 : AddCommMonoid N
inst_37 : AddCommMonoid P
inst_38 : AddCommMonoid Q
inst_39 : Module R M
inst_40 : Module R₂ N
inst_41 : Module R₃ P
inst_42 : Module R₄ Q
inst_43 : Module R₅ P
inst_44 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_45 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst_46 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x x_1 : M
⊢ (lcompₛₗ R₅ P σ₂₃ g : (a : N →ₛₗ[σ₂₃] P) → Q →ₛₗ[σ₄₃] P) ((h : (a : M) → N →ₛₗ[σ₂₃] P) (x + x_1)) =
    HAdd.hAdd (α := Q →ₛₗ[σ₄₃] P) (β := Q →ₛₗ[σ₄₃] P)
      ((lcompₛₗ R₅ P σ₂₃ g : (a : N →ₛₗ[σ₂₃] P) → Q →ₛₗ[σ₄₃] P) ((h : (a : M) → N →ₛₗ[σ₂₃] P) x) : Q →ₛₗ[σ₄₃] P)
      ((lcompₛₗ R₅ P σ₂₃ g : (a : N →ₛₗ[σ₂₃] P) → Q →ₛₗ[σ₄₃] P) ((h : (a : M) → N →ₛₗ[σ₂₃] P) x_1) : Q →ₛₗ[σ₄₃] P)

Tactic:
simp [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R_1 : Type u_1
R₂_1 : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R_1
inst_1 : Semiring R₂_1
inst_2 : Semiring S
inst_3 : Semiring S₂
M_1 : Type u_5
M₂ : Type u_6
N_1 : Type u_7
N₂ : Type u_8
P_1 : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M_1
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P_1
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R_1 M_1
inst_12 : Module R_1 M₂
inst_13 : Module S N_1
inst_14 : Module S N₂
inst_15 : Module R₂_1 P_1
inst_16 : Module S₂ P_1
inst_17 : Module R_1 P₂
inst_18 : Module S₂ P₂
inst_19 : Module R_1 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_1 M'
inst_24 : Module R₂_1 P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂_1 P_1
inst_27 : SMulCommClass S R_1 Pₗ
inst_28 : SMulCommClass S₂ R₂_1 P'
inst_29 : SMulCommClass S₂ R_1 P₂
ρ₁₂ : R_1 →+* R₂_1
σ₁₂_1 : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst_30 : Semiring R
inst_31 : Semiring R₂
inst_32 : Semiring R₃
inst_33 : Semiring R₄
inst_34 : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst_35 : AddCommMonoid M
inst_36 : AddCommMonoid N
inst_37 : AddCommMonoid P
inst_38 : AddCommMonoid Q
inst_39 : Module R M
inst_40 : Module R₂ N
inst_41 : Module R₃ P
inst_42 : Module R₄ Q
inst_43 : Module R₅ P
inst_44 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_45 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst_46 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x : R
x_1 : M
⊢ (lcompₛₗ R₅ P σ₂₃ g : (a : N →ₛₗ[σ₂₃] P) → Q →ₛₗ[σ₄₃] P) ((h : (a : M) → N →ₛₗ[σ₂₃] P) (x • x_1)) =
    HSMul.hSMul (α := R₅) (β := Q →ₛₗ[σ₄₃] P) ((σ₁₅ : (a : R) → R₅) x : R₅)
      ((lcompₛₗ R₅ P σ₂₃ g : (a : N →ₛₗ[σ₂₃] P) → Q →ₛₗ[σ₄₃] P) ((h : (a : M) → N →ₛₗ[σ₂₃] P) x_1) : Q →ₛₗ[σ₄₃] P)

Tactic:
simp [map_smulₛₗ, lcompₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, LinearMap.lcompₛₗ
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₄
inst_4 : Semiring R₅
σ₂₃ : R₂ →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : Module R M
inst_10 : Module R₂ N
inst_11 : Module R₃ P
inst_12 : Module R₄ Q
inst_13 : Module R₅ P
inst_14 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst_15 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
m : M
q : Q
⊢ Eq.{u_21 + 1} (α := P) ((((h.compl₂ g : (a : M) → Q →ₛₗ[σ₄₃] P) m : Q →ₛₗ[σ₄₃] P) : (a : Q) → P) q : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) m : N →ₛₗ[σ₂₃] P) : (a : N) → P) ((g : (a : Q) → N) q : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
h₁ :
  ∀ (x : M) (x_1 : N),
    Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
      ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
⊢ h.compl₂ id = h

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
x : M
x_1 : N
h₁ :
  Eq.{u_21 + 1} (α := P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) ((id : (a : N) → N) x_1 : N) : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
h₂ :
  Eq.{u_21 + 1} (α := P) ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) (_root_.id x_1) : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
h₃ h₄ :
  Eq.{u_21 + 1} (α := P) ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
⊢ Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)

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

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

Tactic:
rfl

Premises used: rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
M₂ : Type u_6
N : Type u_7
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module S N
inst_8 : Module R N
inst_9 : SMulCommClass R S N
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] N
x : M
⊢ Eq.{u_7 + 1} (α := N) ((((lcomp S N f : (a : M₂ →ₗ[R] N) → M →ₗ[R] N) g : M →ₗ[R] N) : (a : M) → N) x : N)
    ((g : (a : M₂) → N) ((f : (a : M) → M₂) x : M₂) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
M₂ : Type u_6
N : Type u_7
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module S N
inst_8 : Module R N
inst_9 : SMulCommClass R S N
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] N
⊢ (lcomp S N f : (a : M₂ →ₗ[R] N) → M →ₗ[R] N) g = g ∘ₗ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
M₂ : Type u_6
N : Type u_7
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module S N
inst_8 : Module R N
inst_9 : SMulCommClass R S N
g : M →ₗ[R] M₂
surj : Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
⊢ Injective (α := M₂ →ₗ[R] N) (β := M →ₗ[R] N) (⇑(lcomp S N g) : (a : M₂ →ₗ[R] N) → M →ₗ[R] N)

Tactic:
surj.injective_linearMapComp_right

Premises used: Function.Surjective.injective_linearMapComp_right
-- 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
⊢ f.flip.flip = f

Tactic:
LinearMap.ext₂ fun _x _y => (f.flip.flip_apply _ _).trans (f.flip_apply _ _)

Premises used: LinearMap.flip_apply, LinearMap.flip, LinearMap.ext₂, Eq.trans
-- 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 g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : f.flip = g.flip
m : M
n : N
rw rw₁ :
  Eq.{u_9 + 1} (α := P) ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
    ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
⊢ Eq.{u_9 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
    ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)

Tactic:
rw [H]
-- 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
y : N
⊢ Eq.{u_9 + 1} (α := P) (((f : (a : M) → N →ₛₗ[σ₁₂] P) 0 : (a : N) → P) y : P) (0 : P)

Tactic:
(flip f y).map_zero

Premises used: LinearMap.map_zero, LinearMap.flip, DFunLike.coe
-- 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₂
N : Type u_7
inst_4 : AddCommMonoid N
inst_5 : Module S N
M' : Type u_12
P' : Type u_13
inst_6 : AddCommGroup M'
inst_7 : AddCommGroup P'
inst_8 : Module R M'
inst_9 : Module R₂ P'
inst_10 : Module S₂ P'
inst_11 : SMulCommClass S₂ R₂ P'
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P'
x : M'
y : N
⊢ Eq.{u_13 + 1} (α := P') ((((f : (a : M') → N →ₛₗ[σ₁₂] P') (-x) : N →ₛₗ[σ₁₂] P') : (a : N) → P') y : P')
    (-(((f : (a : M') → N →ₛₗ[σ₁₂] P') x : N →ₛₗ[σ₁₂] P') : (a : N) → P') y : P')

Tactic:
(flip f y).map_neg _

Premises used: LinearMap.map_neg, LinearMap.flip, DFunLike.coe
-- 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₂
N : Type u_7
inst_4 : AddCommMonoid N
inst_5 : Module S N
M' : Type u_12
P' : Type u_13
inst_6 : AddCommGroup M'
inst_7 : AddCommGroup P'
inst_8 : Module R M'
inst_9 : Module R₂ P'
inst_10 : Module S₂ P'
inst_11 : SMulCommClass S₂ R₂ P'
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P'
x y : M'
z : N
⊢ (((f : (a : M') → N →ₛₗ[σ₁₂] P') (x - y) : N →ₛₗ[σ₁₂] P') : (a : N) → P') z =
    HSub.hSub (α := P') (β := P') ((((f : (a : M') → N →ₛₗ[σ₁₂] P') x : N →ₛₗ[σ₁₂] P') : (a : N) → P') z : P')
      ((((f : (a : M') → N →ₛₗ[σ₁₂] P') y : N →ₛₗ[σ₁₂] P') : (a : N) → P') z : P')

Tactic:
(flip f z).map_sub _ _

Premises used: LinearMap.flip, LinearMap.map_sub, DFunLike.coe
-- 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
x₁ x₂ : M
y : N
⊢ (((f : (a : M) → N →ₛₗ[σ₁₂] P) (x₁ + x₂) : N →ₛₗ[σ₁₂] P) : (a : N) → P) y =
    HAdd.hAdd (α := P) (β := P) ((((f : (a : M) → N →ₛₗ[σ₁₂] P) x₁ : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)
      ((((f : (a : M) → N →ₛₗ[σ₁₂] P) x₂ : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
(flip f y).map_add _ _

Premises used: LinearMap.map_add, LinearMap.flip, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring S₂
M₂ : Type u_6
N₂ : Type u_8
P₂ : Type u_10
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P₂
inst_6 : Module R M₂
inst_7 : Module S N₂
inst_8 : Module R P₂
inst_9 : Module S₂ P₂
inst_10 : SMulCommClass S₂ R P₂
σ₁₂ : S →+* S₂
f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂
r : R
x : M₂
y : N₂
⊢ (((f : (a : M₂) → N₂ →ₛₗ[σ₁₂] P₂) (r • x) : N₂ →ₛₗ[σ₁₂] P₂) : (a : N₂) → P₂) y =
    HSMul.hSMul (β := P₂) r ((((f : (a : M₂) → N₂ →ₛₗ[σ₁₂] P₂) x : N₂ →ₛₗ[σ₁₂] P₂) : (a : N₂) → P₂) y : P₂)

Tactic:
(flip f y).map_smul _ _

Premises used: LinearMap.flip, LinearMap.map_smul, DFunLike.coe
-- 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
r : R
x : M
y : N
⊢ (((f : (a : M) → N →ₛₗ[σ₁₂] P) (r • x) : N →ₛₗ[σ₁₂] P) : (a : N) → P) y =
    HSMul.hSMul.{u_2, u_9, u_9} (α := R₂) (β := P) ((ρ₁₂ : (a : R) → R₂) r : R₂)
      ((((f : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
(flip f y).map_smulₛₗ _ _

Premises used: LinearMap.flip, LinearMap.map_smulₛₗ, DFunLike.coe
-- 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₂
ι : Type u_14
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
t : Finset ι
x : ι → M
y : N
⊢ Eq.{u_9 + 1} (α := P) (((f : (a : M) → N →ₛₗ[σ₁₂] P) (∑ i ∈ t, x i) : (a : N) → P) y : P)
    (∑ i ∈ t, (((f : (a : M) → N →ₛₗ[σ₁₂] P) (x i) : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
_root_.map_sum (flip f y) _ _

Premises used: map_sum, LinearMap.flip, DFunLike.coe
-- 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₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
m₁ m₂ : M
x : ↥q
⊢ Eq.{u_9 + 1} (α := P) ((domRestrict ((f : (a : M) → N →ₛₗ[σ₁₂] P) (m₁ + m₂)) q : (a : ↥q) → P) x : P)
    ((HAdd.hAdd (α := LinearMap.{u_3, u_4, u_7, u_9} σ₁₂ (↥q) P) (domRestrict ((f : (a : M) → N →ₛₗ[σ₁₂] P) m₁) q)
            (domRestrict ((f : (a : M) → N →ₛₗ[σ₁₂] P) m₂) q) :
          (a : ↥q) → P)
        x :
      P)

Tactic:
simp only [map_add, domRestrict_apply, add_apply]

Premises used: LinearMap.add_apply, map_add, LinearMap.domRestrict_apply
-- 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₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
c : R
m : M
x : ↥q
⊢ Eq.{u_9 + 1} (α := P) ((domRestrict ((f : (a : M) → N →ₛₗ[σ₁₂] P) (c • m)) q : (a : ↥q) → P) x : P)
    ((HSMul.hSMul (α := R₂) (β := LinearMap.{u_3, u_4, u_7, u_9} σ₁₂ (↥q) P) ((ρ₁₂ : (a : R) → R₂) c : R₂)
            (domRestrict ((f : (a : M) → N →ₛₗ[σ₁₂] P) m) q) :
          (a : ↥q) → P)
        x :
      P)

Tactic:
simp only [f.map_smulₛₗ, domRestrict_apply, smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.map_smulₛₗ, LinearMap.domRestrict_apply
-- 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
q : Submodule S N
x : M
y : ↥q
⊢ Eq.{u_9 + 1} (α := P)
    ((((f.domRestrict₂ q : (a : M) → ↥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 : N →ₛₗ[σ₁₂] P) : (a : N) → P) (↑y : N) : P)

Tactic:
rfl

Premises used: rfl