harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/Hyperreal.lean
theorem st_eq_sSup {x : ℝ*} : st x = sSup { y : ℝ | (y : ℝ*) < x }

Proof state:
x : ℝ*
⊢ x.st = sSup {y | ↑y < x}

Tactic:
rcases _root_.em (Infinite x) with (hx|hx)

Result:
case inl
x : ℝ*
hx : x.Infinite
⊢ x.st = sSup {y | ↑y < x}

case inr
x : ℝ*
hx : ¬x.Infinite
⊢ x.st = sSup {y | ↑y < x}

Proof state:
case inl.inr
x : ℝ*
hx : x.InfiniteNeg
⊢ 0 = sSup {y | ↑y < x}

Tactic:
convert Real.sSup_empty.symm

Result:
case h.e'_3.h.e'_3
x : ℝ*
hx : x.InfiniteNeg
⊢ {y | ↑y < x} = ∅

Proof state:
case h.e'_3.h.e'_3
x : ℝ*
hx : x.InfiniteNeg
⊢ {y | ↑y < x} = ∅

Tactic:
exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)

Result:
no goals

Proof state:
case inr
x : ℝ*
hx : ¬x.Infinite
⊢ x.st = sSup {y | ↑y < x}

Tactic:
exact (isSt_sSup hx).st_eq

Result:
no goals

Proof state:
case inl
x : ℝ*
hx : x.Infinite
⊢ x.st = sSup {y | ↑y < x}

Tactic:
rw [hx.st_eq]

Result:
case inl
x : ℝ*
hx : x.Infinite
⊢ 0 = sSup {y | ↑y < x}

Proof state:
case inl
x : ℝ*
hx : x.Infinite
⊢ 0 = sSup {y | ↑y < x}

Tactic:
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
x : ℝ*
hx : x.InfinitePos
⊢ {y | ↑y < x} = Set.univ

Tactic:
exact Set.eq_univ_of_forall hx

Result:
no goals

Proof state:
case inl.inl
x : ℝ*
hx : x.InfinitePos
⊢ 0 = sSup {y | ↑y < x}

Tactic:
convert Real.sSup_univ.symm

Result:
case h.e'_3.h.e'_3
x : ℝ*
hx : x.InfinitePos
⊢ {y | ↑y < x} = Set.univ
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.rotateL {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateL l x r)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateL x r).Sized

Tactic:
cases r

Result:
case nil
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : nil.Sized
⊢ (l.rotateL x nil).Sized

case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Tactic:
rw [Ordnode.rotateL_node]

Result:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).Sized

Tactic:
exact hl.node3L hr.2.1 hr.2.2

Result:
no goals

Proof state:
case nil
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : nil.Sized
⊢ (l.rotateL x nil).Sized

Tactic:
exact hl.node' hr

Result:
no goals

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized

Tactic:
split_ifs

Result:
case pos
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).Sized

case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized

Proof state:
case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized

Tactic:
exact hl.node4L hr.2.1 hr.2.2

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongr_apply_apply (f : ∀ a, W a) (a : α) : h₁.piCongr h₂ f (h₁ a) = h₂ a (f a)

Proof state:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)

Tactic:
simp only [piCongr, piCongrRight, trans_apply, coe_fn_mk, piCongrLeft_apply_apply, Pi.map_apply]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem cons_bagInter_of_pos (l₁ : List α) (h : a ∈ l₂) :
    (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Proof state:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ []
⊢ (a :: l₁).bagInter [] = a :: l₁.bagInter ([].erase a)

Tactic:
exact if_pos h

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = a :: l₁.bagInter ((head✝ :: tail✝).erase a)

Tactic:
simp only [List.bagInter, if_pos (elem_eq_true_of_mem h)]

Result:
no goals

Proof state:
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
cases l₂

Result:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ []
⊢ (a :: l₁).bagInter [] = a :: l₁.bagInter ([].erase a)

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = a :: l₁.bagInter ((head✝ :: tail✝).erase a)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_dvd_iff_dvd_coeff (r : R) (φ : MvPolynomial σ R) : C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
constructor

Result:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ

Proof state:
case mp.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ

Tactic:
apply dvd_mul_right

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
lemma equicontinuousAt_restrict_iff (F : ι → X → α) {S : Set X} (x₀ : S) :
    EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : ↑S
⊢ EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S ↑x₀

Tactic:
simp [EquicontinuousWithinAt, EquicontinuousAt,
  ← eventually_nhds_subtype_iff]

Result:
no goals
-- Mathlib/Data/Set/MemPartition.lean
lemma memPartitionSet_mem (f : ℕ → Set α) (n : ℕ) (a : α) :
    memPartitionSet f n a ∈ memPartition f n

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)

Tactic:
classical
rw [memPartitionSet_succ, memPartition_succ]
refine ⟨memPartitionSet f n a, ?_⟩
split_ifs <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ memPartitionSet f n a ∈ memPartition f n

Tactic:
induction n with
| zero => simp [memPartitionSet]
| succ n ih =>
  classical
  rw [memPartitionSet_succ, memPartition_succ]
  refine ⟨memPartitionSet f n a, ?_⟩
  split_ifs <;> simp [ih]

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)

Tactic:
split_ifs <;> simp [ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a ∈ memPartition f 0

Tactic:
simp [memPartitionSet]

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈
    {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Tactic:
refine ⟨memPartitionSet f n a, ?_⟩

Result:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)

Tactic:
rw [memPartitionSet_succ, memPartition_succ]

Result:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈
    {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
private lemma A_subset_aH (a : G) (ha : a ∈ A) : A ⊆ a • (A⁻¹ * A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ 1 ∈ a •> A⁻¹

Tactic:
simp [← inv_smul_mem_iff, inv_mem_inv ha]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> (A⁻¹ * A)

Tactic:
rw [← smul_mul_assoc]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A

Tactic:
exact subset_mul_right _ (by simp [← inv_smul_mem_iff, inv_mem_inv ha])

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y

Proof state:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ x <* y = const β <$> x <*> y

Tactic:
show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y

Result:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let a ← x
      let _ ← y
      pure a) =
    do
    let f ← const β <$> x
    f <$> y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x

Proof state:
α : Type u_1
β : Type u_2
ε : Sort u_3
γ : Type u_4
δ : Type u_5
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
x : α ⊕ γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.inverse_comp_of_right {g : M₂ →L[R] M₃} {f : M →L[R] M₂}
    (hf : f.IsInvertible) : (g ∘L f).inverse = f.inverse ∘L g.inverse

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (g.comp f).inverse = f.inverse.comp g.inverse

Tactic:
rcases hf with ⟨M, rfl⟩

Result:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (g.comp ↑M).inverse = (↑M).inverse.comp g.inverse

Proof state:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (g.comp ↑M).inverse = (↑M).inverse.comp g.inverse

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem le_comap_mkQ (p' : Submodule R (M ⧸ p)) : p ≤ comap p.mkQ p'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap p.mkQ p'

Tactic:
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
theorem iSupLift_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
    {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
    {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : K i) (h : K i ≤ T) :
    iSupLift K dir f hf T hT (inclusion h x) = f i x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x

Tactic:
dsimp [iSupLift, inclusion]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ (Set.inclusion h x) = (f i) x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ (Set.inclusion h x) = (f i) x

Tactic:
rw [Set.iUnionLift_inclusion]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem apply_eq_zero_of_not_le_supDegree {p : R[A]} {a : A} (hlt : ¬ D a ≤ p.supDegree D) :
    p a = 0

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
p : R[A]
a : A
hlt : ¬D a ≤ supDegree D p
⊢ p a = 0

Tactic:
contrapose! hlt

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
p : R[A]
a : A
hlt : p a ≠ 0
⊢ D a ≤ supDegree D p

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
p : R[A]
a : A
hlt : p a ≠ 0
⊢ D a ≤ supDegree D p

Tactic:
exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
lemma summable_norm_eisSummand {k : ℤ} (hk : 3 ≤ k) (z : ℍ) :
    Summable fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ ‖eisSummand k b z‖ ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Tactic:
simp only [eisSummand, norm_zpow]

Result:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ ‖↑(b 0) * ↑z + ↑(b 1)‖ ^ (-k) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ 0 ≤ ↑k

Tactic:
positivity

Result:
no goals

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ Summable fun x => ‖eisSummand k x z‖

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast

Result:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ Summable fun x => ‖eisSummand k x z‖

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ Summable fun x => ‖eisSummand k x z‖

Tactic:
apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le
  (fun _ ↦ norm_nonneg _)

Result:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ ∀ (b : Fin 2 → ℤ), ‖eisSummand k b z‖ ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ ∀ (b : Fin 2 → ℤ), ‖eisSummand k b z‖ ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Tactic:
intro b

Result:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ ‖eisSummand k b z‖ ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ 2 < ↑k

Tactic:
norm_cast

Result:
no goals

Proof state:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ ‖↑(b 0) * ↑z + ↑(b 1)‖ ^ (-k) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Tactic:
exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_go_succ {p : α → Bool} {xs : List α} {i : Nat} :
    findIdx?.go p xs (i+1) = (findIdx?.go p xs i).map fun i => i + 1

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
⊢ findIdx?.go p xs (i + 1) = Option.map (fun i => i + 1) (findIdx?.go p xs i)

Tactic:
induction xs generalizing i with simp
| cons _ _ _ => split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun i => i + 1) (findIdx?.go p tail✝ i)
i : Nat
⊢ (if p head✝ = true then some (i + 1) else findIdx?.go p tail✝ (i + 1 + 1)) =
    Option.map (fun i => i + 1) (if p head✝ = true then some i else findIdx?.go p tail✝ (i + 1))

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toReal_mul {x y : EReal} : toReal (x * y) = toReal x * toReal y

Proof state:
case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ (↑x✝ * ⊥).toReal = (↑x✝).toReal * ⊥.toReal

Tactic:
simp [coe_mul_bot_of_neg h]

Result:
no goals

Proof state:
x y : EReal
⊢ (x * y).toReal = x.toReal * y.toReal

Tactic:
induction x, y using induction₂_symm with
| top_zero | zero_bot | top_top | top_bot | bot_bot => simp
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => norm_cast
| top_pos _ h => simp [top_mul_coe_of_pos h]
| top_neg _ h => simp [top_mul_coe_of_neg h]
| pos_bot _ h => simp [coe_mul_bot_of_pos h]
| neg_bot _ h => simp [coe_mul_bot_of_neg h]

Result:
no goals

Proof state:
case coe_coe
x✝ y✝ : ℝ
⊢ (↑x✝ * ↑y✝).toReal = (↑x✝).toReal * (↑y✝).toReal

Tactic:
norm_cast

Result:
no goals

Proof state:
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝ * ⊥).toReal = (↑x✝).toReal * ⊥.toReal

Tactic:
simp [coe_mul_bot_of_pos h]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (⊤ * ↑x✝).toReal = ⊤.toReal * (↑x✝).toReal

Tactic:
simp [top_mul_coe_of_pos h]

Result:
no goals

Proof state:
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ (⊤ * ↑x✝).toReal = ⊤.toReal * (↑x✝).toReal

Tactic:
simp [top_mul_coe_of_neg h]

Result:
no goals

Proof state:
case bot_bot

⊢ (⊥ * ⊥).toReal = ⊥.toReal * ⊥.toReal

Tactic:
simp

Result:
no goals

Proof state:
case symm
x✝ y✝ : EReal
h : (x✝ * y✝).toReal = x✝.toReal * y✝.toReal
⊢ (y✝ * x✝).toReal = y✝.toReal * x✝.toReal

Tactic:
rwa [mul_comm, EReal.mul_comm]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem sumCongr_refl {α β} :
    Equiv.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)

Proof state:
case H
α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) i = (Equiv.refl (α ⊕ β)) i

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
α : Type u_9
β : Type u_10
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
ext i

Result:
case H
α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) i = (Equiv.refl (α ⊕ β)) i
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem tendsto_residual_of_isOpenMap (hc : Continuous f) (ho : IsOpenMap f) :
    Tendsto f (residual α) (residual β)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
t : Set β
ht : IsOpen t
htd : Dense t
⊢ t ∈ (map f (residual α)).sets

Tactic:
exact residual_of_dense_open (ht.preimage hc) (htd.preimage ho)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
⊢ Tendsto f (residual α) (residual β)

Tactic:
apply le_countableGenerate_iff_of_countableInterFilter.mpr

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
⊢ {t | IsOpen t ∧ Dense t} ⊆ (map f (residual α)).sets

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
⊢ {t | IsOpen t ∧ Dense t} ⊆ (map f (residual α)).sets

Tactic:
rintro t ⟨ht, htd⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
t : Set β
ht : IsOpen t
htd : Dense t
⊢ t ∈ (map f (residual α)).sets
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k

Proof state:
case H0
m k : Nat
⊢ (m * 0).gcd (m * k) = m * gcd 0 k

Tactic:
simp

Result:
no goals

Proof state:
m n k : Nat
⊢ (m * n).gcd (m * k) = m * n.gcd k

Tactic:
induction n, k using gcd.induction with
| H0 k => simp
| H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH

Result:
no goals

Proof state:
case H1
m n k : Nat
a✝ : 0 < n
IH : (m * (k % n)).gcd (m * n) = m * (k % n).gcd n
⊢ (m * n).gcd (m * k) = m * n.gcd k

Tactic:
rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
/-- `eqToHom h` is heterogeneously equal to the identity of its domain. -/
lemma eqToHom_heq_id_dom (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 X)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ HEq (eqToHom ⋯) (𝟙 X)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ HEq (eqToHom h) (𝟙 X)

Tactic:
subst h

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ HEq (eqToHom ⋯) (𝟙 X)
-- Mathlib/Data/Finset/Prod.lean
theorem diag_insert : (insert a s).diag = insert (a, a) s.diag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).diag = insert (a, a) s.diag

Tactic:
rw [insert_eq, insert_eq, diag_union, diag_singleton]

Result:
no goals