awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (hypothesis)
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
⊢ (map (↑e.flip.symm : Dual R N →ₗ[R] M) p).dualAnnihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
have this : IsReflexive R N
Tactic: have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
⊢ (map (↑e.flip.symm : Dual R N →ₗ[R] M) p).dualAnnihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
have rw : map (↑e.flip : M →ₗ[R] Dual R N).flip p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
Tactic: rw [← map_dualCoannihilator_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
rw : map (↑e.flip : M →ₗ[R] Dual R N).flip p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
⊢ (map (↑e.flip.symm : Dual R N →ₗ[R] M) p).dualAnnihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
have rw₁ : map (↑e.flip.flip : N →ₗ[R] Dual R M) p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
Tactic: rw [← map_dualCoannihilator_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
rw : map (↑e.flip : M →ₗ[R] Dual R N).flip p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
rw₁ : map (↑e.flip.flip : N →ₗ[R] Dual R M) p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
⊢ (map (↑e.flip.symm : Dual R N →ₗ[R] M) p).dualAnnihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
have rw₂ : map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
Tactic: rw [← map_dualCoannihilator_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
⊢ Bijective (α := M') (β := N' →ₗ[R] R) (⇑(p.compl₁₂ i j) : (a : M') → N' →ₗ[R] R)
have refine_1 : ∀ (m : M') (hm : m ∈ (p.compl₁₂ i j).ker), Membership.mem (γ := Submodule R M') ⊥ m
Tactic: refine ⟨LinearMap.ker_eq_bot.mp <| eq_bot_iff.mpr fun m hm ↦ ?_, fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
refine_1 : ∀ (m : M') (hm : m ∈ (p.compl₁₂ i j).ker), Membership.mem (γ := Submodule R M') ⊥ m
⊢ Bijective (α := M') (β := N' →ₗ[R] R) (⇑(p.compl₁₂ i j) : (a : M') → N' →ₗ[R] R)
have refine_2 : ∀ (f : N' →ₗ[R] R), ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
Tactic: refine ⟨LinearMap.ker_eq_bot.mp <| eq_bot_iff.mpr fun m hm ↦ ?_, fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
⊢ Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)
have simp : ∃ (y : Dual R N),
  (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y : (a : N) → R) w : R) (0 : R)) ∧
    Eq.{u_2 + 1} (α := M) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y : M)
      ((i : (a : M') → M) m : M)
Tactic: simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
⊢ ∃ (y : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y : (a : N) → R) w : R) (0 : R)) ∧
      Eq.{u_2 + 1} (α := M) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y : M)
        ((i : (a : M') → M) m : M)
have refine : ∀ w ∈ j.range,
  Eq.{u_1 + 1} (α := R) ((((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m) : Dual R N) : (a : N) → R) w : R)
    (0 : R)
Tactic: refine ⟨p.toPerfPair (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
⊢ Membership.mem (γ := Submodule R M') ⊥ m
have hm₁ : Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
  ((i : (a : M') → M) m : M)
Tactic: replace hm : i m ∈ j.range.dualAnnihilator.map (p.toPerfPair.symm : Dual R N →ₗ[R] M) := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]
      refine ⟨p.toPerfPair (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
      rintro - ⟨n, rfl⟩
      simpa using LinearMap.congr_fun hm n
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
m : M'
hm :
  Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)
⊢ Membership.mem (γ := Submodule R M') ⊥ m
have refine_1 : Membership.mem.{u_2, u_2} (α := M) (γ := Submodule R M) ⊥ ((i : (a : M') → M) m : M)
Tactic: suffices i m ∈ (⊥ : Submodule R M) by simpa [hi] using this
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
have hF : let F :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj sorry;
F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj sorry
Tactic: set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
have 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)
Tactic: have hF (n : N') : F (j n) = f n := by simp [hF]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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)
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
have hm : let m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F;
m = (p.toPerfPair.symm : (a : Dual R N) → M) F
Tactic: set m : M := p.toPerfPair.symm F with hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
have refine_2 : ∀ (y : M) (m₀ : M') (hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
  (hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m),
  ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
Tactic: obtain ⟨-, y, ⟨m₀, rfl⟩, hy, hm'⟩ :=
      Submodule.codisjoint_iff_exists_add_eq.mp hij.isCompl_left.codisjoint m
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
have refine_2 : ∀ (n : N'),
  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: refine ⟨m₀, LinearMap.ext fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
⊢ 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)
have hy₁ : ∃ (y_1 : Dual R N),
  (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y_1 : (a : N) → R) w : R) (0 : R)) ∧
    ((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y_1 = y
Tactic: simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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 :
  ∃ (y_1 : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y_1 : (a : N) → R) w : R) (0 : R)) ∧
      ((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y_1 = y
⊢ 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)
have obtain : ∀ (g : Dual R N) (hg : ∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((g : (a : N) → R) w : R) (0 : R))
  (hm' :
    HAdd.hAdd (α := M) (β := M) ((i : (a : M') → M) m₀ : M)
        (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g : M) =
      m),
  Eq.{u_1 + 1} (α := R)
    ((((p : (a : M) → N →ₗ[R] R) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g) : N →ₗ[R] R) :
          (a : N) → R)
        ((j : (a : N') → N) n : N) :
      R)
    (0 : R)
Tactic: obtain ⟨g, hg, rfl⟩ := hy
Cleared hypotheses: y, hm', hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
⊢ 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)
have 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)
Tactic: replace hy : (p y) (j n) = 0 := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy
      obtain ⟨g, hg, rfl⟩ := hy
      simpa using hg _ (LinearMap.mem_range_self j n)
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm] at hm'
Cleared hypotheses: hm', n, hy