awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
⊢ Function.Injective (α := B₁ →bᵢ B₂) toLinearMap

Tactic:
fun _f _g h =>
  DFunLike.coe_injective (congr_arg DFunLike.coe h :)

Premises used: congr_arg, DFunLike.coe_injective, Function.Injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f g : B₁ →bᵢ B₂
h : ∀ (x : M₁), Eq.{u_4 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) ((g : (a : M₁) → M₂) x : M₂)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁ →bᵢ B₂
m m' : M₁
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((f : (a : M₁) → M₂) m) : M₂ →ₗ[R] R) : (a : M₂) → R)
        ((f : (a : M₁) → M₂) m' : M₂) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m : M₁ →ₗ[R] R) : (a : M₁) → R) m' : R)

Tactic:
f.map_app' m  m'

Premises used: LinearMap.BilinForm.Isometry.map_app'
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁ →bᵢ B₂
⊢ Eq (α := (a : M₁) → M₂) (⇑f.toLinearMap : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
B : LinearMap.BilinForm R M₁
⊢ ofEq ⋯ = id B

Tactic:
rfl

Premises used: LinearMap.BilinForm.Isometry.id, rfl
-- 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₃
f : B₁ →bᵢ B₂
x y : M₁
rw :
  Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) y : M₂) : 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)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) y : M₂) : M₃) :
      R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) y : M₂) : M₃) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) y : M₂) : M₃) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) x : M₁ →ₗ[R] R) : (a : M₁) → R) y : R)

Tactic:
rw [← f.map_app, ← g.map_app]

Premises used: LinearMap.BilinForm.Isometry.map_app
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
⊢ (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁ →bᵢ B₂
⊢ (id B₂).comp f = f

Tactic:
ext fun _ => rfl

Premises used: LinearMap.BilinForm.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁ →bᵢ B₂
⊢ f.comp (id B₁) = f

Tactic:
ext fun _ => rfl

Premises used: LinearMap.BilinForm.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
h : B₃ →bᵢ B₄
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext fun _ => rfl

Premises used: LinearMap.BilinForm.Isometry.ext, rfl
-- 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₄
inst_13 : Subsingleton M₁
x y : M₁
rw :
  Eq.{u_1 + 1} (α := R)
    (((B₂ : (a : M₂) → M₂ →ₗ[R] R)
            (AddHom.toFun.{u_3, u_4} (M := M₁) (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0)
              0) :
          (a : M₂) → R)
        (AddHom.toFun.{u_3, u_4} (M := M₁) (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0) 0) :
      R)
    (((B₁ : (a : M₁) → M₁ →ₗ[R] R) 0 : (a : M₁) → R) 0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((B₂ : (a : M₂) → M₂ →ₗ[R] R)
            (AddHom.toFun (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0) x) :
          (a : M₂) → R)
        (AddHom.toFun (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0) y) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) x : M₁ →ₗ[R] R) : (a : M₁) → R) y : R)

Tactic:
rw [Subsingleton.elim x 0, Subsingleton.elim y 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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₄
inst_13 : Subsingleton M₁
x y : M₁
⊢ Eq.{u_1 + 1} (α := R)
    (((B₂ : (a : M₂) → M₂ →ₗ[R] R)
            (AddHom.toFun.{u_3, u_4} (M := M₁) (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0)
              0) :
          (a : M₂) → R)
        (AddHom.toFun.{u_3, u_4} (M := M₁) (toAddHom.{u_1, u_1, u_3, u_4} (R := R) (S := R) (σ := RingHom.id R) 0) 0) :
      R)
    (((B₁ : (a : M₁) → M₁ →ₗ[R] R) 0 : (a : M₁) → R) 0 : R)

Tactic:
simp
-- 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₄
inst_13 : Subsingleton M₂
⊢ Subsingleton (B₁ →bᵢ B₂)

Tactic:
⟨fun _ _ => ext fun _ => Subsingleton.elim _ _⟩

Premises used: Subsingleton.intro, LinearMap.BilinForm.Isometry.ext, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f g : B₁.IsometryEquiv B₂
mk :
  ∀ (toLinearEquiv : M₁ ≃ₗ[R] M₂)
    (map_app' :
      ∀ (n m : M₁),
        Eq.{u_1 + 1} (α := R)
          ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun n) : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) :
            R)
          ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)),
    Eq (α := M₁ → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.toLinearEquiv : (a : M₁) → M₂)
        (⇑g.toLinearEquiv : (a : M₁) → M₂) →
      Eq (α := M₂ → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁)
          (⇑g.symm : (a : M₂) → M₁) →
        { toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ } = g
⊢ Eq (α := M₁ → M₂) (⇑f.toLinearEquiv : (a : M₁) → M₂) (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁) (⇑f.symm : (a : M₂) → M₁) (⇑g.symm : (a : M₂) → M₁) → f = g

Tactic:
cases f
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
g : B₁.IsometryEquiv B₂
toLinearEquiv : M₁ ≃ₗ[R] M₂
map_app' :
  ∀ (n m : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun n) : M₂ →ₗ[R] R) : (a : M₂) → R)
          ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) :
        R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)
mk :
  ∀ (toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
    (map_app'_1 :
      ∀ (n m : M₁),
        Eq.{u_1 + 1} (α := R)
          ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun n) : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun m) :
            R)
          ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)),
    Eq (α := M₁ → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.toLinearEquiv : (a : M₁) → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : B₁.IsometryEquiv B₂ }.toLinearEquiv :
          (a : M₁) → M₂) →
      Eq (α := M₂ → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁) →
        { toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ } =
          { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }
⊢ Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁)
        (⇑g.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
toLinearEquiv : M₁ ≃ₗ[R] M₂
map_app' :
  ∀ (n m : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun n) : M₂ →ₗ[R] R) : (a : M₂) → R)
          ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) :
        R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)
toLinearEquiv_1 : M₁ ≃ₗ[R] M₂
map_app'_1 :
  ∀ (n m : M₁),
    Eq.{u_1 + 1} (α := R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun n) : M₂ →ₗ[R] R) : (a : M₂) → R)
          ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun m) :
        R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)
⊢ Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : B₁.IsometryEquiv B₂ }.toLinearEquiv :
        (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : B₁.IsometryEquiv B₂ }.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : B₁.IsometryEquiv B₂ } =
        { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }

Tactic:
simp +contextual
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁.IsometryEquiv B₂
⊢ Eq (α := (a : M₁) → M₂) (⇑f.toLinearEquiv : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
f : B₁.IsometryEquiv B₂
m n : M₁
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((f : (a : M₁) → M₂) n) : M₂ →ₗ[R] R) : (a : M₂) → R) ((f : (a : M₁) → M₂) m : M₂) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)

Tactic:
f.map_app' n m

Premises used: LinearMap.BilinForm.IsometryEquiv.map_app'
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n : M₂
_ :
  ∀ (m : M₂),
    Eq.{u_1 + 1} (α := R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) : M₁ →ₗ[R] R) : (a : M₁) → R)
          ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) :
        R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) n : M₂ →ₗ[R] R) : (a : M₂) → R) m : R)
⊢ ∀ (m : M₂),
    Eq.{u_1 + 1} (α := R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) : M₁ →ₗ[R] R) : (a : M₁) → R)
          ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) :
        R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) n : M₂ →ₗ[R] R) : (a : M₂) → R) m : R)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
rw :
  Eq.{u_1 + 1} (α := R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n)) : M₂ →ₗ[R] R) :
          (a : M₂) → R)
        ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) :
      R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) n : M₂ →ₗ[R] R) : (a : M₂) → R) m : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) : M₁ →ₗ[R] R) : (a : M₁) → R)
        ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) :
      R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) n : M₂ →ₗ[R] R) : (a : M₂) → R) m : R)

Tactic:
rw [← f.map_app]

Premises used: LinearMap.BilinForm.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
h : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) = n
h₁ : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n)) : M₂ →ₗ[R] R) :
          (a : M₂) → R)
        ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) :
      R)
    ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) n : M₂ →ₗ[R] R) : (a : M₂) → R) m : R)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) = n

Tactic:
f.toLinearEquiv.apply_symm_apply _

Premises used: LinearMap.BilinForm.IsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) = n

Tactic:
exact f.toLinearEquiv.apply_symm_apply _

Premises used: LinearMap.BilinForm.IsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m

Tactic:
f.toLinearEquiv.apply_symm_apply _

Premises used: LinearMap.BilinForm.IsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
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₃
f : B₁.IsometryEquiv B₂
n m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m

Tactic:
exact f.toLinearEquiv.apply_symm_apply _

Premises used: LinearMap.BilinForm.IsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply