awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₁ →qᵢ Q₂
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
mk :
  ∀ (toLinearMap_1 : M₁ →ₗ[R] M₂)
    (map_app'_1 :
      ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N))
    (h :
      Eq (α := (a : M₁) → M₂)
        ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap, map_app' := map_app' })
        ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap_1, map_app' := map_app'_1 })),
    { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } =
      { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑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' : Q₁ →qᵢ Q₂ } =
    { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑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
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap : M₁ →ₗ[R] M₂
map_app' : ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
toLinearMap_1 : M₁ →ₗ[R] M₂
map_app'_1 :
  ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap_1.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
h :
  Eq (α := (a : M₁) → M₂)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
      { toLinearMap := toLinearMap, map_app' := map_app' })
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑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.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
⊢ Function.Injective (α := Q₁ →qᵢ Q₂) 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.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f g : Q₁ →qᵢ Q₂
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.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁ →qᵢ Q₂
m : M₁
⊢ Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) m : M₂) : N) ((Q₁ : (a : M₁) → N) m : N)

Tactic:
f.map_app' m

Premises used: QuadraticMap.Isometry.map_app'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁ →qᵢ Q₂
⊢ Eq (α := (a : M₁) → M₂) (⇑f.toLinearMap : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid N
inst_3 : Module R M₁
inst_4 : Module R N
Q : QuadraticMap R M₁ N
⊢ ofEq ⋯ = id Q

Tactic:
rfl

Premises used: QuadraticMap.Isometry.id, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
rw :
  Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) x : M₂) : N)
rw₁ rw₂ :
  Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
⊢ Eq.{u_7 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃) : N)
    ((Q₁ : (a : M₁) → N) x : N)

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

Premises used: QuadraticMap.Isometry.map_app
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
⊢ (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁ →qᵢ Q₂
⊢ (id Q₂).comp f = f

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁ →qᵢ Q₂
⊢ f.comp (id Q₁) = f

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
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 N
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
inst_9 : Module R M₄
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
h : Q₃ →qᵢ Q₄
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.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
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
inst_13 : Subsingleton M₂
⊢ Subsingleton (Q₁ →qᵢ Q₂)

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

Premises used: QuadraticMap.Isometry.ext, Subsingleton.intro, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f g : Q₁.IsometryEquiv Q₂
mk :
  ∀ (toLinearEquiv : M₁ ≃ₗ[R] M₂)
    (map_app' :
      ∀ (m : M₁),
        Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) : N)
          ((Q₁ : (a : M₁) → N) m : N)),
    Eq (α := M₁ → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
        (⇑g.toLinearEquiv : (a : M₁) → M₂) →
      Eq (α := M₂ → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
          (⇑g.symm : (a : M₂) → M₁) →
        { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } = 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.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₁.IsometryEquiv Q₂
toLinearEquiv : M₁ ≃ₗ[R] M₂
map_app' :
  ∀ (m : M₁),
    Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
mk :
  ∀ (toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
    (map_app'_1 :
      ∀ (m : M₁),
        Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun m) : N)
          ((Q₁ : (a : M₁) → N) m : N)),
    Eq (α := M₁ → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
        (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.toLinearEquiv :
          (a : M₁) → M₂) →
      Eq (α := M₂ → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
          (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁) →
        { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } =
          { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }
⊢ Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑g.toLinearEquiv : (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
        (⇑g.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
toLinearEquiv : M₁ ≃ₗ[R] M₂
map_app' :
  ∀ (m : M₁),
    Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv : M₁ →ₗ[R] M₂).toFun m) : N) ((Q₁ : (a : M₁) → N) m : N)
toLinearEquiv_1 : M₁ ≃ₗ[R] M₂
map_app'_1 :
  ∀ (m : M₁),
    Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((↑toLinearEquiv_1 : M₁ →ₗ[R] M₂).toFun m) : N)
      ((Q₁ : (a : M₁) → N) m : N)
⊢ Eq (α := M₁ → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.toLinearEquiv : (a : M₁) → M₂)
      (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.toLinearEquiv :
        (a : M₁) → M₂) →
    Eq (α := M₂ → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁)
        (⇑{ toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 : Q₁.IsometryEquiv Q₂ }.symm : (a : M₂) → M₁) →
      { toLinearEquiv := toLinearEquiv, map_app' := map_app' : Q₁.IsometryEquiv Q₂ } =
        { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }

Tactic:
simp +contextual
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁.IsometryEquiv Q₂
⊢ Eq (α := (a : M₁) → M₂) (⇑f.toLinearEquiv : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁.IsometryEquiv Q₂
m : M₁
⊢ Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) m : M₂) : N) ((Q₁ : (a : M₁) → N) m : N)

Tactic:
f.map_app' m

Premises used: QuadraticMap.IsometryEquiv.map_app'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
rw :
  Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) : N)
    ((Q₂ : (a : M₂) → N) m : N)
⊢ Eq.{u_9 + 1} (α := N) ((Q₁ : (a : M₁) → N) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : N) ((Q₂ : (a : M₂) → N) m : N)

Tactic:
rw [← f.map_app]

Premises used: QuadraticMap.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
h : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m
⊢ Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) : N)
    ((Q₂ : (a : M₂) → N) m : N)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m

Tactic:
f.toLinearEquiv.apply_symm_apply m

Premises used: LinearEquiv.apply_symm_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m

Tactic:
exact f.toLinearEquiv.apply_symm_apply m

Premises used: LinearEquiv.apply_symm_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
rw :
  Eq.{u_9 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) : N)
    ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) : N)
⊢ Eq.{u_9 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) : N)
    ((Q₁ : (a : M₁) → N) m : N)

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

Premises used: QuadraticMap.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Eq.{u_9 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) : N)
    ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) : N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁.IsometryEquiv Q₂
x : M₂
⊢ (f : (a : M₁) → M₂) ((f.symm : (a : M₂) → M₁) x : M₁) = x

Tactic:
f.toEquiv.apply_symm_apply x

Premises used: Equiv.apply_symm_apply, LinearEquiv.toEquiv, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁.IsometryEquiv Q₂
x : M₁
⊢ (f.symm : (a : M₂) → M₁) ((f : (a : M₁) → M₂) x : M₂) = x

Tactic:
f.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, LinearEquiv.toEquiv, QuadraticMap.IsometryEquiv.toLinearEquiv