awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
x : M
y : M₁
⊢ Eq.{u_8 + 1} (α := M₃)
    ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)

Tactic:
exact h x y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x : M
mpr :
  ∀ (y : M₁),
    Eq.{u_8 + 1} (α := M₃)
      ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)
⊢ ∀ (y : M₁),
    Eq.{u_8 + 1} (α := M₃)
      ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x : M
y : M₁
mpr :
  Eq.{u_8 + 1} (α := M₃)
    ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
mpr₁ :
  Eq.{u_8 + 1} (α := M₃) ((((B' ∘ₗ f : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
mpr₂ mpr₃ :
  Eq.{u_8 + 1} (α := M₃) ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
⊢ Eq.{u_8 + 1} (α := M₃)
    ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)

Tactic:
rw [← compl₂_apply, ← comp_apply, h]

Premises used: LinearMap.compl₂_apply, LinearMap.comp_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
x : M
x_1 : M₁
⊢ Eq.{u_8 + 1} (α := M₃) (((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (0 x) : (a : M₁) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (0 x_1) : M₃)

Tactic:
simp only [Pi.zero_apply, map_zero, zero_apply]

Premises used: LinearMap.zero_apply, Pi.zero_apply, map_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
⊢ B.IsAdjointPair B _root_.id _root_.id

Tactic:
fun _ _ ↦ rfl

Premises used: LinearMap.IsAdjointPair, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
⊢ B.IsAdjointPair B (⇑1 : (a : M) → M) (⇑1 : (a : M) → M)

Tactic:
isAdjointPair_id

Premises used: LinearMap.isAdjointPair_id
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] 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_8 + 1} (α := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f x + f' x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g + g') x_1) : M₃)
rw₁ :
  Eq.{u_8 + 1} (α := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f x + f' x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1 + g' x_1) : M₃)
rw₂ :
  HAdd.hAdd (α := M₃) (β := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃)
      ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f' x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃) =
    (((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1 + g' x_1)
rw₃ :
  HAdd.hAdd (α := M₃) (β := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃)
      ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f' x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃) =
    HAdd.hAdd (α := M₃) (β := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1) : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g' x_1) : M₃)
rw₄ :
  HAdd.hAdd (α := M₃) (β := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1) : M₃)
      ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f' x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃) =
    HAdd.hAdd (α := M₃) (β := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1) : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g' x_1) : M₃)
rw₅ rw₆ :
  HAdd.hAdd (α := M₃) (β := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1) : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g' x_1) : M₃) =
    HAdd.hAdd (α := M₃) (β := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g x_1) : M₃)
      ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g' x_1) : M₃)
⊢ Eq.{u_8 + 1} (α := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f + f') x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g + g') x_1) : M₃)

Tactic:
rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, h, h']

Premises used: LinearMap.map_add, Pi.add_apply, LinearMap.map_add₂, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : AddCommMonoid M₃
inst_8 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x : M
x_1 : M₂
rw :
  Eq.{u_8 + 1} (α := M₃) (((B'' : (a : M₂) → M₂ →ₛₗ[I] M₃) ((fun (x : M) ↦ f' (f x)) x) : (a : M₂) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g ∘ g') x_1) : M₃)
rw₁ :
  Eq.{u_8 + 1} (α := M₃) (((B'' : (a : M₂) → M₂ →ₛₗ[I] M₃) ((fun (x : M) ↦ f' (f x)) x) : (a : M₂) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((fun (x : M₂) ↦ g (g' x)) x_1) : M₃)
rw₂ :
  Eq.{u_8 + 1} (α := M₃) ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) (f x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) (g' x_1) : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((fun (x : M₂) ↦ g (g' x)) x_1) : M₃)
rw₃ rw₄ :
  Eq.{u_8 + 1} (α := M₃) ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) (g (g' x_1)) : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((fun (x : M₂) ↦ g (g' x)) x_1) : M₃)
⊢ Eq.{u_8 + 1} (α := M₃) ((((B'' : (a : M₂) → M₂ →ₛₗ[I] M₃) ((f' ∘ f) x) : M₂ →ₛₗ[I] M₃) : (a : M₂) → M₃) x_1 : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g ∘ g') x_1) : M₃)

Tactic:
rw [Function.comp_def, Function.comp_def, h', h]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
f g f' g' : End R M
h : B.IsAdjointPair B (⇑f : (a : M) → M) (⇑g : (a : M) → M)
h' : B.IsAdjointPair B (⇑f' : (a : M) → M) (⇑g' : (a : M) → M)
⊢ B.IsAdjointPair B (⇑(f * f') : (a : M) → M) (⇑(g' * g) : (a : M) → M)

Tactic:
h'.comp h

Premises used: LinearMap.IsAdjointPair.comp
-- 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 : 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₂)
rw₅ 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₂)
⊢ 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₂)

Tactic:
rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']

Premises used: LinearMap.map_sub₂, LinearMap.map_sub, DFunLike.coe, Pi.sub_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 : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f : M → M₁
g : M₁ → M
c : R
h : B.IsAdjointPair B' f g
x : M
x_1 : M₁
⊢ Eq.{u_7 + 1} (α := M₂) ((((B' : (a : M₁) → M₁ →ₗ[R] M₂) ((c • f) x) : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x_1 : M₂)
    ((((B : (a : M) → M →ₗ[R] M₂) x : M →ₗ[R] M₂) : (a : M) → M₂) ((c • g) x_1) : M₂)

Tactic:
simp [h _]
-- 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 : M ≃ M
hf : IsAdjointPair B B (⇑f : (a : M) → M) (⇑f.symm : (a : M) → M)
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)

Tactic:
simpa using hf x (f y)

Premises used: DFunLike.coe
-- 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 : M ≃ M
hf : IsOrthogonal B (⇑f : (a : M) → M)
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) y : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) ((f.symm : (a : M) → M) y : M) : R)

Tactic:
simpa using hf x (f.symm y)

Premises used: Equiv.symm, DFunLike.coe
-- 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
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)
⊢ 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)

Tactic:
suffices 2 * B (f x) (f y) = 2 * B x y from h this
-- 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
⊢ 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)
-- 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 :
  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)
⊢ 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

Premises used: LinearMap.add_apply, map_add, LinearMap.IsSymm.eq
-- 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) 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)
⊢ 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

Premises used: LinearMap.IsSymm.eq, DFunLike.coe
-- 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) 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)
⊢ 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

Premises used: add_assoc, add_right_inj
-- 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)
      ((((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))
⊢ 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

Premises used: add_assoc, add_left_inj