awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PID
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
set :
  let 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');
  A.trace =
    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)
⊢ 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:
set A : Matrix (Fin n) (Fin n) R := toMatrix snf.bN snf.bN (f.restrict hf')

Premises used: Matrix, LinearMap.restrict, Fin, DFunLike.coe, Module.Basis.SmithNormalForm.bN, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.PID
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')
set :
  let 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
⊢ A.trace =
    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:
set B : Matrix ι ι R := toMatrix snf.bM snf.bM f

Premises used: Matrix, Module.Basis.SmithNormalForm.bM, DFunLike.coe, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.PID
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
contrapose : ∀ (hi : i ∉ Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)), 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:
contrapose hi
-- Module: Mathlib.LinearAlgebra.PID
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 : i ∉ Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)
⊢ B i i = 0

Tactic:
snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi

Premises used: Subtype.mk, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range
-- Module: Mathlib.LinearAlgebra.PID
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 : i ∉ Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)
⊢ B i i = 0

Tactic:
exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi

Premises used: Subtype.mk, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range
-- Module: Mathlib.LinearAlgebra.PID
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 : ι),
    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
-- Module: Mathlib.LinearAlgebra.PID
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
change : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, A i i) (∑ i : ι, B i i)
⊢ A.trace = B.trace

Tactic:
change ∑ i, A i i = ∑ i, B i i
-- Module: Mathlib.LinearAlgebra.PID
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
⊢ ∀ (x : Module.Free.ChooseBasisIndex R M),
    Membership.mem (γ := Finset (Module.Free.ChooseBasisIndex R M)) Finset.univ x →
      B x x ≠ 0 →
        (fun (j : Module.Free.ChooseBasisIndex R M) ↦
            Membership.mem (γ := Set (Module.Free.ChooseBasisIndex R M))
              (Set.range (ι := Fin n) (⇑snf.f : (a : Fin n) → Module.Free.ChooseBasisIndex R M)) j)
          x

Tactic:
simpa using aux
-- Module: Mathlib.LinearAlgebra.PID
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
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)
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Fin n, A i i) (∑ i : ι, B i i)

Tactic:
rw [← Finset.sum_filter_of_ne (p := fun j ↦ j ∈ Set.range snf.f) (by simpa using aux)]

Premises used: Finset.sum_filter_of_ne
-- Module: Mathlib.LinearAlgebra.PID
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)
    (∑ 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:
simp [A, B, hf, Finset.sum_image snf.f.injective.injOn]

Premises used: Function.Injective.injOn, Function.Embedding.injective, Module.Basis.SmithNormalForm.f, Finset.sum_image
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
K : Type u_2
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
x : M
y : N
inst_9 : p.IsPerfPair
⊢ p.flip.IsPerfPair

Tactic:
.flip ‹_›

Premises used: LinearMap.IsPerfPair.flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
K : Type u_2
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
x_1 : M
y_1 : N
inst_9 : p.IsPerfPair
x y : M
⊢ AddHom.toFun p.1 (x + y) = HAdd.hAdd (α := Dual R N) (AddHom.toFun p.1 x) (AddHom.toFun p.1 y)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
K : Type u_2
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
x_1 : M
y : N
inst_9 : p.IsPerfPair
r : R
x : M
⊢ AddHom.toFun p.1 (r • x) =
    HSMul.hSMul (α := R) (β := Dual R N) ((RingHom.id R : (a : R) → R) r : R) (AddHom.toFun p.1 x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
x : M
⊢ Eq (α := Dual R N) ((p.toPerfPair : (a : M) → Dual R N) x : Dual R N) ((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
x : M
y : N
⊢ Eq.{u_1 + 1} (α := R) ((((p.toPerfPair : (a : M) → Dual R N) x : Dual R N) : (a : N) → R) y : R)
    ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
f : Dual R N
⊢ (p : (a : M) → N →ₗ[R] R) ((p.toPerfPair.symm : (a : Dual R N) → M) f) = f

Tactic:
p.toPerfPair.apply_symm_apply f

Premises used: LinearMap.toPerfPair, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
f : Dual R M
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((p.flip.toPerfPair.symm : (a : Dual R M) → N) f : N) :
      R)
    ((f : (a : M) → R) x : R)

Tactic:
congr($(p.flip.apply_symm_toPerfPair_self ..) x)

Premises used: LinearMap.apply_symm_toPerfPair_self, congrArg, id, LinearMap.flip, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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))
    (⇑(p.toPerfPair ≪≫ₗ p.flip.toPerfPair.dualMap.symm) : (a : M) → Dual R (Dual R M))

Tactic:
(p.toPerfPair.trans p.flip.toPerfPair.dualMap.symm).bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, LinearMap.toPerfPair, LinearMap.flip, LinearEquiv.dualMap, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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))
⊢ Bijective (α := M) (β := Dual R (Dual R M)) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M))

Tactic:
convert! (p.toPerfPair.trans p.flip.toPerfPair.dualMap.symm).bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, LinearMap.toPerfPair, LinearMap.flip, LinearEquiv.dualMap, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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)
⊢ 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:
ext x f
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_6 : Module.Finite R M
inst_7 : Free R M
⊢ finrank R M = finrank R N

Tactic:
((Module.Free.chooseBasis R M).toDualEquiv.trans p.flip.toPerfPair.symm).finrank_eq

Premises used: LinearEquiv.symm, LinearEquiv.finrank_eq, LinearMap.toPerfPair, LinearMap.flip, LinearEquiv.trans, Module.Free.chooseBasis, Module.Basis.toDualEquiv
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
K : Type u_2
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
x : M
y : N
inst_9 : p.IsPerfPair
inst_10 : IsReflexive R M
⊢ IsPerfPair (R := R) (M := M) (N := Dual R M) (Dual.eval R M)

Tactic:
.flip .id

Premises used: LinearMap.IsPerfPair.id, LinearMap.IsPerfPair.flip, Module.Dual.eval
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
K : Type u_2
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
x : M
y : N
inst_9 : p.IsPerfPair
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
⊢ (p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)).IsPerfPair

Tactic:
⟨((LinearEquiv.congrLeft R R eN).symm.bijective.comp
    (IsPerfPair.bijective_left p)).comp eM.bijective,
    ((LinearEquiv.congrLeft R R eM).symm.bijective.comp
    (IsPerfPair.bijective_right p)).comp eN.bijective⟩

Premises used: LinearMap.IsPerfPair.bijective_left, LinearMap.IsPerfPair.mk, LinearEquiv.symm, LinearEquiv.bijective, LinearMap.IsPerfPair.bijective_right, LinearEquiv.congrLeft, Function.Bijective.comp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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)
⊢ q = p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)

Tactic:
subst H
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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)
⊢ q = (q.compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N')).compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
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
⊢ q.IsPerfPair

Tactic:
obtain rfl : q = p.compl₁₂ eM eN := by subst H; ext; simp

Premises used: LinearMap.compl₁₂, rfl