awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
inr :
  HSMul.hSMul (α := Rˣ) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
inr₁ :
  HSMul.hSMul (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
have inr₂ : LT.lt.{u_1} (α := R) (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) 0 ↔
  LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
Tactic: rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
inr :
  HSMul.hSMul (α := Rˣ) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
inr₁ :
  HSMul.hSMul (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
inr₂ :
  LT.lt.{u_1} (α := R) (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) 0 ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
have inr₃ : LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R) ↔
  LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
Tactic: rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have obtain : ∀ (n : ℕ) (snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n),
  Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: obtain ⟨n, snf⟩ := p.smithNormalForm (Module.Free.chooseBasis R M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
⊢ Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have rw : Eq.{u_1 + 1} (α := R)
  (Matrix.trace (n := Fin n) ((toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')))
  (Matrix.trace.{u_2, u_1} (n := Module.Free.ChooseBasisIndex R M)
    ((toMatrix snf.bM snf.bM :
        (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
      f))
Tactic: rw [trace_eq_matrix_trace R snf.bM, trace_eq_matrix_trace R snf.bN]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')
B : Matrix ι ι R :=
  (toMatrix snf.bM snf.bM :
      (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
    f
i : ι
hi : B i i ≠ 0
⊢ Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
    (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) i
have contrapose : ∀ (hi : i ∉ Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)), B i i = 0
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')
B : Matrix ι ι R :=
  (toMatrix snf.bM snf.bM :
      (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
    f
⊢ A.trace = B.trace
have aux : ∀ (i : ι),
  B i i ≠ 0 →
    Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
      (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) i
Tactic: have aux : ∀ i, B i i ≠ 0 → i ∈ Set.range snf.f := fun i hi ↦ by
    contrapose hi; exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')
B : Matrix ι ι R :=
  (toMatrix snf.bM snf.bM :
      (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
    f
aux :
  ∀ (i : ι),
    B i i ≠ 0 →
      Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
        (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) i
⊢ A.trace = B.trace
have change : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, A i i) (∑ i : ι, B i i)
Tactic: change ∑ i, A i i = ∑ i, B i i
-- Lean 4 proof step from Mathlib.LinearAlgebra.PID (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')
B : Matrix ι ι R :=
  (toMatrix snf.bM snf.bM :
      (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
    f
aux :
  ∀ (i : ι),
    B i i ≠ 0 →
      Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
        (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) i
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Fin n, A i i) (∑ i : ι, B i i)
have rw : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, A i i)
  (∑ x : Module.Free.ChooseBasisIndex R M with
    Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
      (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) x,
    B x x)
Tactic: rw [← Finset.sum_filter_of_ne (p := fun j ↦ j ∈ Set.range snf.f) (by simpa using aux)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
⊢ Bijective (α := M) (β := Dual R (Dual R M)) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M))
have h : Eq (α := M → Dual R (Dual R M)) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M))
  (⇑(p.toPerfPair ≪≫ₗ p.flip.toPerfPair.dualMap.symm) : (a : M) → Dual R (Dual R M))
Tactic: convert! (p.toPerfPair.trans p.flip.toPerfPair.dualMap.symm).bijective
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
⊢ Eq (α := M → Dual R (Dual R M)) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M))
    (⇑(p.toPerfPair ≪≫ₗ p.flip.toPerfPair.dualMap.symm) : (a : M) → Dual R (Dual R M))
have h : ∀ (x : M) (f : Dual R M),
  Eq.{u_1 + 1} (α := R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) x : Dual R (Dual R M)) : (a : Dual R M) → R) f : R)
    ((((p.toPerfPair ≪≫ₗ p.flip.toPerfPair.dualMap.symm : (a : M) → Dual R (Dual R M)) x : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        f :
      R)
Tactic: ext x f
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : AddCommGroup M'
inst_3 : AddCommGroup N'
inst_4 : CommRing R
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R N'
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
H : q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N') = p
⊢ q = p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)
have subst : ∀ [(q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).IsPerfPair],
  q = (q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)
Tactic: subst H
Cleared hypotheses: p, inst_9, H
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : AddCommGroup M'
inst_3 : AddCommGroup N'
inst_4 : CommRing R
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R N'
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
inst_9 : (q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).IsPerfPair
⊢ q = (q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)
have h : ∀ (x : M') (x_1 : N'),
  Eq.{u_1 + 1} (α := R) ((((q : (a : M') → N' →ₗ[R] R) x : N' →ₗ[R] R) : (a : N') → R) x_1 : R)
    (((((q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N) :
                (a : M') → N' →ₗ[R] R)
              x :
            N' →ₗ[R] R) :
          (a : N') → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : AddCommGroup M'
inst_3 : AddCommGroup N'
inst_4 : CommRing R
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R N'
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
H : q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N') = p
⊢ q.IsPerfPair
have obtain : ∀ (H : (p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)).compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N') = p),
  (p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)).IsPerfPair
Tactic: obtain rfl : q = p.compl₁₂ eM eN := by subst H; ext; simp
Cleared hypotheses: q, H
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (hypothesis)
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K M
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
⊢ Surjective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
have this : FiniteDimensional K N
Tactic: have : FiniteDimensional K N := FiniteDimensional.of_injective p.flip h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Basic (goal)
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K M
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
this : FiniteDimensional K N
⊢ Surjective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
have rwa : Injective (α := M) (β := N →ₗ[K] K) (⇑p.flip.flip : (a : M) → N →ₗ[K] K)
Tactic: rwa [← p.flip.flip_injective_iff₁, LinearMap.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
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
V : Submodule R N
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤
have refine_1 : ∀ (h : p.IsPerfectCompl ⊤ V), V = ⊤
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
V : Submodule R N
refine_1 : ∀ (h : p.IsPerfectCompl ⊤ V), V = ⊤
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤
have refine_2 : ∀ (h : V = ⊤), p.IsPerfectCompl ⊤ V
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V
have refine_2 : p.IsPerfectCompl ⊤ ⊤
Tactic: rw [h]
-- 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
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
U : Submodule R M
⊢ p.IsPerfectCompl U ⊤ ↔ U = ⊤
have rw : p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤
Tactic: rw [← IsPerfectCompl.flip_iff]
-- 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
⊢ (↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) = Dual.eval R N
have h : ∀ (x : N) (x_1 : Dual R N),
  Eq.{u_1 + 1} (α := R)
    (((((↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N)) x :
            Dual R (Dual R N)) :
          (a : Dual R N) → R)
        x_1 :
      R)
    ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) x : Dual R (Dual R N)) : (a : Dual R N) → R) x_1 : R)
Tactic: ext
-- 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
⊢ IsReflexive R N
have bijective_dual_eval' : Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))
Tactic: constructor
-- 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
⊢ Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))
have bijective_dual_eval' : Bijective (α := N) (β := Dual R (Dual R N))
  (⇑(↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N))
Tactic: rw [← trans_dualMap_symm_flip e]
-- 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
h : IsReflexive R N
⊢ e.flip.flip = e
have h₁ : ∀ (x : N) (x_1 : M),
  Eq.{u_1 + 1} (α := R) ((((e.flip.flip : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)
    ((((e : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)
Tactic: ext
-- 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
e : N ≃ₗ[R] Dual R M
p : Submodule R M
⊢ (map (↑e : N →ₗ[R] Dual R M).flip p).dualCoannihilator = map (↑e.symm : Dual R M →ₗ[R] N) p.dualAnnihilator
have h : ∀ (x : N),
  x ∈ (map (↑e : N →ₗ[R] Dual R M).flip p).dualCoannihilator ↔ x ∈ map (↑e.symm : Dual R M →ₗ[R] N) p.dualAnnihilator
Tactic: ext
-- 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 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 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 [← dualCoannihilator_map_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 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 [← dualCoannihilator_map_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 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 [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]
-- 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 M)
⊢ map (↑e : N →ₗ[R] Dual R M).flip p.dualCoannihilator = (map (↑e.symm : Dual R M →ₗ[R] N) p).dualAnnihilator
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 M)
this : IsReflexive R N
⊢ map (↑e : N →ₗ[R] Dual R M).flip p.dualCoannihilator = (map (↑e.symm : Dual R M →ₗ[R] N) p).dualAnnihilator
have Dual : map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.symm : Dual R M →ₗ[R] N) p).dualAnnihilator =
  map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.flip : M →ₗ[R] Dual R N) p.dualCoannihilator)
Tactic: suffices
      (p.map (e.symm : Dual R M →ₗ[R] N)).dualAnnihilator.map (e.flip.symm : Dual R N →ₗ[R] M) =
        (p.dualCoannihilator.map (e.flip : M →ₗ[R] Dual R N)).map (e.flip.symm : Dual R N →ₗ[R] M)
    from (Submodule.map_injective_of_injective e.flip.symm.injective this).symm
-- 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 M)
this : IsReflexive R N
⊢ map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.symm : Dual R M →ₗ[R] N) p).dualAnnihilator =
    map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.flip : M →ₗ[R] Dual R N) p.dualCoannihilator)
have rw : (map ((↑e : N →ₗ[R] Dual R M) ∘ₗ (↑e.symm : Dual R M →ₗ[R] N)) p).dualCoannihilator =
  map ((↑e.flip.symm : Dual R N →ₗ[R] M) ∘ₗ (↑e.flip : M →ₗ[R] Dual R N)) p.dualCoannihilator
Tactic: rw [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip, ← map_comp, ← map_comp]