awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis ⋯ b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₁ : Eq.{u_3 + 1} (α := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.flip.dualBasis sorry b)) : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis ⋯ b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.flip.dualBasis ⋯ b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₂ : Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
⊢ Eq (α := Submodule R M)
    (B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw : Eq (α := Submodule R M)
  (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
    dualBasis_flip_dualBasis hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₁ : Eq.{u_3 + 1} (α := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis sorry (B.dualBasis hB b)) : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
    dualBasis_flip_dualBasis hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis ⋯ (B.dualBasis hB b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₂ : Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
    dualBasis_flip_dualBasis hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := ⋯
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw : Eq (α := Submodule R M)
  (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₁ : Eq.{u_3 + 1} (α := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.dualBasis hB b)) : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.dualBasis hB b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw₂ : Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']
-- 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
r : M →ₗ[R] M
⊢ B.comp id r = B.compRight r
have H : ∀ (x y : M),
  Eq.{u_1 + 1} (α := R) ((((B.comp id r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B.compRight r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: ext
-- 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
l : M →ₗ[R] M
⊢ B.comp l id = B.compLeft l
have H : ∀ (x y : M),
  Eq.{u_1 + 1} (α := R) ((((B.comp l id : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B.compLeft l : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: ext
-- 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
⊢ B.compLeft id = B
have H : ∀ (x y : M),
  Eq.{u_1 + 1} (α := R) ((((B.compLeft 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: ext
-- 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
⊢ B.compRight id = B
have 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)
Tactic: ext
-- 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
⊢ B.comp id id = B
have 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)
Tactic: ext
-- 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
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')
⊢ B₁.comp l r = B₂.comp l r ↔ B₁ = B₂
have mp : B₁.comp l r = B₂.comp l r → B₁ = B₂
Tactic: constructor
-- 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
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₂
⊢ B₁.comp l r = B₂.comp l r ↔ B₁ = B₂
have mpr : B₁ = B₂ → B₁.comp l r = B₂.comp l r
Tactic: constructor
-- 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
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
⊢ B₁ = B₂
have 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)
Tactic: ext x y
-- 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
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'
⊢ 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)
have 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)
Tactic: obtain ⟨x', rfl⟩ := hₗ x
Cleared hypotheses: x
-- 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
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
⊢ 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)
have 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)
Tactic: obtain ⟨y', rfl⟩ := hᵣ y
Cleared hypotheses: y
-- 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
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
⊢ 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)
have 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)
Tactic: rw [← comp_apply, ← comp_apply, h]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← comp_apply, ← comp_apply, h]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← comp_apply, ← comp_apply, h]
-- 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
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₂
⊢ B₁.comp l r = B₂.comp l r
have mpr : B₂.comp l r = B₂.comp l r
Tactic: rw [h]
-- 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
| ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have 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)
Tactic: rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]
-- 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
⊢ 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)
have 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)
Tactic: conv_rhs => rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]
-- 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
⊢ 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)
  (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)
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
    smul_eq_mul]