awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
hy :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
    (0 : R)
refine_2 :
  ∀
    (hm' :
      HAdd.hAdd (α := Dual R N) (β := Dual R N) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m₀) : Dual R N)
          ((p.toPerfPair : (a : M) → Dual R N) y : Dual R N) =
        F)
    (n : N')
    (hy :
      Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
        (0 : R)),
    Eq.{u_1 + 1} (α := R) ((((p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) m₀ : N' →ₗ[R] R) : (a : N') → R) n : R)
      ((f : (a : N') → R) n : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) m₀ : N' →ₗ[R] R) : (a : N') → R) n : R)
    ((f : (a : N') → R) n : R)

Tactic:
rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm] at hm'

Premises used: LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hm' :
  HAdd.hAdd (α := Dual R N) (β := Dual R N) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m₀) : Dual R N)
      ((p.toPerfPair : (a : M) → Dual R N) y : Dual R N) =
    F
n : N'
hy :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) m₀ : N' →ₗ[R] R) : (a : N') → R) n : R)
    ((f : (a : N') → R) n : R)

Tactic:
simpa [← hF, ← LinearMap.congr_fun hm' (j n)]

Premises used: LinearMap.congr_fun, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
rw : (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).ker = ⊥
⊢ Injective (α := M') (β := N' →ₗ[S] S)
    (⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) : (a : M') → N' →ₗ[S] S)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).ker = ⊥

Tactic:
(Submodule.eq_bot_iff _).mpr fun x (hx : f x = 0) ↦ ?_

Premises used: Iff.mpr, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
refine : ∀ (x : M') (hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)), x = 0
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).ker = ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun x (hx : f x = 0) ↦ ?_

Premises used: Iff.mpr, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
⊢ Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n

Tactic:
have hn : n ∈ span R (LinearMap.range j : Set N) := hN ▸ Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n z : N
hz : z ∈ (↑j.range : Set N)
mem :
  ∀ (n' : N'),
    Eq.{u_1 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n' : N) : R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)

Tactic:
obtain ⟨n', rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
n' : N'
⊢ Eq.{u_1 + 1} (α := R)
    ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n' : N) : R)
    (0 : R)

Tactic:
simpa [f] using LinearMap.congr_fun hx n'

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n x_1 y : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
hy : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
h_1 :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) (0 : R)
add :
  HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (x_1 + y) : R)
    (0 : R)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n x_1 y : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
hy : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
h_1 :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) =
    0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
a : R
x_1 : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
smul :
  HSMul.hSMul (β := R) a ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) = 0
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (a • x_1) : R)
    (0 : R)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
a : R
x_1 : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
⊢ HSMul.hSMul (β := R) a ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) = 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
mem :
  ∀ (z : N) (hz : z ∈ (↑j.range : Set N)),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
zero :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) 0 : R) (0 : R)
add :
  ∀ (x_1 y : N),
    Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1 →
      Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y →
        Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
            (0 : R) →
          Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
              (0 : R) →
            Eq.{u_1 + 1} (α := R)
              ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (x_1 + y) : R) (0 : R)
smul :
  ∀ (a : R) (x_1 : N),
    Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1 →
      Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
          (0 : R) →
        Eq.{u_1 + 1} (α := R)
          ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (a • x_1) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)

Tactic:
induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop

Premises used: map_add, rfl, map_smul