-- Mathlib/LinearAlgebra/SesquilinearForm.lean
lemma isOrthogonal_of_forall_apply_same {F : Type*} [FunLike F M M] [LinearMapClass F R M M]
    (f : F) (h : IsLeftRegular (2 : R)) (hB : B.IsSymm) (hf : ∀ x, B (f x) (f x) = B x x) :
    B.IsOrthogonal f

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
simp only [← add_assoc, add_left_inj] at this

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f x)) (f y) + (B (f x)) (f y) = (B x) y + (B x) y
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
have := hf (x + y)

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f (x + y))) (f (x + y)) = (B (x + y)) (x + y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f (x + y))) (f (x + y)) = (B (x + y)) (x + y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

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

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f y)) (f x) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
simp only [add_assoc, add_right_inj] at this

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f y)) (f x) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
⊢ IsOrthogonal B ⇑f

Tactic:
intro x y

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
⊢ (B (f x)) (f y) = (B x) y

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f x)) (f y) + (B (f x)) (f y) = (B x) y + (B x) y
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
simpa only [← two_mul] using this

Result:
no goals

Proof state:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
⊢ (B (f x)) (f y) = (B x) y

Tactic:
suffices 2 * B (f x) (f y) = 2 * B x y from h this

Result:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y