awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h :
  (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) →
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
⊢ (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) ↔
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
have h₁ : Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂) →
  ∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
z : K
⊢ B.IsOrtho (z • x) y
have h₁ : Eq (α := K) ((RingHom.id K : (a : K) → K) z : K) (0 : K) ∨
  Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
Tactic: rw [isOrtho_def, map_smulₛₗ₂, smul_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
V : Type u_16
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ K ∙ x ⊔ Submodule.orthogonalBilin B (K ∙ x) = ⊤
have rw : Eq (α := Submodule K V) (K ∙ x ⊔ ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K) ((B : (a : V) → V →ₗ[K] K) x)) ⊤
Tactic: rw [orthogonal_span_singleton_eq_to_lin_ker]
-- 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_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
⊢ B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) ↔ B' ∘ₗ f = B.compl₂ g
have mp : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) → B' ∘ₗ f = B.compl₂ g
Tactic: constructor
-- 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_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
mp : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) → B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) ↔ B' ∘ₗ f = B.compl₂ g
have mpr : B' ∘ₗ f = B.compl₂ g → B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
Tactic: constructor
-- 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_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)
⊢ B' ∘ₗ f = B.compl₂ g
have mp : ∀ (x : M) (y : M₁),
  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₃)
Tactic: ext x y
-- 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_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' ∘ₗ 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₃)
have mp : 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 [comp_apply, compl₂_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_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₁
⊢ 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₃)
have 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₃)
Tactic: rw [← compl₂_apply, ← comp_apply, 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_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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [← compl₂_apply, ← comp_apply, 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_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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [← compl₂_apply, ← comp_apply, 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_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₁
⊢ 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₃)
have 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₃)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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_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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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_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₃)
⊢ 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₃)
have 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)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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_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)
⊢ 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₃)
have 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₃)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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_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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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_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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, 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
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₂
⊢ 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₃)
have 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₃)
Tactic: rw [Function.comp_def, Function.comp_def, 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
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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Function.comp_def, Function.comp_def, 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
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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Function.comp_def, Function.comp_def, 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
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₃)
⊢ 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₃)
have 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₃)
Tactic: rw [Function.comp_def, Function.comp_def, h', h]