awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Hom (goal)
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
simp_rw :
  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.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
              HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) :
          (a : M) → R)
        (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (i : ι) (a : R) ↦
          HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : 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)
              ((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)
have simp_rw₁ : Eq.{u_1 + 1} (α := R)
  (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) x_2 : M) :
              R)) :
    R)
  (((B : (a : M) → M →ₗ[R] R)
          (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
              ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → M) x_1 : M)) :
        (a : M) → R)
      (∑ x ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
          ((b : (a : ι) → M) x : M)) :
    R)
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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)
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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)
⊢ { toLinearMap := toLinearMap, map_app' := map_app' : B₁ →bᵢ B₂ } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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, map_app' := map_app' : B₁ →bᵢ B₂ } =
    { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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₁
⊢ 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)
have 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)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Isometry (goal)
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 (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)
have 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)
Tactic: rw [Subsingleton.elim x 0, Subsingleton.elim y 0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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₂
⊢ 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
have 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
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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)
⊢ 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
have 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 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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₂
⊢ 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)
have 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)
Tactic: rw [← f.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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₂
⊢ 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)
have h : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) = n
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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
⊢ 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)
have h₁ : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv (goal)
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₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun n) : M₃ →ₗ[R] R) :
          (a : M₃) → R)
        ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)
have rw : Eq.{u_1 + 1} (α := R)
  ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun n) : M₃ →ₗ[R] R) :
        (a : M₃) → R)
      ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) :
    R)
  ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) n : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
      ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) :
    R)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) (a • x) : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
have rw : Eq.{u_7 + 1} (α := R₄)
    ((HSMul.hSMul (β := M₄ →ₗ[R₄] R₄) a ((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄)
    (0 : R₄) ↔
  Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ Eq.{u_7 + 1} (α := R₄)
      ((HSMul.hSMul (β := M₄ →ₗ[R₄] R₄) a ((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄)
      (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
have simp : a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
Tactic: simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) (a • y) : R₄) (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
have rw : HSMul.hSMul (β := R₄) a ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) = 0 ↔
  Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ HSMul.hSMul (β := R₄) a ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) = 0 ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
have simp : a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
Tactic: simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]