-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Basis.ofZLatticeBasis_repr_apply (x : L) (i : ι) :
    (b.ofZLatticeBasis K L).repr x i = b.repr x i

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i✝ i : ι
⊢ (↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)

Tactic:
simp_rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
  LinearEquiv.coe_coe, coe_subtype, ← b.ofZLatticeBasis_apply K, repr_self,
  Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr

Tactic:
refine Basis.ext b fun i ↦ ?_

Result:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i✝ i : ι
⊢ (↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ((ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

Tactic:
suffices ((b.ofZLatticeBasis K L).repr.toLinearMap.restrictScalars ℤ) ∘ₗ L.subtype
    = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ b.repr.toLinearMap by
  exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Result:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i : ι
this : ↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr
⊢ ((ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Result:
no goals