awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
hf : Subset (α := Set A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) {a : A | IsStrictlyPositive a}
⊢ ConvexOn ℝ (E := A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) Ring.inverse

Tactic:
refine ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))

Premises used: CStarAlgebra.convexOn_ringInverse, ConvexOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
hf : Subset (α := Set A) (Ici ((algebraMap ℝ A : (a : ℝ) → A) t) : Set A) ({a : A | IsStrictlyPositive a} : Set A)
⊢ Subset (α := Set A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) {a : A | IsStrictlyPositive a}

Tactic:
simp only [AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add,
    LinearMap.coe_toAffineMap, LinearMap.id_coe, AffineMap.coe_const, Pi.add_apply, id_eq,
    Function.const_apply, image_add_right, preimage_add_const_Ici, sub_neg_eq_add, zero_add, addl]

Premises used: Function.const_apply, LinearMap.id_coe, AffineMap.coe_const, LinearMap.coe_toAffineMap, zero_add, Set.image_add_right, Pi.add_apply, AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add, sub_neg_eq_add, id_eq, Set.preimage_add_const_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
x : A
hx : Membership.mem (γ := Set A) (Ici ((algebraMap ℝ A : (a : ℝ) → A) t) : Set A) x
⊢ IsStrictlyPositive (A := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ Subset (α := Set A) (Ici ((algebraMap ℝ A : (a : ℝ) → A) t) : Set A) ({a : A | IsStrictlyPositive a} : Set A)

Tactic:
exact fun x hx  => IsStrictlyPositive.of_le (by grind) hx

Premises used: IsStrictlyPositive.of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ Fintype.card (Fin 2) = finrank ℝ ℂ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ (L.basis : (a : Fin 2) → ℂ) 0 = L.ω₁

Tactic:
simp [PeriodPair.basis]

Premises used: PeriodPair.basis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ (L.basis : (a : Fin 2) → ℂ) 1 = L.ω₂

Tactic:
simp [PeriodPair.basis]

Premises used: PeriodPair.basis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
⊢ x ∈ L.lattice ↔ ∃ (m : ℤ) (n : ℤ), (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = x

Tactic:
simp only [lattice, Submodule.mem_span_pair, zsmul_eq_mul]

Premises used: zsmul_eq_mul, Submodule.mem_span_pair, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Membership.mem (γ := Set ℂ) {L.ω₁, L.ω₂} L.ω₁

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Membership.mem (γ := Set ℂ) {L.ω₁, L.ω₂} L.ω₂

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1

Tactic:
⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: HMul.hMul, Membership.mem, Rat.cast, PeriodPair.ω₂, _private.0.PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice.match_1, PeriodPair.ω₁, HAdd.hAdd, Iff.intro, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
refine_1 : ∀ (H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice), α.den = 1 ∧ β.den = 1
refine_2 : α.den = 1 ∧ β.den = 1 → ∀ (h₁ : α.den = 1) (h₂ : β.den = 1), (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
refine_1 :
  ∀ (m n : ℤ) (e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂), α.den = 1 ∧ β.den = 1
⊢ α.den = 1 ∧ β.den = 1

Tactic:
obtain ⟨m, n, e⟩ := mem_lattice.mp H

Premises used: PeriodPair.mem_lattice, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
simp : HSub.hSub (α := ℂ) (↑m : ℂ) (↑α : ℂ) * L.ω₁ + HSub.hSub (α := ℂ) (↑n : ℂ) (↑β : ℂ) * L.ω₂ = 0
⊢ HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) • L.ω₁ + HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) • L.ω₂ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
⊢ HSub.hSub (α := ℂ) (↑m : ℂ) (↑α : ℂ) * L.ω₁ + HSub.hSub (α := ℂ) (↑n : ℂ) (↑β : ℂ) * L.ω₂ = 0

Tactic:
linear_combination e
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
⊢ HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) = 0 ∧ HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) = 0

Tactic:
have := LinearIndependent.pair_iff.mp L.indep (m - α) (n - β)
      (by simp; linear_combination e)
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
this : HSub.hSub (α := ℝ) (↑m : ℝ) (↑α : ℝ) = 0 ∧ HSub.hSub (α := ℝ) (↑n : ℝ) (↑β : ℝ) = 0
⊢ Eq (α := ℝ) (↑m : ℝ) (↑α : ℝ) ∧ Eq (α := ℝ) (↑n : ℝ) (↑β : ℝ)

Tactic:
simp only [sub_eq_zero] at this

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
this : Eq (α := ℝ) (↑m : ℝ) (↑α : ℝ) ∧ Eq (α := ℝ) (↑n : ℝ) (↑β : ℝ)
⊢ (↑m : ℚ) = α ∧ (↑n : ℚ) = β

Tactic:
norm_cast at this
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
H : (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
m n : ℤ
e : (↑m : ℂ) * L.ω₁ + (↑n : ℂ) * L.ω₂ = (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂
this : (↑m : ℚ) = α ∧ (↑n : ℚ) = β
⊢ α.den = 1 ∧ β.den = 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
h : α.den = 1 ∧ β.den = 1
h₁ : α.den = 1
h₂ : β.den = 1
⊢ α.den = 1

Tactic:
h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℚ
h : α.den = 1 ∧ β.den = 1
h₁ : α.den = 1
h₂ : β.den = 1
refine_2 : ∀ (α : ℤ), Rat.den (↑α : ℚ) = 1 ∧ β.den = 1 → (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice
⊢ (↑α : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice

Tactic:
lift α to ℤ using h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
β : ℚ
h₂ : β.den = 1
α : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ β.den = 1
⊢ β.den = 1

Tactic:
h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
β : ℚ
h₂ : β.den = 1
α : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ β.den = 1
refine_2 :
  ∀ (β : ℤ), Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1 → (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑(↑β : ℚ) : ℂ) * L.ω₂ ∈ L.lattice
⊢ (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑β : ℂ) * L.ω₂ ∈ L.lattice

Tactic:
lift β to ℤ using h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1
refine_2 : α • L.ω₁ + β • L.ω₂ ∈ L.lattice
⊢ (↑(↑α : ℚ) : ℂ) * L.ω₁ + (↑(↑β : ℚ) : ℂ) * L.ω₂ ∈ L.lattice

Tactic:
simp only [Rat.cast_intCast, ← zsmul_eq_mul]

Premises used: zsmul_eq_mul, Rat.cast_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1
⊢ α • L.ω₁ + β • L.ω₂ ∈ L.lattice

Tactic:
add_mem (Submodule.smul_mem _ _ L.ω₁_mem_lattice)
      (Submodule.smul_mem _ _ L.ω₂_mem_lattice)

Premises used: AddMemClass.add_mem, PeriodPair.ω₁_mem_lattice, PeriodPair.ω₂_mem_lattice, Submodule.smul_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
α β : ℤ
h : Rat.den (↑α : ℚ) = 1 ∧ Rat.den (↑β : ℚ) = 1
⊢ α • L.ω₁ + β • L.ω₂ ∈ L.lattice

Tactic:
exact add_mem (Submodule.smul_mem _ _ L.ω₁_mem_lattice)
      (Submodule.smul_mem _ _ L.ω₂_mem_lattice)

Premises used: AddMemClass.add_mem, PeriodPair.ω₁_mem_lattice, PeriodPair.ω₂_mem_lattice, Submodule.smul_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ ¬((1 / 2).den = 1 ∧ Rat.den 0 = 1)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ L.ω₁ / 2 ∉ L.lattice

Tactic:
simpa [inv_mul_eq_div] using
    (L.mul_ω₁_add_mul_ω₂_mem_lattice (α := 1 / 2) (β := 0)).not.mpr (by norm_num)

Premises used: Iff.mpr, inv_mul_eq_div, Iff.not, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ ¬(Rat.den 0 = 1 ∧ (1 / 2).den = 1)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ L.ω₂ / 2 ∉ L.lattice

Tactic:
simpa [inv_mul_eq_div] using
    (L.mul_ω₁_add_mul_ω₂_mem_lattice (α := 0) (β := 1 / 2)).not.mpr (by norm_num)

Premises used: Iff.mpr, inv_mul_eq_div, Iff.not, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ Eq (α := Finset (Fin 2)) Finset.univ {0, 1}

Tactic:
have : Finset.univ (α := Fin 2) = {0, 1} := rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : Eq (α := Finset (Fin 2)) Finset.univ {0, 1}
rw :
  Eq (α := Submodule ℤ ℂ) (Submodule.span ℤ {L.ω₁, L.ω₂})
    (Submodule.span ℤ ((⇑L.basis : (a : Fin 2) → ℂ) '' (↑{0, 1} : Set (Fin 2))))
⊢ L.lattice = Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ))

Tactic:
rw [lattice, ← Set.image_univ, ← Finset.coe_univ, this]

Premises used: Set.image_univ, Finset.coe_univ, PeriodPair.lattice
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
this : Eq (α := Finset (Fin 2)) Finset.univ {0, 1}
⊢ Eq (α := Submodule ℤ ℂ) (Submodule.span ℤ {L.ω₁, L.ω₂})
    (Submodule.span ℤ ((⇑L.basis : (a : Fin 2) → ℂ) '' (↑{0, 1} : Set (Fin 2))))

Tactic:
simp [Set.image_insert_eq]

Premises used: Set.image_insert_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ DiscreteTopology ↥L.lattice

Tactic:
L.lattice_eq_span_range_basis ▸ inferInstance

Premises used: Eq.rec, inferInstance, Eq.symm, PeriodPair.lattice_eq_span_range_basis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
simp_rw : IsZLattice ℝ (E := ℂ) (Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ)))
⊢ IsZLattice ℝ L.lattice

Tactic:
simp_rw [L.lattice_eq_span_range_basis]

Premises used: PeriodPair.lattice_eq_span_range_basis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ IsZLattice ℝ (E := ℂ) (Submodule.span ℤ (Set.range (ι := Fin 2) (⇑L.basis : (a : Fin 2) → ℂ)))

Tactic:
infer_instance
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ IsClosed (↑L.lattice : Set ℂ)

Tactic:
@AddSubgroup.isClosed_of_discrete _ _ _ _ _ L.lattice.toAddSubgroup
    (inferInstanceAs (DiscreteTopology L.lattice))

Premises used: AddSubgroup.isClosed_of_discrete
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
⊢ IsClosed
    (Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
      (Subtype.val (p := fun (x : ℂ) ↦ x ∈ L.lattice) ⁻¹' s))

Tactic:
L.isClosed_lattice.isClosedMap_subtype_val _ (isClosed_discrete (α := L.lattice) ((↑) ⁻¹' s))

Premises used: PeriodPair.isClosed_lattice, isClosed_discrete, Set.preimage, IsClosed.isClosedMap_subtype_val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
h :
  s =
    Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
      (Subtype.val (p := fun (x : ℂ) ↦ x ∈ L.lattice) ⁻¹' s)
⊢ IsClosed s

Tactic:
convert!
    L.isClosed_lattice.isClosedMap_subtype_val _ (isClosed_discrete (α := L.lattice) ((↑) ⁻¹' s))

Premises used: PeriodPair.isClosed_lattice, isClosed_discrete, Set.preimage, IsClosed.isClosedMap_subtype_val
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
⊢ s ∩
      Set.range (ι := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) })
        (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ))) =
    Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
      (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)) ⁻¹' s)

Tactic:
Set.image_preimage_eq_inter_range.symm

Premises used: Set.image_preimage_eq_inter_range, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
h :
  s =
    s ∩
      Set.range (ι := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
⊢ s =
    Set.image (α := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))
      (Subtype.val (p := fun (x : ℂ) ↦ x ∈ L.lattice) ⁻¹' s)

Tactic:
convert! Set.image_preimage_eq_inter_range.symm using 1

Premises used: Set.image_preimage_eq_inter_range, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
hs : s ⊆ (↑L.lattice : Set ℂ)
⊢ s =
    s ∩
      Set.range (ι := { x : ℂ // x ∈ (↑L.lattice : Set ℂ) }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ (↑L.lattice : Set ℂ)))

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
s : Set ℂ
⊢ IsOpen ((↑L.lattice : Set ℂ) \ s)ᶜ

Tactic:
(L.isClosed_of_subset_lattice Set.diff_subset).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℂ
⊢ x ∈ ((↑L.lattice : Set ℂ) \ {x})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ ProperSpace ↥L.lattice

Tactic:
.of_isClosed L.isClosed_lattice

Premises used: PeriodPair.isClosed_lattice, ProperSpace.of_isClosed
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
L : PeriodPair
⊢ Submodule.span ℤ (Set.range ![L.ω₁, L.ω₂]) = L.lattice

Tactic:
simp [lattice, Set.pair_comm L.ω₂ L.ω₁]

Premises used: PeriodPair.ω₂, PeriodPair.ω₁, PeriodPair.lattice, Set.pair_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ (↑((L.latticeBasis : (a : Fin 2) → ↥L.lattice) 0) : ℂ) = L.ω₁

Tactic:
simp [latticeBasis]

Premises used: PeriodPair.latticeBasis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ (↑((L.latticeBasis : (a : Fin 2) → ↥L.lattice) 1) : ℂ) = L.ω₂

Tactic:
simp [latticeBasis]

Premises used: PeriodPair.latticeBasis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
⊢ finrank ℤ ↥L.lattice = 2

Tactic:
finrank_eq_card_basis L.latticeBasis

Premises used: Fintype.card, Module.finrank_eq_card_basis, Finset.card, Multiset.card, PeriodPair.latticeBasis
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
x : ℤ × ℤ
⊢ (↑((L.latticeEquivProd.symm : (a : ℤ × ℤ) → ↥L.lattice) x) : ℂ) = (↑x.1 : ℂ) * L.ω₁ + (↑x.2 : ℂ) * L.ω₂

Tactic:
simp [latticeEquivProd, Finsupp.linearCombination]

Premises used: Finsupp.linearCombination, PeriodPair.latticeEquivProd
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
rw :
  ∀ (x : ℂ),
    TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
      (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
⊢ HasSumLocallyUniformly f fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x

Tactic:
rw [hasSumLocallyUniformly_iff_tendstoLocallyUniformly, tendstoLocallyUniformly_iff_filter]

Premises used: hasSumLocallyUniformly_iff_tendstoLocallyUniformly, tendstoLocallyUniformly_iff_filter
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
⊢ 0 < ‖x‖ + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 (‖x‖ + 1)) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
obtain :
  ∀ (r : ℝ) (hr : 0 < r) (hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)),
    TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
      (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)

Tactic:
obtain ⟨r, hr, hr'⟩ : ∃ r, 0 < r ∧ 𝓝 x ≤ 𝓟 (Metric.ball 0 r) :=
    ⟨‖x‖ + 1, by positivity, Filter.le_principal_iff.mpr (Metric.isOpen_ball.mem_nhds (by simp))⟩

Premises used: nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)

Tactic:
.mono_right ?_ hr'

Premises used: TendstoUniformlyOnFilter.mono_right
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
refine :
  TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓟 (Metric.ball 0 r))
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓝 x)

Tactic:
refine .mono_right ?_ hr'
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
rw :
  TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (Metric.ball 0 r)
⊢ TendstoUniformlyOnFilter (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (𝓟 (Metric.ball 0 r))

Tactic:
rw [← tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]

Premises used: tendstoUniformlyOn_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖(↑l : ℂ)‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ↥L.lattice) (x2 : ℂ) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : ℂ) ↦ ∑' (j : ↥L.lattice), f j x) atTop (Metric.ball 0 r)

Tactic:
tendstoUniformlyOn_tsum_of_cofinite_eventually (hu r hr) ?_

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually