awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_3
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_4} ↥L
inst_4 : IsZLattice ℝ L
inst_5 : Finite ι
b : Basis.{u_3, 0, u_4} ι ℤ ↥L
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
μ : Measure E
e_1 : ↥L = ↥(span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)))
⊢ L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

Premises used: Real, Module.Basis.ofZLatticeBasis_span, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
ι : Type u_3
hs : IsZLattice K L_1
b : Basis.{u_3, 0, u_2} ι ℤ ↥L_1
E : Type u_4
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_4} ↥L
inst_14 : IsZLattice ℝ L
simp_rw :
  Countable.{u_4 + 1}
    ↥(span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L)
          (⇑(Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) : (a : Free.ChooseBasisIndex ℤ ↥L) → E)))
⊢ Countable.{u_4 + 1} ↥L

Tactic:
simp_rw [← (Module.Free.chooseBasis ℤ L).ofZLatticeBasis_span ℝ]

Premises used: Real, Membership.mem, Module.Basis.ofZLatticeBasis_span, Subtype, Int, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
ι : Type u_3
hs : IsZLattice K L_1
b : Basis.{u_3, 0, u_2} ι ℤ ↥L_1
E : Type u_4
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_4} ↥L
inst_14 : IsZLattice ℝ L
⊢ Countable.{u_4 + 1}
    ↥(span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L)
          (⇑(Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) : (a : Free.ChooseBasisIndex ℤ ↥L) → E)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
e : ↥(span ℤ s) ≃L[ℤ] ↥L := { toLinearEquiv := f.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ DiscreteTopology.{u_4} ↥L

Tactic:
e.toHomeomorph.discreteTopology

Premises used: Homeomorph.discreteTopology, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
e : ↥(span ℤ s) ≃L[ℤ] ↥L := { toLinearEquiv := f.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ DiscreteTopology.{u_4} ↥L

Tactic:
exact e.toHomeomorph.discreteTopology

Premises used: Homeomorph.discreteTopology, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
⊢ DiscreteTopology.{u_4} ↥L

Tactic:
have : DiscreteTopology L := by
    let e : span ℤ s ≃L[ℤ] L :=
      ⟨f.symm, continuous_of_discreteTopology, Isometry.continuous fun _ ↦ congrFun rfl⟩
    exact e.toHomeomorph.discreteTopology
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this : DiscreteTopology.{u_4} ↥L
⊢ IsZLattice ℝ L

Tactic:
have : IsZLattice ℝ L := ⟨eq_top_iff.mpr <|
    span_span_coe_preimage.symm.le.trans (span_mono (Set.preimage_mono subset_span))⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this_1 : DiscreteTopology.{u_4} ↥L
this : IsZLattice ℝ L
rw :
  finrank.{0, u_4} ℝ ↥(span ℝ s) =
    finrank.{0, u_4} ℤ ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s))
⊢ Set.finrank ℝ s = Set.finrank ℤ s

Tactic:
rw [Set.finrank, Set.finrank, ← f.finrank_eq]

Premises used: Set.finrank, LinearEquiv.finrank_eq
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this_1 : DiscreteTopology.{u_4} ↥L
this : IsZLattice ℝ L
⊢ finrank.{0, u_4} ℝ ↥(span ℝ s) =
    finrank.{0, u_4} ℤ ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s))

Tactic:
(ZLattice.rank ℝ L).symm

Premises used: Real, iInf, Set.Mem, Set.iInter, ZLattice.rank, Submodule.restrictScalars, setOf, Submodule.span, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this_1 : DiscreteTopology.{u_4} ↥L
this : IsZLattice ℝ L
⊢ finrank.{0, u_4} ℝ ↥(span ℝ s) =
    finrank.{0, u_4} ℤ ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s))

Tactic:
exact (ZLattice.rank ℝ L).symm

Premises used: Real, ZLattice.rank, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
rw : finrank.{0, u_1} ℤ ↥L = Fintype.card ι
rw₁ : finrank.{0, u_1} ℝ (ι → ℝ) = Fintype.card ι
rw₂ rw₃ : Fintype.card ι = Fintype.card ι
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = Fintype.card ι

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]

Premises used: Real, ZLattice.rank, Module.finrank_eq_card_chooseBasisIndex, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F →ₗ[K] E
⊢ (↑(ZLattice.comap K L e) : Set F) = (⇑e : (a : F) → E) ⁻¹' (↑L : Set E)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
L : Submodule ℤ E
⊢ ZLattice.comap K L 1 = L

Tactic:
Submodule.comap_id L

Premises used: LinearMap.restrictScalars, Submodule.comap_id, ZLattice.comap
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : DiscreteTopology.{u_2} ↥L
e : F →ₗ[K] E
he₁ : Continuous.{u_3, u_2} (X := F) (Y := E) (⇑e : (a : F) → E)
he₂ : Function.Injective.{u_3 + 1, u_2 + 1} (α := F) (β := E) (⇑e : (a : F) → E)
⊢ DiscreteTopology.{u_3} ↥(ZLattice.comap K L e)

Tactic:
DiscreteTopology.preimage_of_continuous_injective L he₁ he₂

Premises used: Set.Mem, setOf, Set.preimage, DiscreteTopology.preimage_of_continuous_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : DiscreteTopology.{u_2} ↥L
e : F →ₗ[K] E
he₁ : Continuous.{u_3, u_2} (X := F) (Y := E) (⇑e : (a : F) → E)
he₂ : Function.Injective.{u_3 + 1, u_2 + 1} (α := F) (β := E) (⇑e : (a : F) → E)
⊢ DiscreteTopology.{u_3} ↥(ZLattice.comap K L e)

Tactic:
exact DiscreteTopology.preimage_of_continuous_injective L he₁ he₂

Premises used: DiscreteTopology.preimage_of_continuous_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
e : F ≃L[K] E
⊢ DiscreteTopology.{u_3} ↥(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E))

Tactic:
ZLattice.comap_discreteTopology K L e.continuous e.injective

Premises used: ZLattice.comap_discreteTopology, ContinuousLinearEquiv.injective, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
e : F →ₗ[K] E
he : (↑L : Set E) ⊆ (↑e.range : Set E)
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : comap e (span K (↑L : Set E)) = ⊤
rw₂ : comap e ⊤ = ⊤
rw₃ rw₄ : Eq.{u_3 + 1} (α := Submodule K F) ⊤ ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L e) : Set F)) ⊤

Tactic:
rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]

Premises used: Submodule.span_preimage_eq, Submodule.nonempty, Submodule.comap_top, ZLattice.coe_comap
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₆ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) (span K (↑L : Set E)) = ⊤
rw₇ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) ⊤ = ⊤
rw₈ : (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F).range = ⊤
rw₉ rw₁₀ : Eq.{u_3 + 1} (α := Submodule K F) ⊤ ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤

Tactic:
rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.toLinearEquiv, Submodule.map_top, ContinuousLinearEquiv.coe_toLinearEquiv, ContinuousLinearEquiv.image_symm_eq_preimage, IsZLattice.span_top, Submodule.map_span, ZLattice.coe_comap, LinearEquiv.coe_coe, LinearEquiv.range
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F →ₗ[K] E
⊢ (ZLattice.comap K L e).toAddSubgroup = AddSubgroup.comap e.toAddMonoidHom L.toAddSubgroup

Tactic:
rfl

Premises used: AddSubgroup.comap, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace K G
e : F →ₗ[K] E
e' : G →ₗ[K] F
⊢ ZLattice.comap K (ZLattice.comap K L e) e' = ZLattice.comap K L (e ∘ₗ e')

Tactic:
(Submodule.comap_comp _ _ L).symm

Premises used: LinearMap.restrictScalars, ZLattice.comap, Submodule.comap_comp, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x : E
h : x ∈ L
⊢ Membership.mem (α := F) (ZLattice.comap K L (↑e : F →ₗ[K] E))
    (((↑ℤ :
              {S : Type u_1} →
                {M : Type u_2} →
                  {M₂ : Type u_3} →
                    [inst : Semiring ℤ] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module ℤ M] →
                              [inst_9 : Module ℤ M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑e.symm : E →ₗ[K] F) :
          (a : E) → F)
        x :
      F)

Tactic:
simpa [← SetLike.mem_coe] using h

Premises used: SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x_1 : ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))
x : F
hx : x ∈ ZLattice.comap K L (↑e : F →ₗ[K] E)
rwa : ∀ (hx : x ∈ (↑(ZLattice.comap K L (↑e : F →ₗ[K] E)) : Set F)), Membership.mem (α := E) L ((e : (a : F) → E) x : E)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hx : Membership.mem (γ := Set F) ((⇑(↑e : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E)) x),
    Membership.mem (α := E) L ((e : (a : F) → E) x : E)
⊢ Membership.mem (α := E) L ((e : (a : F) → E) x : E)

Tactic:
rwa [← SetLike.mem_coe, ZLattice.coe_comap] at hx

Premises used: SetLike.mem_coe, ZLattice.coe_comap
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x_1 : ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))
x : F
hx : x ∈ ZLattice.comap K L (↑e : F →ₗ[K] E)
⊢ ((LinearMap.restrict
            ((↑ℤ :
                {S : Type u_1} →
                  {M : Type u_2} →
                    {M₂ : Type u_3} →
                      [inst : Semiring ℤ] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module ℤ M] →
                                [inst_9 : Module ℤ M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (↑e.symm : E →ₗ[K] F))
            ⋯ :
          LinearMap.{0, 0, u_2, u_3} (RingHom.id ℤ) ↥L ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))) :
        (a : ↥L) → ↥(ZLattice.comap K L (↑e : F →ₗ[K] E)))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((e : (a : F) → E) x) ⋯) =
    Subtype.mk (p := fun (x : F) ↦ x ∈ ZLattice.comap K L (↑e : F →ₗ[K] E)) x hx

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x : ↥L
⊢ Eq.{u_3 + 1} (α := F) ((↑((comap_equiv K L e : (a : ↥L) → ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))) x) : F) : F)
    ((e.symm : (a : E) → F) (↑x : E) : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
ι : Type u_4
b : Basis.{u_4, 0, u_2} ι ℤ ↥L
i : ι
⊢ Eq.{u_3 + 1} (α := F) ((↑((ofZLatticeComap K L e b : (a : ι) → ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))) i) : F) : F)
    ((e.symm : (a : E) → F) (↑((b : (a : ι) → ↥L) i) : E) : F)

Tactic:
simp [Basis.ofZLatticeComap]

Premises used: Module.Basis.ofZLatticeComap
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
ι : Type u_4
b : Basis.{u_4, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
⊢ Eq (α := ℤ)
    (((((ofZLatticeComap K L e b).repr : (a : ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))) → ι →₀ ℤ)
              ((ZLattice.comap_equiv K L e : (a : ↥L) → ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))) x) :
            ι →₀ ℤ) :
          (a : ι) → ℤ)
        i :
      ℤ)
    ((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i : ℤ)

Tactic:
simp [Basis.ofZLatticeComap]

Premises used: Module.Basis.ofZLatticeComap
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
F : Type u_3
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace K F
inst_11 : FiniteDimensional K F
inst_12 : ProperSpace F
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_2} ↥L
inst_14 : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis.{u_4, 0, u_2} ι ℤ ↥L
a :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := F)
      ((ofZLatticeBasis K (ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E))
              (ofZLatticeComap K L (↑e : F ≃ₗ[K] E) b) :
            (a : ι) → F)
          i :
        F)
      ((Basis.map (ofZLatticeBasis K L b) (↑e.symm : E ≃ₗ[K] F) : (a : ι) → F) i : F)
⊢ ofZLatticeBasis K (ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) (ofZLatticeComap K L (↑e : F ≃ₗ[K] E) b) =
    Basis.map (ofZLatticeBasis K L b) (↑e.symm : E ≃ₗ[K] F)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
F : Type u_3
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace K F
inst_11 : FiniteDimensional K F
inst_12 : ProperSpace F
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_2} ↥L
inst_14 : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis.{u_4, 0, u_2} ι ℤ ↥L
i : ι
⊢ Eq.{u_3 + 1} (α := F)
    ((ofZLatticeBasis K (ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) (ofZLatticeComap K L (↑e : F ≃ₗ[K] E) b) :
          (a : ι) → F)
        i :
      F)
    ((Basis.map (ofZLatticeBasis K L b) (↑e.symm : E ≃ₗ[K] F) : (a : ι) → F) i : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
⊢ Free.{0, u_1} ℤ ↥L

Tactic:
have := ZLattice.module_free ℝ L
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ IsCompact (f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E))

Tactic:
(b.ofZLatticeBasis ℝ).parallelepiped.isCompact.image hf

Premises used: Real, Module.Basis.ofZLatticeBasis, TopologicalSpace.PositiveCompacts.isCompact, IsCompact.image, Module.Basis.parallelepiped
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h : Set.range f = f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
⊢ IsCompact (Set.range f)

Tactic:
convert! (b.ofZLatticeBasis ℝ).parallelepiped.isCompact.image hf

Premises used: Real, Module.Basis.ofZLatticeBasis, TopologicalSpace.PositiveCompacts.isCompact, IsCompact.image, Module.Basis.parallelepiped
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Set.range f = f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)

Tactic:
le_antisymm ?_ (Set.image_subset_range _ _)

Premises used: Set.image_subset_range, le_antisymm