awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.Nondegenerate
⊢ Nondegenerate.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)

Tactic:
⟨h.1.congr e₁ e₂, h.2.congr e₁ e₂⟩

Premises used: LinearMap.SeparatingRight.congr, And.right, And.left, And.intro, LinearMap.Nondegenerate, LinearMap.SeparatingLeft.congr
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h :
  SeparatingLeft.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)
⊢ SeparatingLeft.{u_1, u_1, u_1, u_5, u_9, u_11} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁) (M₂ := Mₗ₂) (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.symm.arrowCongr (e₂.symm.arrowCongr (LinearEquiv.refl R M)) :
        (a : Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) → Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M)
      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M)
        B))

Tactic:
h.congr e₁.symm e₂.symm

Premises used: LinearEquiv.symm, LinearMap.SeparatingLeft.congr
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h :
  SeparatingLeft.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)
h₁ :
  B =
    (e₁.symm.arrowCongr (e₂.symm.arrowCongr (LinearEquiv.refl R M)) :
        (a : Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) → Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M)
      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)
⊢ B.SeparatingLeft

Tactic:
convert! h.congr e₁.symm e₂.symm

Premises used: LinearEquiv.symm, LinearMap.SeparatingLeft.congr
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h :
  SeparatingLeft.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)
h₁ :
  ∀ (x : Mₗ₁) (y : Mₗ₂),
    Eq.{u_5 + 1} (α := M) ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) x : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M)
      ((((((e₁.symm.arrowCongr (e₂.symm.arrowCongr (LinearEquiv.refl R M)) :
                        (a : Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) → Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M)
                      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) :
                          (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M)
                        B) :
                    Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) :
                  (a : Mₗ₁) → Mₗ₂ →ₗ[R] M)
                x :
              Mₗ₂ →ₗ[R] M) :
            (a : Mₗ₂) → M)
          y :
        M)
⊢ B =
    (e₁.symm.arrowCongr (e₂.symm.arrowCongr (LinearEquiv.refl R M)) :
        (a : Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) → Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M)
      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h :
  SeparatingLeft.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R)
    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) B)
x : Mₗ₁
y : Mₗ₂
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) x : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M)
    ((((((e₁.symm.arrowCongr (e₂.symm.arrowCongr (LinearEquiv.refl R M)) :
                      (a : Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M) → Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M)
                    ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) :
                        (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M)
                      B) :
                  Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) :
                (a : Mₗ₁) → Mₗ₂ →ₗ[R] M)
              x :
            Mₗ₂ →ₗ[R] M) :
          (a : Mₗ₂) → M)
        y :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
⊢ SeparatingRight.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂')
      (I₁ := RingHom.id R) (I₂ := RingHom.id R)
      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M)
        B) ↔
    B.SeparatingRight

Tactic:
separatingLeft_congr_iff (B := B.flip) e₂ e₁

Premises used: LinearMap.SeparatingRight, LinearMap.separatingLeft_congr_iff
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₗ₁
inst_4 : AddCommMonoid Mₗ₂
inst_5 : AddCommMonoid Mₗ₁'
inst_6 : AddCommMonoid Mₗ₂'
inst_7 : Module R Mₗ₁
inst_8 : Module R Mₗ₂
inst_9 : Module R Mₗ₁'
inst_10 : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
⊢ Nondegenerate.{u_1, u_1, u_1, u_5, u_10, u_12} (R := R) (R₁ := R) (R₂ := R) (M := M) (M₁ := Mₗ₁') (M₂ := Mₗ₂') (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R)
      ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) : (a : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M) → Mₗ₁' →ₗ[R] Mₗ₂' →ₗ[R] M)
        B) ↔
    B.Nondegenerate

Tactic:
⟨fun h ↦ ⟨separatingLeft_congr_iff e₁ e₂ |>.mp h.1, separatingRight_congr_iff e₁ e₂ |>.mp h.2⟩,
    .congr e₁ e₂⟩

Premises used: LinearMap.Nondegenerate.congr, LinearMap.separatingRight_congr_iff, LinearMap.separatingLeft_congr_iff, And.right, And.left, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.SeparatingRight ↔ B.SeparatingLeft

Tactic:
⟨fun hB x hy ↦ hB x hy, fun hB x hy ↦ hB x hy⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
rw : B.flip.flip.SeparatingRight ↔ B.SeparatingRight
rw₁ rw₂ : B.SeparatingRight ↔ B.SeparatingRight
⊢ B.flip.SeparatingLeft ↔ B.SeparatingRight

Tactic:
rw [← flip_separatingRight, flip_flip]

Premises used: LinearMap.flip_separatingRight, LinearMap.flip_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.Nondegenerate ↔ B.Nondegenerate

Tactic:
Iff.trans and_comm (and_congr flip_separatingRight flip_separatingLeft)

Premises used: and_comm, LinearMap.flip_separatingRight, Iff.trans, LinearMap.flip_separatingLeft, and_congr
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
mp :
  B.SeparatingLeft →
    ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
mpr :
  (∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0) →
    B.SeparatingLeft
⊢ B.SeparatingLeft ↔
    ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : B.SeparatingLeft
x : M₁
hB : Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M)
⊢ x = 0

Tactic:
simpa only [hB, zero_apply, eq_self_iff_true, forall_const] using h x

Premises used: LinearMap.zero_apply, forall_const, eq_self_iff_true
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
h₁ :
  ∀ (x_1 : M₂),
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M)
      ((0 : (a : M₂) → M) x_1 : M)
⊢ Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
x_1 : M₂
h₁ : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M)
    ((0 : (a : M₂) → M) x_1 : M)

Tactic:
rw [zero_apply]

Premises used: LinearMap.zero_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
x_1 : M₂
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M) (0 : M)

Tactic:
hB _
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
x_1 : M₂
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M) (0 : M)

Tactic:
exact hB _
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
⊢ Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M)

Tactic:
have h' : B x = 0 := by
    ext
    rw [zero_apply]
    exact hB _
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
h' : Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M)
⊢ x = 0

Tactic:
h x h'
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
x : M₁
hB : ∀ (y : M₂), Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)
h' : Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M)
⊢ x = 0

Tactic:
exact h x h'
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
rw :
  B.flip.SeparatingLeft ↔
    ∀ (y : M₂), Eq (α := M₁ →ₛₗ[I₁] M) ((B.flip : (a : M₂) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) (0 : M₁ →ₛₗ[I₁] M) → y = 0
rw₁ rw₂ :
  (∀ (x : M₂),
      Eq (α := M₁ →ₛₗ[I₁] M) ((B.flip : (a : M₂) → M₁ →ₛₗ[I₁] M) x : M₁ →ₛₗ[I₁] M) (0 : M₁ →ₛₗ[I₁] M) → x = 0) ↔
    ∀ (y : M₂), Eq (α := M₁ →ₛₗ[I₁] M) ((B.flip : (a : M₂) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) (0 : M₁ →ₛₗ[I₁] M) → y = 0
⊢ B.SeparatingRight ↔
    ∀ (y : M₂), Eq (α := M₁ →ₛₗ[I₁] M) ((B.flip : (a : M₂) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) (0 : M₁ →ₛₗ[I₁] M) → y = 0

Tactic:
rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]

Premises used: LinearMap.separatingLeft_iff_linear_nontrivial, LinearMap.flip_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingLeft ↔ B.ker = ⊥

Tactic:
Iff.trans separatingLeft_iff_linear_nontrivial LinearMap.ker_eq_bot'.symm

Premises used: LinearMap.ker_eq_bot', Iff.trans, LinearMap.separatingLeft_iff_linear_nontrivial, Iff.symm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
rw : B.flip.SeparatingLeft ↔ B.flip.ker = ⊥
rw₁ rw₂ : B.flip.ker = ⊥ ↔ B.flip.ker = ⊥
⊢ B.SeparatingRight ↔ B.flip.ker = ⊥

Tactic:
rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]

Premises used: LinearMap.flip_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingLeft

Tactic:
⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩

Premises used: And.left, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
refine : ∀ (hB' : B.SeparatingLeft), B.SeparatingRight
⊢ B.Nondegenerate ↔ B.SeparatingLeft

Tactic:
refine ⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
rw : B.ker = ⊥
⊢ B.SeparatingRight

Tactic:
rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]

Premises used: LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot, LinearMap.separatingRight_iff_flip_ker_eq_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' rwa rwa₁ rwa₂ rwa₃ : B.SeparatingLeft
⊢ B.ker = ⊥

Tactic:
rwa [← separatingLeft_iff_ker_eq_bot]

Premises used: LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingRight

Tactic:
⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩

Premises used: And.right, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
refine : ∀ (hB' : B.SeparatingRight), B.SeparatingLeft
⊢ B.Nondegenerate ↔ B.SeparatingRight

Tactic:
refine ⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
rw : B.flip.ker = ⊥
⊢ B.SeparatingLeft

Tactic:
rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]

Premises used: Iff.mpr, LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' rwa rwa₁ rwa₂ rwa₃ : B.SeparatingRight
⊢ B.flip.ker = ⊥

Tactic:
rwa [← separatingRight_iff_flip_ker_eq_bot]

Premises used: LinearMap.separatingRight_iff_flip_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
⊢ Disjoint W B.ker

Tactic:
Submodule.disjoint_def.mpr fun x hx hx' ↦ ?_

Premises used: Iff.mpr, Submodule.disjoint_def