awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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.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₁)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
⊢ 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₁)
have he : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ 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₁)
have 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₁)
Tactic: simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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₁)
⊢ 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₁)
have 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)
Tactic: simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ 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₁)
have 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)
Tactic: simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ 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₁)
have 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)
Tactic: simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.IsSkewAdjoint (⇑f : (a : M) → M)
have rw : f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B (⇑f : (a : M) → M) (⇑f : (a : M) → M)
Tactic: rw [isSkewAdjoint_iff_neg_self_adjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ x = 0
have rw : Eq.{u_9 + 1} (α := Mₗ₁) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x : Mₗ₁) (0 : Mₗ₁)
Tactic: rw [← e₁.symm.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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ₗ₁)
have 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)
Tactic: refine h (e₁.symm x) fun y ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
    ((((B : (a : Mₗ₁) → Mₗ₂ →ₗ[R] M) ((e₁.symm : (a : Mₗ₁') → Mₗ₁) x) : Mₗ₂ →ₗ[R] M) : (a : Mₗ₂) → M) y : M) (0 : M)
have 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)
Tactic: specialize hx (e₂ y)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ B.SeparatingLeft
have 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)
Tactic: convert! h.congr e₁.symm e₂.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.SeparatingLeft ↔ B.SeparatingRight
have rw : B.flip.flip.SeparatingRight ↔ B.SeparatingRight
Tactic: rw [← flip_separatingRight, flip_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.flip.SeparatingLeft ↔ B.SeparatingRight
have rw₁ : B.SeparatingRight ↔ B.SeparatingRight
Tactic: rw [← flip_separatingRight, flip_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 ↔
    ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.SeparatingLeft ↔
    ∀ (x : M₁), Eq (α := M₂ →ₛₗ[I₂] M) ((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) (0 : M₂ →ₛₗ[I₂] M) → x = 0
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : (a : M₂) → M) x_1 : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x_1 : M) (0 : M)
Tactic: rw [zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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 = 0
have h' : 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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.SeparatingRight ↔
    ∀ (y : M₂), Eq (α := M₁ →ₛₗ[I₁] M) ((B.flip : (a : M₂) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) (0 : M₁ →ₛₗ[I₁] M) → y = 0
have 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
Tactic: rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]