awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
inst_3 : Module.IsTorsionFree R β
this : AddCommMonoid α := e.addCommMonoid
this_1 : Module R α := Equiv.module R e
⊢ Module.IsTorsionFree R α

Tactic:
exact (e.linearEquiv R).injective.moduleIsTorsionFree _ (by simp)

Premises used: Equiv.linearEquiv, Function.Injective.moduleIsTorsionFree, LinearEquiv.injective
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (x y : A) (b : α), (x * y) • b = x • y • b

Tactic:
simp [Equiv.smul_def, mul_smul]

Premises used: Equiv.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (b : α), HSMul.hSMul.{u_4, u_2, u_2} (α := A) 1 b = b

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (a : A), HSMul.hSMul (β := α) a 0 = 0

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (a : A) (x y : α), a • (x + y) = a • x + a • y

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (r s : A) (x : α), (r + s) • x = r • x + s • x

Tactic:
simp [Equiv.smul_def, add_smul]

Premises used: Equiv.smul_def, add_smul
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
e : α ≃+ β
⊢ ∀ (x : α), HSMul.hSMul.{u_4, u_2, u_2} (α := A) 0 x = 0

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
inst_6 : Module R α
inst_7 : Module R β
inst_8 : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
smul_assoc : ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z
⊢ IsScalarTower R A α

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
inst_6 : Module R α
inst_7 : Module R β
inst_8 : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
smul_assoc :
  ({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.symm : (a : β) → α)
      (x •
        HSMul.hSMul (β := β) y
          (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
                (a : α) → β)
              z :
            β)) =
    HSMul.hSMul (β := α) x
      (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.symm :
            (a : β) → α)
          (HSMul.hSMul (β := β) y
            (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
                  (a : α) → β)
                z :
              β)) :
        α)
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Equiv.smul_def, smul_assoc]

Premises used: smul_assoc, Equiv.smul_def
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
inst_6 : Module R α
inst_7 : Module R β
inst_8 : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ ({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.symm : (a : β) → α)
      (x •
        HSMul.hSMul (β := β) y
          (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
                (a : α) → β)
              z :
            β)) =
    HSMul.hSMul (β := α) x
      (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.symm :
            (a : β) → α)
          (HSMul.hSMul (β := β) y
            (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
                  (a : α) → β)
                z :
              β)) :
        α)

Tactic:
apply e.symm.map_smul

Premises used: LinearEquiv.symm, LinearEquiv.map_smul
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
inst : SMul R M
s : ULift.{u_1, u} R
x : M
⊢ s • x = s.down • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : SMul R M
inst_1 : SMul M N
inst_2 : SMul R N
inst_3 : IsScalarTower R M N
⊢ IsScalarTower (ULift.{u_1, u} R) M N

Tactic:
⟨fun x y z => show (x.down • y) • z = x.down • y • z from smul_assoc _ _ _⟩

Premises used: smul_assoc, IsScalarTower.mk, ULift.down
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : SMul R M
inst_1 : SMul M N
inst_2 : SMul R N
inst_3 : IsScalarTower R M N
⊢ IsScalarTower R (ULift.{u_1, v} M) N

Tactic:
⟨fun x y z => show (x • y.down) • z = x • y.down • z from smul_assoc _ _ _⟩

Premises used: smul_assoc, IsScalarTower.mk, ULift.down
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : SMul R M
inst_1 : SMul M N
inst_2 : SMul R N
inst_3 : IsScalarTower R M N
x : R
y : M
z : ULift.{u_1, w} N
rw rw₁ : { down := x • y • z.down : ULift.{u_1, w} N } = { down := x • y • z.down }
⊢ { down := (x • y) • z.down : ULift.{u_1, w} N } = { down := x • y • z.down }

Tactic:
rw [smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : SMul R M
inst_1 : SMul.{u, v} Rᵐᵒᵖ M
inst_2 : IsCentralScalar R M
⊢ IsCentralScalar R (ULift.{u_1, v} M)

Tactic:
⟨fun r m => congr_arg up <| op_smul_eq_smul r m.down⟩

Premises used: congr_arg, IsCentralScalar.mk, ULift.up, ULift.down, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
h : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) c 0) = down.{u_1, v} 0
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) c 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
⊢ down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) c 0) = down.{u_1, v} 0

Tactic:
simp [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
h h₁ : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) c 0) = down.{u_1, v} 0
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) c 0 = 0

Tactic:
{ ext; simp [smul_zero] }

Premises used: smul_zero
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : AddZeroClass M
inst_1 : DistribSMul R M
c : R
f g : ULift.{u_1, v} M
h : down.{u_1, v} (c • (f + g)) = down.{u_1, v} (c • f + c • g)
⊢ c • (f + g) = c • f + c • g

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : AddZeroClass M
inst_1 : DistribSMul R M
c : R
f g : ULift.{u_1, v} M
⊢ down.{u_1, v} (c • (f + g)) = down.{u_1, v} (c • f + c • g)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
h : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) x 1) = down.{u_1, v} 1
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) x 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
⊢ down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) x 1) = down.{u_1, v} 1

Tactic:
simp [smul_one]

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
x_1 x_2 : ULift.{u_1, v} M
h : down.{u_1, v} (x • (x_1 * x_2)) = down.{u_1, v} (x • x_1 * x • x_2)
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ULift
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
x_1 x_2 : ULift.{u_1, v} M
⊢ down.{u_1, v} (x • (x_1 * x_2)) = down.{u_1, v} (x • x_1 * x • x_2)

Tactic:
simp [smul_mul']

Premises used: smul_mul'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
⊢ Eq (α := Submodule K E) (span K (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)) ⊤

Tactic:
simp [span_span_of_tower]

Premises used: Submodule.span_span_of_tower
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E ≃ₗ[K] F
simp_rw :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      (Set.image.{u_1, u_4} (α := E) (⇑(↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F) : (a : E) → F)
        (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₁ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      ((fun (a : E) ↦ (LinearEquiv.restrictScalars ℤ f : (a : E) → F) a) ''
        Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₂ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ ((fun (a : E) ↦ (f : (a : E) → F) a) '' Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₃ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ ((fun (a : E) ↦ (f : (a : E) → F) a) '' Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ
      (Set.range.{u_4, u_2 + 1} (ι := ι)
        (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) (⇑b : (a : ι) → E))))
⊢ Eq (α := Submodule ℤ F)
    (Submodule.map (↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))

Tactic:
simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]

Premises used: Module.Basis.coe_map, LinearEquiv.restrictScalars_apply, Set.range_comp, Submodule.map_span, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
rw :
  Eq.{u_1 + 1} (α := Submodule ℤ E) (span ℤ (Set.range fun (i : ι) ↦ HSMul.hSMul (β := E) c ((b : (a : ι) → E) i : E)))
    (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯) : (a : ι) → E)))
⊢ HSMul.hSMul (β := Submodule ℤ E) c (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) =
    span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯) : (a : ι) → E))

Tactic:
rw [smul_span, Set.smul_set_range]

Premises used: Set.smul_set_range, Submodule.smul_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
h :
  ∀ (x : ι), HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = (b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯ : (a : ι) → E) x
⊢ Eq.{u_1 + 1} (α := Submodule ℤ E) (span ℤ (Set.range fun (i : ι) ↦ HSMul.hSMul (β := E) c ((b : (a : ι) → E) i : E)))
    (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯) : (a : ι) → E)))

Tactic:
congr!
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
x : ι
h h₁ : HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E)
⊢ HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = (b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯ : (a : ι) → E) x

Tactic:
rw [Basis.isUnitSMul_apply]

Premises used: Module.Basis.isUnitSMul_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
m : E
⊢ m ∈ fundamentalDomain b ↔
    ∀ (i : ι),
      Membership.mem.{u_3, u_3} (α := K) (γ := Set K) (Set.Ico 0 1)
        ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, ZSpan.fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
h :
  ∀ (x : F), Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔ x ∈ fundamentalDomain (b.map f)
⊢ (⇑f : (a : E) → F) '' fundamentalDomain b = fundamentalDomain (b.map f)

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ Eq.{u_1 + 1} (α := E) ((f.symm : (a : F) → E) x : E) ((f.toEquiv.symm : (a : F) → E) x : E)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
x : F
h :
  Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔
    Membership.mem (γ := Set F) ((⇑f.toEquiv : (a : E) → F) '' fundamentalDomain b) x
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔ x ∈ fundamentalDomain (b.map f)

Tactic:
rw [mem_fundamentalDomain, Basis.map_repr, LinearEquiv.trans_apply, ← mem_fundamentalDomain,
    show f.symm x = f.toEquiv.symm x by rfl, ← Set.mem_image_equiv]

Premises used: Module.Basis.map_repr, LinearEquiv.trans_apply, ZSpan.mem_fundamentalDomain, Set.mem_image_equiv
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔
    Membership.mem (γ := Set F) ((⇑f.toEquiv : (a : E) → F) '' fundamentalDomain b) x

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
ι' : Type u_4
e : ι ≃ ι'
h : ∀ (x : E), x ∈ fundamentalDomain (b.reindex e) ↔ x ∈ fundamentalDomain b
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
ι' : Type u_4
e : ι ≃ ι'
x : E
⊢ x ∈ fundamentalDomain (b.reindex e) ↔ x ∈ fundamentalDomain b

Tactic:
simp [e.forall_congr_left]

Premises used: Equiv.forall_congr_left
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Fintype ι
h :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (fundamentalDomain (ι := ι) (K := ℝ) (Pi.basisFun ℝ ι)) x ↔
      Membership.mem (γ := Set (ι → ℝ)) (Set.pi (α := fun (x : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1) x
⊢ Eq.{u_2 + 1} (α := Set (ι → ℝ)) (fundamentalDomain (ι := ι) (K := ℝ) (Pi.basisFun ℝ ι))
    (Set.pi (α := fun (x : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Fintype ι
x : ι → ℝ
⊢ Membership.mem (γ := Set (ι → ℝ)) (fundamentalDomain (ι := ι) (K := ℝ) (Pi.basisFun ℝ ι)) x ↔
    Membership.mem (γ := Set (ι → ℝ)) (Set.pi (α := fun (x : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
i : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)

Tactic:
simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Premises used: Submodule.coe_sum, Finset.mem_univ, if_true, Finset.sum_ite_eq', Finset.sum_apply', ZSpan.floor, Module.Basis.restrictScalars_apply, Finsupp.smul_single', Module.Basis.repr, map_sum, Submodule.coe_smul_of_tower, LinearEquiv.map_smul, Finsupp.single_apply, mul_one, Int.cast_smul_eq_zsmul, Module.Basis.repr_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
i : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)

Tactic:
classical simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Premises used: Submodule.coe_sum, Finset.mem_univ, if_true, Finset.sum_ite_eq', Finset.sum_apply', ZSpan.floor, Module.Basis.restrictScalars_apply, Finsupp.smul_single', Module.Basis.repr, map_sum, Submodule.coe_smul_of_tower, LinearEquiv.map_smul, Finsupp.single_apply, mul_one, Int.cast_smul_eq_zsmul, Module.Basis.repr_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
i : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(ceil b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)

Tactic:
simp only [ceil, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Premises used: Submodule.coe_sum, Finset.mem_univ, if_true, Finset.sum_ite_eq', Finset.sum_apply', Module.Basis.restrictScalars_apply, Finsupp.smul_single', Module.Basis.repr, map_sum, Submodule.coe_smul_of_tower, ZSpan.ceil, LinearEquiv.map_smul, Finsupp.single_apply, mul_one, Int.cast_smul_eq_zsmul, Module.Basis.repr_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
i : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(ceil b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)

Tactic:
classical simp only [ceil, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Premises used: Submodule.coe_sum, Finset.mem_univ, if_true, Finset.sum_ite_eq', Finset.sum_apply', Module.Basis.restrictScalars_apply, Finsupp.smul_single', Module.Basis.repr, map_sum, Submodule.coe_smul_of_tower, ZSpan.ceil, LinearEquiv.map_smul, Finsupp.single_apply, mul_one, Int.cast_smul_eq_zsmul, Module.Basis.repr_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
apply :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
⊢ (↑(floor b m) : E) = m

Tactic:
apply b.ext_elem

Premises used: Module.Basis.ext_elem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
simp_rw :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := K)
      ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
⊢ ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)

Tactic:
simp_rw [repr_floor_apply b]

Premises used: ZSpan.repr_floor_apply