awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_20
M : Type u_21
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst_3 : FunLike F M M
inst_4 : LinearMapClass F R M M
f : F
h : IsLeftRegular.{u_20} (R := R) 2
hB : IsSymm B
hf :
  ∀ (x : M),
    Eq.{u_20 + 1} (α := R)
      ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) x : M) : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
this :
  HAdd.hAdd (α := R) (β := R)
      ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R)
      ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R) =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
simpa only [← two_mul] using this

Premises used: two_mul
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
f : End R M
⊢ f ∈ B.isPairSelfAdjointSubmodule F ↔ B.IsPairSelfAdjoint F (⇑f : (a : M) → M)

Tactic:
Iff.rfl

Premises used: LinearMap.IsAdjointPair, Set.Mem, Iff.rfl, LinearMap.IsPairSelfAdjoint, setOf
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
h :
  ∀ (x x_1 : M₁),
    Eq.{u_7 + 1} (α := M₂)
      ((((F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f :
                  (a : M₁) → M₁ →ₗ[R] M₂)
                x :
              M₁ →ₗ[R] M₂) :
            (a : M₁) → M₂)
          x_1 :
        M₂)
      (((((F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] M₂) x : M₁ →ₗ[R] M₂) :
            (a : M₁) → M₂)
          x_1 :
        M₂)
⊢ F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
x x_1 : M₁
⊢ Eq.{u_7 + 1} (α := M₂)
    ((((F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f :
                (a : M₁) → M₁ →ₗ[R] M₂)
              x :
            M₁ →ₗ[R] M₂) :
          (a : M₁) → M₂)
        x_1 :
      M₂)
    (((((F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] M₂) x : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
        x_1 :
      M₂)

Tactic:
simp only [LinearEquiv.symm_conj_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply,
      LinearEquiv.apply_symm_apply, Function.comp_apply]

Premises used: LinearEquiv.symm_conj_apply, LinearMap.coe_comp, LinearMap.compl₁₂_apply, LinearEquiv.apply_symm_apply, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
⊢ F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)

Tactic:
have hₗ :
    (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).comp (e.symm.conj f) =
      (F.comp f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) := by
    ext
    simp only [LinearEquiv.symm_conj_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply,
      LinearEquiv.apply_symm_apply, Function.comp_apply]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ :
  F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
h :
  ∀ (x x_1 : M₁),
    Eq.{u_7 + 1} (α := M₂)
      (((((B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
                    ((e.symm.conj : (a : End R M) → End R M₁) f) :
                  (a : M₁) → M₁ →ₗ[R] M₂)
                x :
              M₁ →ₗ[R] M₂) :
            (a : M₁) → M₂)
          x_1 :
        M₂)
      (((((B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] M₂) x : M₁ →ₗ[R] M₂) :
            (a : M₁) → M₂)
          x_1 :
        M₂)
⊢ (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
      ((e.symm.conj : (a : End R M) → End R M₁) f) =
    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ :
  F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
x x_1 : M₁
⊢ Eq.{u_7 + 1} (α := M₂)
    (((((B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
                  ((e.symm.conj : (a : End R M) → End R M₁) f) :
                (a : M₁) → M₁ →ₗ[R] M₂)
              x :
            M₁ →ₗ[R] M₂) :
          (a : M₁) → M₂)
        x_1 :
      M₂)
    (((((B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] M₂) x : M₁ →ₗ[R] M₂) :
          (a : M₁) → M₂)
        x_1 :
      M₂)

Tactic:
simp only [LinearEquiv.symm_conj_apply, compl₂_apply, coe_comp, LinearEquiv.coe_coe,
      compl₁₂_apply, LinearEquiv.apply_symm_apply, Function.comp_apply]

Premises used: LinearMap.compl₂_apply, LinearEquiv.symm_conj_apply, LinearMap.coe_comp, LinearMap.compl₁₂_apply, LinearEquiv.apply_symm_apply, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ :
  F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
⊢ (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
      ((e.symm.conj : (a : End R M) → End R M₁) f) =
    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)

Tactic:
have hᵣ :
    (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (e.symm.conj f) =
      (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) := by
    ext
    simp only [LinearEquiv.symm_conj_apply, compl₂_apply, coe_comp, LinearEquiv.coe_coe,
      compl₁₂_apply, LinearEquiv.apply_symm_apply, Function.comp_apply]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ :
  F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
hᵣ :
  (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
      ((e.symm.conj : (a : End R M) → End R M₁) f) =
    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
⊢ Function.Surjective.{u_6 + 1, u_5 + 1} (α := M₁) (β := M) (⇑(↑e : M₁ →ₗ[R] M) : (a : M₁) → M)

Tactic:
have he : Function.Surjective (⇑(↑e : M₁ →ₗ[R] M) : M₁ → M) := e.surjective
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ :
  F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
hᵣ :
  (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
      ((e.symm.conj : (a : End R M) → End R M₁) f) =
    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
he : Function.Surjective.{u_6 + 1, u_5 + 1} (α := M₁) (β := M) (⇑(↑e : M₁ →ₗ[R] M) : (a : M₁) → M)
simp_rw :
  B.IsAdjointPair F (⇑f : (a : M) → M) (⇑f : (a : M) → M) ↔
    (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).IsAdjointPair (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M))
      (⇑((e.symm.conj : (a : End R M) → End R M₁) f : End R M₁) : (a : M₁) → M₁)
      (⇑((e.symm.conj : (a : End R M) → End R M₁) f : End R M₁) : (a : M₁) → M₁)
simp_rw₁ :
  F ∘ₗ f = B.compl₂ f ↔
    F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) ∘ₗ (e.symm.conj : (a : End R M) → End R M₁) f =
      (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
        ((e.symm.conj : (a : End R M) → End R M₁) f)
simp_rw₂ :
  F ∘ₗ f = B.compl₂ f ↔
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) =
      (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (σ₄₂ := RingHom.id R)
        ((e.symm.conj : (a : End R M) → End R M₁) f)
simp_rw₃ :
  F ∘ₗ f = B.compl₂ f ↔
    (F ∘ₗ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) = (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)
⊢ B.IsPairSelfAdjoint F (⇑f : (a : M) → M) ↔
    (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).IsPairSelfAdjoint (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M))
      (⇑((e.symm.conj : (a : End R M) → End R M₁) f : End R M₁) : (a : M₁) → M₁)

Tactic:
simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]

Premises used: LinearMap.isAdjointPair_iff_comp_eq_compl₂, LinearMap.IsPairSelfAdjoint, LinearMap.compl₁₂_inj
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
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₂
f : M → M
⊢ (∀ (x y : M),
      Eq.{u_7 + 1} (α := M₂) ((((B : (a : M) → M →ₗ[R] M₂) (f x) : M →ₗ[R] M₂) : (a : M) → M₂) y : M₂)
        ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((-f) y) : M₂)) ↔
    ∀ (x y : M),
      Eq.{u_7 + 1} (α := M₂) ((((B : (a : M) → M →ₗ[R] M₂) (f x) : M →ₗ[R] M₂) : (a : M) → M₂) y : M₂)
        ((((-B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (f y) : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
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₂
f : End R M
⊢ f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint (⇑f : (a : M) → M)

Tactic:
Iff.rfl

Premises used: LinearMap.IsAdjointPair, Set.Mem, Iff.rfl, LinearMap.IsPairSelfAdjoint, setOf, LinearMap.IsSelfAdjoint
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
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₂
f : End R M
rw : f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B (⇑f : (a : M) → M) (⇑f : (a : M) → M)
⊢ f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint (⇑f : (a : M) → M)

Tactic:
rw [isSkewAdjoint_iff_neg_self_adjoint]

Premises used: LinearMap.isSkewAdjoint_iff_neg_self_adjoint
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
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₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B (⇑f : (a : M) → M) (⇑f : (a : M) → M)

Tactic:
Iff.rfl

Premises used: LinearMap.IsAdjointPair, Set.Mem, Iff.rfl, LinearMap.IsPairSelfAdjoint, setOf
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
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₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B (⇑f : (a : M) → M) (⇑f : (a : M) → M)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- 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
inst_9 : Nontrivial M₁
⊢ ¬SeparatingLeft.{u_1, u_2, u_3, u_5, u_6, u_7} (R := R) (R₁ := R₁) (R₂ := R₂) (M := M) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      I₁) (I₂ := I₂) 0

Tactic:
let ⟨m, hm⟩ := exists_ne (0 : M₁)
  fun h ↦ hm (h m fun _n ↦ rfl)

Premises used: exists_ne, _private.0.LinearMap.not_separatingLeft_zero.match_1, OfNat.ofNat, Not, rfl, LinearMap.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
inst_9 : Nontrivial M₁
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : B.SeparatingLeft
⊢ B ≠ 0

Tactic:
fun h0 ↦ not_separatingLeft_zero M₁ M₂ I₁ I₂ <| h0 ▸ h

Premises used: LinearMap.not_separatingLeft_zero, Not
-- 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.SeparatingLeft
x : Mₗ₁'
hx :
  ∀ (y : Mₗ₂'),
    Eq.{u_5 + 1} (α := 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)
      (0 : M)
rw : Eq.{u_9 + 1} (α := Mₗ₁) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x : Mₗ₁) (0 : Mₗ₁)
⊢ x = 0

Tactic:
rw [← e₁.symm.map_eq_zero_iff]

Premises used: LinearEquiv.symm, LinearEquiv.map_eq_zero_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ₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
hx :
  ∀ (y : Mₗ₂'),
    Eq.{u_5 + 1} (α := 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)
      (0 : M)
⊢ Eq.{u_9 + 1} (α := Mₗ₁) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x : Mₗ₁) (0 : Mₗ₁)

Tactic:
h (e₁.symm x) fun y ↦ ?_

Premises used: LinearEquiv.symm, DFunLike.coe
-- 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.SeparatingLeft
x : Mₗ₁'
hx :
  ∀ (y : Mₗ₂'),
    Eq.{u_5 + 1} (α := 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)
      (0 : M)
refine :
  ∀ (y : Mₗ₂),
    Eq.{u_5 + 1} (α := M)
      ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)
⊢ Eq.{u_9 + 1} (α := Mₗ₁) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x : Mₗ₁) (0 : Mₗ₁)

Tactic:
refine h (e₁.symm x) fun y ↦ ?_

Premises used: LinearEquiv.symm, DFunLike.coe
-- 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.SeparatingLeft
x : Mₗ₁'
hx :
  ∀ (y : Mₗ₂'),
    Eq.{u_5 + 1} (α := 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)
      (0 : M)
y : Mₗ₂
⊢ Eq.{u_5 + 1} (α := 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)
        ((e₂ : (a : Mₗ₂) → Mₗ₂') y : Mₗ₂') :
      M)
    (0 : M)

Tactic:
specialize hx (e₂ y)

Premises used: DFunLike.coe
-- 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.SeparatingLeft
x : Mₗ₁'
y : Mₗ₂
hx :
  Eq.{u_5 + 1} (α := 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)
        ((e₂ : (a : Mₗ₂) → Mₗ₂') y : Mₗ₂') :
      M)
    (0 : M)
⊢ Eq.{u_5 + 1} (α := M)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)

Tactic:
simp only [LinearEquiv.arrowCongr_apply, LinearEquiv.symm_apply_apply,
    LinearEquiv.map_eq_zero_iff] at hx

Premises used: LinearEquiv.symm_apply_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.map_eq_zero_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ₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
y : Mₗ₂
hx :
  Eq.{u_5 + 1} (α := M)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)

Tactic:
hx
-- 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.SeparatingLeft
x : Mₗ₁'
y : Mₗ₂
hx :
  Eq.{u_5 + 1} (α := M)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)

Tactic:
exact hx
-- 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.SeparatingRight
⊢ 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)

Tactic:
SeparatingLeft.congr (B := B.flip) e₂ e₁ h

Premises used: LinearMap.SeparatingRight, LinearMap.SeparatingLeft.congr