harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Prod.lean
theorem snd_map_snd : (Submodule.snd R M M₂).map (LinearMap.snd R M M₂) = ⊤

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.snd R M M₂) (snd R M M₂) = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ map (LinearMap.snd R M M₂) (snd R M M₂)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M₂
⊢ x ∈ map (LinearMap.snd R M M₂) (snd R M M₂)

Tactic:
simp only [snd, comap_bot, mem_map, mem_ker, snd_apply, fst_apply,
  Prod.exists, exists_eq_right, exists_eq]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ map (LinearMap.snd R M M₂) (snd R M M₂)

Tactic:
rintro x -

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M₂
⊢ x ∈ map (LinearMap.snd R M M₂) (snd R M M₂)
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem induction {p : Multiset α → Prop} (empty : p 0)
    (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : ∀ s, p s

Proof state:
case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)

Tactic:
induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih

Result:
no goals

Proof state:
case mk.cons
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
head✝ : α
tail✝ : List α
ih : p (Quot.mk (⇑(isSetoid α)) tail✝)
⊢ p (Quot.mk (⇑(isSetoid α)) (head✝ :: tail✝))

Tactic:
exact cons _ _ ih

Result:
no goals

Proof state:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s

Tactic:
rintro ⟨l⟩

Result:
case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)

Proof state:
case mk.nil
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
⊢ p (Quot.mk ⇑(isSetoid α) [])

Tactic:
exact empty

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
    Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
use x

Result:
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
use max x (x + dy)

Result:
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ x ⊔ (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)

Proof state:
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ x ⊔ (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
rcases lt_or_le x y with h' | h'

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Proof state:
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*, not_le.2 h']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_range_of_injective {f : α → β} (hf : Injective f) :
    Nat.card (range f) = Nat.card α

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(f ⁻¹' range f) = Nat.card α

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(range f) = Nat.card α

Tactic:
rw [← Nat.card_preimage_of_injective hf le_rfl]

Result:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(f ⁻¹' range f) = Nat.card α
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_δ₀' (i : Δ' ⟶ Δ) [Mono i] (hi : Isδ₀ i) : mapMono K i = K.d Δ.len Δ'.len

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len

Tactic:
simp only [dif_neg this, dif_pos hi]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = K.d Δ.len Δ'.len

Tactic:
unfold mapMono

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len

Tactic:
suffices Δ ≠ Δ' by
  simp only [dif_neg this, dif_pos hi]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'

Tactic:
rintro rfl

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False

Tactic:
simpa only [self_eq_add_right, Nat.one_ne_zero] using hi.1

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_ofLE {Y Z : C} {P Q : Subobject Y} {f : Z ⟶ Y} (h : P ≤ Q) (w : P.Factors f) :
    Q.factorThru f (factors_of_le f h w) = P.factorThru f w ≫ ofLE P Q h

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ = P.factorThru f w ≫ P.ofLE Q h

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem Monotone.ciSup_mem_iInter_Icc_of_antitone [SemilatticeSup β] {f g : β → α} (hf : Monotone f)
    (hg : Antitone g) (h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ ⨆ n, f n ∈ ⋂ n, Icc (f n) (g n)

Tactic:
refine mem_iInter.2 fun n => ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this✝ : Nonempty β
this : ∀ (m : β), f m ≤ g n
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Tactic:
exact ⟨le_ciSup ⟨g <| n, forall_mem_range.2 this⟩ _, ciSup_le this⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Tactic:
have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n

Result:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this✝ : Nonempty β
this : ∀ (m : β), f m ≤ g n
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Tactic:
haveI : Nonempty β := ⟨n⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem IsAcc.isLimit {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : IsLimit o

Proof state:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o.IsLimit

Tactic:
refine isLimit_of_not_succ_of_ne_zero (fun ⟨x, hx⟩ ↦ ?_) h.1

Result:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x✝ : ∃ a, o = succ a
x : Ordinal.{u_1}
hx : o = succ x
⊢ False

Proof state:
case intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x✝ : ∃ a, o = succ a
x : Ordinal.{u_1}
hx : o = succ x
p : Ordinal.{u_1}
hp : p ∈ S ∩ Ioo x o
⊢ False

Tactic:
exact (hx.symm ▸ (succ_le_iff.mpr hp.2.1)).not_lt hp.2.2

Result:
no goals

Proof state:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x✝ : ∃ a, o = succ a
x : Ordinal.{u_1}
hx : o = succ x
⊢ False

Tactic:
rcases h.2 x (lt_of_lt_of_le (lt_succ x) hx.symm.le) with ⟨p, hp⟩

Result:
case intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x✝ : ∃ a, o = succ a
x : Ordinal.{u_1}
hx : o = succ x
p : Ordinal.{u_1}
hp : p ∈ S ∩ Ioo x o
⊢ False

Proof state:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o.IsAcc S
⊢ o.IsLimit

Tactic:
rw [isAcc_iff] at h

Result:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o.IsLimit
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem rnDeriv_sub (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] [hst : (s - t).HaveLebesgueDecomposition μ] :
    (s - t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ - t.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg]

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
⊢ (s + -t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + -t.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
hst : (s - t).HaveLebesgueDecomposition μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ

Tactic:
rw [sub_eq_add_neg] at hst

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
⊢ (s + -t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + -t.rnDeriv μ

Tactic:
exact ae_eq_trans (rnDeriv_add _ _ _) (Filter.EventuallyEq.add (ae_eq_refl _) (rnDeriv_neg _ _))

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_pow (A : Matrix n n α) (k : ℕ) : adjugate (A ^ k) = adjugate A ^ k

Proof state:
case zero
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (A ^ 0).adjugate = A.adjugate ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)

Tactic:
rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
⊢ (A ^ k).adjugate = A.adjugate ^ k

Tactic:
induction k with
| zero => simp
| succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
/-- Variant of `eisensteinSeries_tendstoLocallyUniformly` formulated with maps `ℂ → ℂ`, which is
nice to have for holomorphicity later. -/
lemma eisensteinSeries_tendstoLocallyUniformlyOn {k : ℤ} {N : ℕ} (hk : 3 ≤ k)
    (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N a )) ↦
      ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z)) (↑ₕ(eisensteinSeries_SIF a k).toFun)
          Filter.atTop {z : ℂ | 0 < z.im}

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MapsTo (↑(IsOpenEmbedding.toPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm)
    (IsOpenEmbedding.toPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤

Tactic:
simp only [IsOpenEmbedding.toPartialHomeomorph_target, Set.top_eq_univ, mapsTo_range_iff,
Set.mem_univ, forall_const]

Result:
no goals

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (fun n z => ∑ x ∈ n, eisSummand k (↑x) z) (⇑(eisensteinSeries_SIF a k)) Filter.atTop

Tactic:
apply eisensteinSeries_tendstoLocallyUniformly hk

Result:
no goals

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun n z => ∑ x ∈ n, eisSummand k (↑x) z) (eisensteinSeries_SIF a k).toFun Filter.atTop ⊤

Tactic:
simp only [SlashInvariantForm.toFun_eq_coe, Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (fun n z => ∑ x ∈ n, eisSummand k (↑x) z) (⇑(eisensteinSeries_SIF a k)) Filter.atTop

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s => (fun z => ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    ((eisensteinSeries_SIF a k).toFun ∘ ↑ofComplex) Filter.atTop (Subtype.val '' Set.univ)

Tactic:
apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (PartialHomeomorph.continuousOn_symm _)

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun n z => ∑ x ∈ n, eisSummand k (↑x) z) (eisensteinSeries_SIF a k).toFun Filter.atTop ⊤

k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MapsTo (↑(IsOpenEmbedding.toPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm)
    (IsOpenEmbedding.toPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s => (fun z => ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    ((eisensteinSeries_SIF a k).toFun ∘ ↑ofComplex) Filter.atTop {z | 0 < z.im}

Tactic:
rw [← Subtype.coe_image_univ {z : ℂ | 0 < z.im}]

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s => (fun z => ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    ((eisensteinSeries_SIF a k).toFun ∘ ↑ofComplex) Filter.atTop (Subtype.val '' Set.univ)
-- Mathlib/GroupTheory/PGroup.lean
theorem nonempty_fixed_point_of_prime_not_dvd_card (α) [MulAction G α] (hpα : ¬p ∣ Nat.card α) :
    (fixedPoints G α).Nonempty :=
  have : Finite α := Nat.finite_of_card_ne_zero (fun h ↦ (h ▸ hpα) (dvd_zero p))
  @Set.Nonempty.of_subtype _ _
    (by
      rw [← Finite.card_pos_iff, pos_iff_ne_zero]
      contrapose! hpα
      rw [← Nat.modEq_zero_iff_dvd, ← hpα]
      exact hG.card_modEq_card_fixedPoints α)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ p ∣ Nat.card α

Tactic:
rw [← Nat.modEq_zero_iff_dvd, ← hpα]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
exact hG.card_modEq_card_fixedPoints α

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nat.card ↑(fixedPoints G α) ≠ 0

Tactic:
contrapose! hpα

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ p ∣ Nat.card α

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nonempty ↑(fixedPoints G α)

Tactic:
rw [← Finite.card_pos_iff, pos_iff_ne_zero]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nat.card ↑(fixedPoints G α) ≠ 0
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Proof state:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ p.degree + (X ^ (n - m)).degree ≤ ↑n

Tactic:
refine le_trans (add_le_add hpdeg (degree_X_pow_le _)) ?_

Result:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ↑m + ↑(n - m) ≤ ↑n

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p ∈ I, p.degree ≤ ↑m ∧ p.leadingCoeff = r
⊢ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = r

Tactic:
rcases hr with ⟨p, hpI, hpdeg, rfl⟩

Result:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.leadingCoeff

Proof state:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ↑m + ↑(n - m) ≤ ↑n

Tactic:
rw [← Nat.cast_add, add_tsub_cancel_of_le H]

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.leadingCoeff

Tactic:
refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩

Result:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ (p * X ^ (n - m)).degree ≤ ↑n

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
⊢ I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Tactic:
intro r hr

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ I.leadingCoeffNth m
⊢ r ∈ I.leadingCoeffNth n

Proof state:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ (p * X ^ (n - m)).degree ≤ ↑n

Tactic:
refine le_trans (degree_mul_le _ _) ?_

Result:
case intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ p.degree + (X ^ (n - m)).degree ≤ ↑n

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ I.leadingCoeffNth m
⊢ r ∈ I.leadingCoeffNth n

Tactic:
simp only [SetLike.mem_coe, mem_leadingCoeffNth] at hr ⊢

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p ∈ I, p.degree ≤ ↑m ∧ p.leadingCoeff = r
⊢ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = r
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_zero_of_mem (h : x ∈ s) : infDist x s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∈ s
⊢ infDist x s = 0

Tactic:
simp [infEdist_zero_of_mem h, infDist]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
@[simp]
lemma ofSection_le_iff (G : Subpresheaf F) :
    ofSection x ≤ G ↔ x ∈ G.obj X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
⊢ ofSection x ≤ G ↔ x ∈ G.obj X

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
⊢ ofSection x ≤ G → x ∈ G.obj X

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
⊢ x ∈ G.obj X → ofSection x ≤ G

Proof state:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
hx : x ∈ G.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ F.map f x ∈ G.obj U

Tactic:
exact G.map f hx

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
hx : ofSection x ≤ G
⊢ x ∈ G.obj X

Tactic:
exact hx _ (mem_ofSection_obj x)

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
⊢ x ∈ G.obj X → ofSection x ≤ G

Tactic:
rintro hx U _ ⟨f, rfl⟩

Result:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
hx : x ∈ G.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ F.map f x ∈ G.obj U

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
⊢ ofSection x ≤ G → x ∈ G.obj X

Tactic:
intro hx

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subpresheaf F
hx : ofSection x ≤ G
⊢ x ∈ G.obj X