awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B.compRight id : (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)
⊢ B.compRight id = B

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.compRight id : (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:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B.comp id id : (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)
⊢ B.comp id id = B

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.comp id id : (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:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
mp : B₁.comp l r = B₂.comp l r → B₁ = B₂
mpr : B₁ = B₂ → B₁.comp l r = B₂.comp l r
⊢ B₁.comp l r = B₂.comp l r ↔ B₁ = B₂

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
h : B₁.comp l r = B₂.comp l r
mp :
  ∀ (x y : M'),
    Eq.{u_1 + 1} (α := 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)
⊢ B₁ = B₂

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
h : B₁.comp l r = B₂.comp l r
x y : M'
mp :
  ∀ (x' : M),
    Eq.{u_1 + 1} (α := R) ((((B₁ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) y : R)
      ((((B₂ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) y : R)
⊢ Eq.{u_1 + 1} (α := 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:
obtain ⟨x', rfl⟩ := hₗ x

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
h : B₁.comp l r = B₂.comp l r
y : M'
x' : M
mp :
  ∀ (y' : M),
    Eq.{u_1 + 1} (α := R)
      ((((B₁ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R)
          ((r : (a : M) → M') y' : M') :
        R)
      ((((B₂ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R)
          ((r : (a : M) → M') y' : M') :
        R)
⊢ Eq.{u_1 + 1} (α := R) ((((B₁ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) y : R)
    ((((B₂ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) y : R)

Tactic:
obtain ⟨y', rfl⟩ := hᵣ y

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
h : B₁.comp l r = B₂.comp l r
x' y' : M
mp :
  Eq.{u_1 + 1} (α := R) ((((B₁.comp l r : (a : M) → M →ₗ[R] R) x' : M →ₗ[R] R) : (a : M) → R) y' : R)
    ((((B₂ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) ((r : (a : M) → M') y' : M') :
      R)
mp₁ :
  Eq.{u_1 + 1} (α := R) ((((B₁.comp l r : (a : M) → M →ₗ[R] R) x' : M →ₗ[R] R) : (a : M) → R) y' : R)
    ((((B₂.comp l r : (a : M) → M →ₗ[R] R) x' : M →ₗ[R] R) : (a : M) → R) y' : R)
mp₂ mp₃ :
  Eq.{u_1 + 1} (α := R) ((((B₂.comp l r : (a : M) → M →ₗ[R] R) x' : M →ₗ[R] R) : (a : M) → R) y' : R)
    ((((B₂.comp l r : (a : M) → M →ₗ[R] R) x' : M →ₗ[R] R) : (a : M) → R) y' : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₁ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) ((r : (a : M) → M') y' : M') :
      R)
    ((((B₂ : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') x') : M' →ₗ[R] R) : (a : M') → R) ((r : (a : M) → M') y' : M') :
      R)

Tactic:
rw [← comp_apply, ← comp_apply, h]

Premises used: LinearMap.BilinForm.comp_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑l : (a : M) → M')
hᵣ : Function.Surjective.{u_2 + 1, w + 1} (α := M) (β := M') (⇑r : (a : M) → M')
h : B₁ = B₂
mpr mpr₁ : B₂.comp l r = B₂.comp l r
⊢ B₁.comp l r = B₂.comp l r

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
B : BilinForm R M
x y : M'
⊢ Eq.{u_1 + 1} (α := R)
    ((((((congr e : (a : BilinForm R M) → BilinForm R M') B : BilinForm R M') : (a : M') → M' →ₗ[R] R) x : M' →ₗ[R] R) :
          (a : M') → R)
        y :
      R)
    ((((B : (a : M) → M →ₗ[R] R) ((e.symm : (a : M') → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((e.symm : (a : M') → M) y : M) :
      R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
⊢ (congr e).symm = congr e.symm

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := BilinForm R M ≃ₗ[R] BilinForm R M) (congr (LinearEquiv.refl R M)) (LinearEquiv.refl R (BilinForm R M))

Tactic:
LinearEquiv.ext fun _ => ext₂ fun _ _ => rfl

Premises used: LinearEquiv.ext, LinearMap.ext₂, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
M'' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M''
inst_5 : Module R M'
inst_6 : Module R M''
e : M ≃ₗ[R] M'
f : M' ≃ₗ[R] M''
⊢ congr e ≪≫ₗ congr f = congr (e ≪≫ₗ f)

Tactic:
rfl

Premises used: LinearEquiv.congrRight, LinearEquiv.arrowCongr, LinearEquiv.toEquiv, LinearMap.BilinForm.congr, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
M'' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M''
inst_5 : Module R M'
inst_6 : Module R M''
e : M' ≃ₗ[R] M''
f : M ≃ₗ[R] M'
B : BilinForm R M
⊢ Eq (α := BilinForm R M'')
    ((congr e : (a : BilinForm R M') → BilinForm R M'') ((congr f : (a : BilinForm R M) → BilinForm R M') B) :
      BilinForm R M'')
    ((congr (f ≪≫ₗ e) : (a : BilinForm R M) → BilinForm R M'') B : BilinForm R M'')

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
M'' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M''
inst_5 : Module R M'
inst_6 : Module R M''
e : M ≃ₗ[R] M'
B : BilinForm R M
l r : M'' →ₗ[R] M'
⊢ comp ((congr e : (a : BilinForm R M) → BilinForm R M') B) l r =
    B.comp ((↑e.symm : M' →ₗ[R] M) ∘ₗ l) ((↑e.symm : M' →ₗ[R] M) ∘ₗ r)

Tactic:
rfl

Premises used: LinearMap.BilinForm.comp, LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
M'' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M''
inst_5 : Module R M'
inst_6 : Module R M''
e : M' ≃ₗ[R] M''
B : BilinForm R M
l r : M' →ₗ[R] M
⊢ (congr e : (a : BilinForm R M') → BilinForm R M'') (B.comp l r) =
    B.comp (l ∘ₗ (↑e.symm : M'' →ₗ[R] M')) (r ∘ₗ (↑e.symm : M'' →ₗ[R] M'))

Tactic:
rfl

Premises used: LinearMap.BilinForm.comp, LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ : Type u_9
N₂ : Type u_10
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : Module R N₁
inst_6 : Module R N₂
e : N₁ ≃ₗ[R] N₂
B : BilinMap R M N₁
⊢ Eq (α := BilinMap R M N₂) ((e.congrRight₂ : (a : BilinMap R M N₁) → BilinMap R M N₂) B : BilinMap R M N₂)
    (compr₂ B (↑e : N₁ →ₗ[R] N₂) : M →ₗ[R] M →ₗ[R] N₂)

Tactic:
rfl

Premises used: LinearMap.compr₂, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ : Type u_9
inst_3 : AddCommMonoid N₁
inst_4 : Module R N₁
⊢ Eq (α := BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₁) (LinearEquiv.congrRight₂ (LinearEquiv.refl R N₁))
    (LinearEquiv.refl R (BilinMap R M N₁))

Tactic:
rfl

Premises used: LinearEquiv.congrRight, LinearEquiv.congrRight₂, LinearEquiv.arrowCongr, LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ : Type u_9
N₂ : Type u_10
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : Module R N₁
inst_6 : Module R N₂
e : N₁ ≃ₗ[R] N₂
⊢ Eq (α := BilinMap R M N₂ ≃ₗ[R] BilinMap R M N₁) (LinearEquiv.symm e.congrRight₂) e.symm.congrRight₂

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.congrRight, LinearEquiv.congrRight₂, LinearEquiv.arrowCongr, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid N₃
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module R N₃
e₁₂ : N₁ ≃ₗ[R] N₂
e₂₃ : N₂ ≃ₗ[R] N₃
⊢ Eq (α := BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₃) (LinearEquiv.congrRight₂ (e₁₂ ≪≫ₗ e₂₃))
    (e₁₂.congrRight₂ ≪≫ₗ e₂₃.congrRight₂)

Tactic:
rfl

Premises used: LinearEquiv.congrRight, LinearEquiv.congrRight₂, LinearEquiv.arrowCongr, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] R
x y : M
⊢ (((linMulLin f g : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_7
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f g : M →ₗ[R] R
l r : M' →ₗ[R] M
⊢ (linMulLin f g).comp l r = linMulLin (f ∘ₗ l) (g ∘ₗ r)

Tactic:
rfl

Premises used: LinearMap.mk₂, LinearMap.mk₂'ₛₗ, LinearMap.BilinForm.linMulLin, LinearMap.mk₂', LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] R
l : M →ₗ[R] M
⊢ (linMulLin f g).compLeft l = linMulLin (f ∘ₗ l) g

Tactic:
rfl

Premises used: LinearMap.mk₂, LinearMap.mk₂'ₛₗ, LinearMap.BilinForm.compLeft, LinearMap.BilinForm.linMulLin, LinearMap.mk₂', LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] R
r : M →ₗ[R] M
⊢ (linMulLin f g).compRight r = linMulLin f (g ∘ₗ r)

Tactic:
rfl

Premises used: LinearMap.mk₂, LinearMap.mk₂'ₛₗ, LinearMap.BilinForm.linMulLin, LinearMap.mk₂', LinearMap.compl₁₂, rfl, LinearMap.compl₂, LinearMap.BilinForm.compRight
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B F₂ : BilinForm R M
ι : Type u_9
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
      ((((F₂ : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
⊢ B = F₂

Tactic:
b.ext fun i => b.ext fun j => h i j

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
rw :
  ((((B : (a : M) → M →ₗ[R] R)
            ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
              ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
          M →ₗ[R] R) :
        (a : M) → R)
      ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) :
        M) :
    R)
| ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
conv_rhs :
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (xi : R) ↦
        Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (j : ι) (yj : R) ↦
          xi •
            HSMul.hSMul (β := R) yj
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) :
                R) :
      R)
    ((((B : (a : M) → M →ₗ[R] R)
              ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
                ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) :
          M) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (xi : R) ↦
        Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (j : ι) (yj : R) ↦
          xi •
            HSMul.hSMul (β := R) yj
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) :
                R) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
conv_rhs => rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
f g : B₁ →bᵢ B₂
h :
  Eq (α := (a : M₁) → M₂) ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) f)
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
mk :
  ∀ (toLinearMap : M₁ →ₗ[R] M₂)
    (map_app' :
      ∀ (m m' : M₁),
        Eq.{u_1 + 1} (α := R)
          ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap.toFun m') :
            R)
          ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R))
    (h :
      Eq (α := (a : M₁) → M₂)
        ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap, map_app' := map_app' })
        ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)),
    { toLinearMap := toLinearMap, map_app' := map_app' : B₁ →bᵢ B₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₁ →bᵢ B₂
toLinearMap : M₁ →ₗ[R] M₂
map_app' :
  ∀ (m m' : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap.toFun m') : R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
mk :
  ∀ (toLinearMap_1 : M₁ →ₗ[R] M₂)
    (map_app'_1 :
      ∀ (m m' : M₁),
        Eq.{u_1 + 1} (α := R)
          ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap_1.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R)
              (toLinearMap_1.toFun m') :
            R)
          ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R))
    (h :
      Eq (α := (a : M₁) → M₂)
        ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap, map_app' := map_app' })
        ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })),
    { toLinearMap := toLinearMap, map_app' := map_app' : B₁ →bᵢ B₂ } =
      { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : B₁ →bᵢ B₂ } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap : M₁ →ₗ[R] M₂
map_app' :
  ∀ (m m' : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap.toFun m') : R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m m' : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap_1.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap_1.toFun m') :
        R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })
mk : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : B₁ →bᵢ B₂ } =
    { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
toLinearMap : M₁ →ₗ[R] M₂
map_app' :
  ∀ (m m' : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap.toFun m') : R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m m' : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) (toLinearMap_1.toFun m) : M₂ →ₗ[R] R) : (a : M₂) → R) (toLinearMap_1.toFun m') :
        R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : B₁ →bᵢ B₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })
⊢ toLinearMap = toLinearMap_1

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective