awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
refine :
  ∀ (i : ι),
    Ne (α := AffineSubspace ℝ E)
      (AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
        AffineSubspace ℝ E)
      (⊤ : AffineSubspace ℝ E)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)

Tactic:
refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)

Premises used: Iff.mpr, Real, Set.univ, AffineSubspace.mk', MeasureTheory.measure_iUnion_null_iff, MeasureTheory.measure_mono_null, SDiff.sdiff, MeasureTheory.Measure.addHaar_affineSubspace, Submodule.span, Set.image, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
i : ι
⊢ Ne (α := AffineSubspace ℝ E)
    (AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
      AffineSubspace ℝ E)
    (⊤ : AffineSubspace ℝ E)

Tactic:
(ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm

Premises used: Iff.mpr, AffineSubspace.mem_top, Iff.not, Ne.symm, AffineSubspace.mem_mk', ne_of_mem_of_not_mem', OfNat.ofNat
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
i : ι
refine :
  VSub.vsub (P := E) (0 : E) ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
⊢ Ne (α := AffineSubspace ℝ E)
    (AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
      AffineSubspace ℝ E)
    (⊤ : AffineSubspace ℝ E)

Tactic:
refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm

Premises used: Iff.mpr, AffineSubspace.mem_top, Iff.not, Ne.symm, AffineSubspace.mem_mk', ne_of_mem_of_not_mem', OfNat.ofNat
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
i : ι
simp_rw : ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
⊢ VSub.vsub (P := E) (0 : E) ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))

Tactic:
simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]

Premises used: neg_mem_iff, vsub_eq_sub, zero_sub
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
i : ι
⊢ ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))

Tactic:
linearIndependent_iff_notMem_span.mp b.linearIndependent i

Premises used: Set.Mem, setOf, Module.Basis.linearIndependent, Iff.mp, linearIndependent_iff_notMem_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
i : ι
⊢ ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))

Tactic:
exact linearIndependent_iff_notMem_span.mp b.linearIndependent i

Premises used: Module.Basis.linearIndependent, Iff.mp, linearIndependent_iff_notMem_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
suffices :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)

Tactic:
suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b
⊢ (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)

Tactic:
simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx

Premises used: Set.mem_Ico, Set.mem_setOf_eq, parallelepiped_basis_eq, not_lt, Set.mem_diff, Set.mem_Icc, not_and, Classical.not_forall, ZSpan.mem_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
obtain :
  ∀ (i : ι)
    (hi :
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      x
⊢ Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    x

Tactic:
obtain ⟨i, hi⟩ := hx.2

Premises used: And.right
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i : ι
hi :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
⊢ Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)

Tactic:
have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i : ι
hi :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
rw :
  Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    (HVAdd.hVAdd (α := E) (β := E)
      (∑ x_1 ∈ Finset.erase Finset.univ i,
        HSMul.hSMul (α := ℝ) (β := E) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
          ((b : (a : ι) → E) x_1 : E))
      ((b : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    x

Tactic:
rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]

Premises used: Finset.mem_univ, one_smul, Finset.sum_erase_add, vadd_eq_add, Module.Basis.sum_repr
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i : ι
hi :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
⊢ Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    (HVAdd.hVAdd (α := E) (β := E)
      (∑ x_1 ∈ Finset.erase Finset.univ i,
        HSMul.hSMul (α := ℝ) (β := E) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
          ((b : (a : ι) → E) x_1 : E))
      ((b : (a : ι) → E) i : E))

Tactic:
Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩

Premises used: Iff.mpr, AffineSubspace.vadd_mem_mk', Submodule.sum_smul_mem, Set.mem_iUnion, Exists.intro, Submodule.subset_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i : ι
hi :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
refine :
  ∀ (i_1 : ι) (hi : i_1 ∈ Finset.erase Finset.univ i),
    Membership.mem.{u_1, u_1} (α := E) (γ := Set E) (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
      ((b : (a : ι) → E) i_1 : E)
⊢ Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    (HVAdd.hVAdd (α := E) (β := E)
      (∑ x_1 ∈ Finset.erase Finset.univ i,
        HSMul.hSMul (α := ℝ) (β := E) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
          ((b : (a : ι) → E) x_1 : E))
      ((b : (a : ι) → E) i : E))

Tactic:
refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i_1 : ι
hi_1 :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ)
this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ) (1 : ℝ)
i : ι
hi : i ∈ Finset.erase Finset.univ i_1
⊢ Membership.mem.{u_1, u_1} (α := E) (γ := Set E) (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i_1}))
    ((b : (a : ι) → E) i : E)

Tactic:
⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩

Premises used: Iff.mpr, trivial, Set.Mem, setOf, Finset.ne_of_mem_erase, And.intro, Exists.intro, Set.image, rfl, Set.mem_diff_singleton
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
x : E
hx :
  (∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
    ∃ (x_1 : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
i_1 : ι
hi_1 :
  LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ) →
    LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ)
this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i_1 : ℝ) (1 : ℝ)
i : ι
hi : i ∈ Finset.erase Finset.univ i_1
⊢ Membership.mem.{u_1, u_1} (α := E) (γ := Set E) (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i_1}))
    ((b : (a : ι) → E) i : E)

Tactic:
exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
obtain :
  ∀ (s : Set E) (h_incl : s ⊆ (↑L : Set E)) (h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E)))
    (h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))),
    L.FG
⊢ L.FG

Tactic:
obtain ⟨s, ⟨h_incl, ⟨h_span, h_lind⟩⟩⟩ := exists_linearIndependent K (L : Set E)

Premises used: exists_linearIndependent, SetLike.coe
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ L.FG

Tactic:
fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_

Premises used: Int, Submodule.span, Submodule.mkQ, Submodule.fg_of_fg_map_of_fg_inf_ker
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_1 : Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)
refine_2 : (L ⊓ LinearMap.ker (M₂ := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (mkQ (span ℤ s))).FG
⊢ L.FG

Tactic:
refine fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_

Premises used: Int, Submodule.span, Submodule.mkQ, Submodule.fg_of_fg_map_of_fg_inf_ker
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)

Tactic:
fg_def.mpr ⟨map (span ℤ s).mkQ L, ?_, span_eq _⟩

Premises used: Iff.mpr, Submodule.fg_def, Int, Submodule.span_eq, SetLike.coe, And.intro, Exists.intro, Submodule.span, Submodule.mkQ, Submodule.map
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_1 : (↑(Submodule.map (mkQ (span ℤ s)) L) : Set (E ⧸ span ℤ s)).Finite
⊢ Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)

Tactic:
refine fg_def.mpr ⟨map (span ℤ s).mkQ L, ?_, span_eq _⟩

Premises used: Iff.mpr, Submodule.fg_def, And.intro, Exists.intro
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
rw :
  LE.le (α := Submodule K E) (span K s)
    (span K (Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))))
⊢ LE.le.{u_2} (α := Submodule K E) ⊤
    (span K (Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))))

Tactic:
rw [← hs.span_top, ← h_span]

Premises used: IsZLattice.span_top