awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw : Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
  ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
rw :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw₁ : Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
  ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1) : M₂)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
rw :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw₂ : HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
  (((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
rw :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1) : M₂)
rw₂ :
  HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    (((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1)
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw₃ : HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
  HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
rw :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1) : M₂)
rw₂ :
  HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    (((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1)
rw₃ :
  HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
      ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw₄ : HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
    ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
  HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- 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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x_1 : M₁
rw :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x - f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1) : M₂)
rw₂ :
  HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    (((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1 - g' x_1)
rw₃ :
  HSub.hSub (α := M₂) (β := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
      ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
rw₄ :
  HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
      ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) (f' x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂) =
    HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
      ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((f - f') x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((g - g') x_1) : M₂)
have rw₅ : HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂) =
  HSub.hSub (α := M₂) (β := M₂) ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g x_1) : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) (g' x_1) : M₂)
Tactic: rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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) y : M) : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have suffices : 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: suffices 2 * B (f x) (f y) = 2 * B x y from h this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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
⊢ 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)
have this : Eq.{u_20 + 1} (α := R)
  ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) (x + y)) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) (x + y) : M) :
    R)
  ((((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
Tactic: have := hf (x + y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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 :
  Eq.{u_20 + 1} (α := R)
    ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) (x + y)) : M →ₗ[R] R) : (a : M) → R)
        ((f : (a : M) → M) (x + y) : M) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + 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)
have this₁ : HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) x : M) : R) +
    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) y : M →ₗ[R] R) : (a : M) → R) y : R) =
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: simp only [map_add, LinearMap.add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) x : M) : R) +
      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) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : 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)
have this₁ : HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : 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) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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) x : M →ₗ[R] R) : (a : M) → R) x : 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) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : 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)
have this₁ : HAdd.hAdd (α := 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) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) =
  HAdd.hAdd (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : M →ₗ[R] R) : (a : M) → R) y : R))
Tactic: simp only [add_assoc, add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
      ((((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) ((f : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) y : M) : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) =
    HAdd.hAdd (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : 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)
have 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)
Tactic: simp only [← add_assoc, add_left_inj] at this
Cleared hypotheses: this
-- 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
⊢ 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)
have 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₂)
Tactic: ext
-- 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
⊢ 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ₗ : 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]
-- 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)
⊢ (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)
have 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₂)
Tactic: ext