harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Localization/Basic.lean
theorem linearMap_compatibleSMul (N₁ N₂) [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁]
    [Module S N₁] [Module R N₂] [Module S N₂] [IsScalarTower R S N₁] [IsScalarTower R S N₂] :
    LinearMap.CompatibleSMul N₁ N₂ S R where
  map_smul f s s'

Proof state:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module S N₁
inst✝³ : Module R N₂
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ f (mk' S r m • s') = mk' S r m • f s'

Tactic:
rw [← (map_units S m).smul_left_cancel]

Result:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module S N₁
inst✝³ : Module R N₂
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module S N₁
inst✝³ : Module R N₂
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s : S
s' : N₁
⊢ f (s • s') = s • f s'

Tactic:
obtain ⟨r, m, rfl⟩ := mk'_surjective M s

Result:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module S N₁
inst✝³ : Module R N₂
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ f (mk' S r m • s') = mk' S r m • f s'

Proof state:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module S N₁
inst✝³ : Module R N₂
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'

Tactic:
simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_add_of_ne {f g : MvPolynomial σ R}
    (h : m.degree f ≠ m.degree g) :
    m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
rw [not_lt, le_iff_eq_or_lt, Classical.or_iff_not_imp_left, EmbeddingLike.apply_eq_iff_eq] at h'

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
rw [add_comm, degree_add_of_lt (h' h), right_eq_sup]

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
by_cases h' : m.degree g ≺[m] m.degree f

Result:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
simp [degree_add_of_lt h', left_eq_sup, le_of_lt h']

Result:
no goals

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Tactic:
simp only [le_of_lt (h' h)]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_eq_lift_iff {a : Cardinal.{u}} :
    (1 : Cardinal) = lift.{v} a ↔ 1 = a

Proof state:
a : Cardinal.{u}
⊢ 1 = lift.{v, u} a ↔ 1 = a

Tactic:
simpa using nat_eq_lift_iff (n := 1)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem ordered_iff {p : Path α} :
    p.Ordered cmp ↔ p.listL.Pairwise (cmpLT cmp) ∧ p.listR.Pairwise (cmpLT cmp) ∧
      ∀ x ∈ p.listL, ∀ y ∈ p.listR, cmpLT cmp x y

Proof state:
α : Type u_1
cmp : α → α → Ordering
p : Path α
⊢ Ordered cmp p ↔
    List.Pairwise (cmpLT cmp) p.listL ∧
      List.Pairwise (cmpLT cmp) p.listR ∧ ∀ (x : α), x ∈ p.listL → ∀ (y : α), y ∈ p.listR → cmpLT cmp x y

Tactic:
induction p with
| root => simp
| left _ _ x _ ih | right _ _ x _ ih => ?_

Result:
case left
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
x : α
r✝ : RBNode α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ Ordered cmp (left c✝ parent✝ x r✝) ↔
    List.Pairwise (cmpLT cmp) (left c✝ parent✝ x r✝).listL ∧
      List.Pairwise (cmpLT cmp) (left c✝ parent✝ x r✝).listR ∧
        ∀ (x_1 : α), x_1 ∈ (left c✝ parent✝ x r✝).listL → ∀ (y : α), y ∈ (left c✝ parent✝ x r✝).listR → cmpLT cmp x_1 y

case right
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ ↔
    List.Pairwise (cmpLT cmp) parent✝.listL ∧
      List.Pairwise (cmpLT cmp) parent✝.listR ∧
        ∀ (x : α), x ∈ parent✝.listL → ∀ (y : α), y ∈ parent✝.listR → cmpLT cmp x y
⊢ Ordered cmp (right c✝ l✝ x parent✝) ↔
    List.Pairwise (cmpLT cmp) (right c✝ l✝ x parent✝).listL ∧
      List.Pairwise (cmpLT cmp) (right c✝ l✝ x parent✝).listR ∧
        ∀ (x_1 : α),
          x_1 ∈ (right c✝ l✝ x parent✝).listL → ∀ (y : α), y ∈ (right c✝ l✝ x parent✝).listR → cmpLT cmp x_1 y
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_right_last {i : Fin (n + 1)} : predAbove i (last (n + 1)) = last n

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ i.predAbove (last (n + 1)) = last n

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.homogeneousHull_mono : Monotone (Ideal.homogeneousHull 𝒜) := fun I J I_le_J => by
  apply Ideal.span_mono
  rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩
  exact ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩

Proof state:
case a.intro.intro.mk
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ ↑(((decompose 𝒜) ↑⟨x, hx⟩) hr1) ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}

Tactic:
exact ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
⊢ homogeneousHull 𝒜 I ≤ homogeneousHull 𝒜 J

Tactic:
apply Ideal.span_mono

Result:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}

Proof state:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}

Tactic:
rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩

Result:
case a.intro.intro.mk
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ ↑(((decompose 𝒜) ↑⟨x, hx⟩) hr1) ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}
-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem isEulerian_iff {u v : V} (p : G.Walk u v) :
    p.IsEulerian ↔ p.IsTrail ∧ ∀ e, e ∈ G.edgeSet → e ∈ p.edges

Proof state:
case mpr.intro
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hl : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian

Tactic:
exact h.isEulerian_of_forall_mem hl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
constructor

Result:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian

Proof state:
case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian

Tactic:
rintro ⟨h, hl⟩

Result:
case mpr.intro
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hl : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian

Proof state:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
intro h

Result:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Proof state:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma eval₂_evalRingHom (x : R) : eval₂ (evalRingHom x) = evalEval x

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = evalEval x x✝

Tactic:
rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ eval₂ (evalRingHom x) = evalEval x

Tactic:
ext1

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = evalEval x x✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : x ^ y = exp (log x * y)

Proof state:
x : ℝ
hx : 0 < x
y : ℝ
⊢ x ^ y = rexp (log x * y)

Tactic:
rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem powerlt_aleph0_le (c : Cardinal) : c ^< ℵ₀ ≤ max c ℵ₀

Proof state:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ c ⊔ ℵ₀

Tactic:
exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

Result:
no goals

Proof state:
c : Cardinal.{u_1}
⊢ c ^< ℵ₀ ≤ c ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ c with h | h

Result:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c ⊔ ℵ₀

case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ c ⊔ ℵ₀

Proof state:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c ⊔ ℵ₀

Tactic:
rw [powerlt_aleph0 h]

Result:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ⊔ ℵ₀

Proof state:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ⊔ ℵ₀

Tactic:
apply le_max_left

Result:
no goals

Proof state:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ c ⊔ ℵ₀

Tactic:
rw [powerlt_le]

Result:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ c ⊔ ℵ₀
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Tactic:
rw [le_floor, Int.cast_zero]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem tendsto_eraseIdx :
    ∀ {n : ℕ} {l : List α}, Tendsto (eraseIdx · n) (𝓝 l) (𝓝 (eraseIdx l n))
  | _, [] => by rw [nhds_nil]; exact tendsto_pure_nhds _ _
  | 0, a::l => by rw [tendsto_cons_iff]; exact tendsto_snd
  | n + 1, a::l => by
    rw [tendsto_cons_iff]
    dsimp [eraseIdx]
    exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ℕ
⊢ Tendsto (fun x => x.eraseIdx x✝) (pure []) (𝓝 ([].eraseIdx x✝))

Tactic:
exact tendsto_pure_nhds _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun x => x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
rw [tendsto_cons_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p => (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun x => x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))

Tactic:
rw [tendsto_cons_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ℕ
⊢ Tendsto (fun x => x.eraseIdx x✝) (𝓝 []) (𝓝 ([].eraseIdx x✝))

Tactic:
rw [nhds_nil]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ℕ
⊢ Tendsto (fun x => x.eraseIdx x✝) (pure []) (𝓝 ([].eraseIdx x✝))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))

Tactic:
exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))

Tactic:
dsimp [eraseIdx]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p => (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
exact tendsto_snd

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) :
    (fun x : ℝ => Complex.exp (-a * x ^ 2)) =o[cocompact ℝ] fun x : ℝ => |x| ^ s

Proof state:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (-a).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

Result:
no goals

Proof state:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x => cexp (-a * ↑x ^ 2)) =o[cocompact ℝ] fun x => |x| ^ s

Tactic:
convert cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1

Result:
case h.e'_7
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x => cexp (-a * ↑x ^ 2)) = fun x => cexp (-a * ↑x ^ 2 + 0 * ↑x)

a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (-a).re < 0

Proof state:
case h.e'_7
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x => cexp (-a * ↑x ^ 2)) = fun x => cexp (-a * ↑x ^ 2 + 0 * ↑x)

Tactic:
simp_rw [zero_mul, add_zero]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem Commute.div_sub_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0)
    (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extChartAt_nhdsWithin_eq_image' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝[s] y) =
      𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x y :=
  map_extend_nhdsWithin_eq_image _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem dvd_iff_normalizedFactors_le_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Proof state:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y → normalizedFactors x ≤ normalizedFactors y

Tactic:
rintro ⟨c, rfl⟩

Result:
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
c : α
hy : x * c ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors (x * c)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y → normalizedFactors x ≤ normalizedFactors y

case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → x ∣ y

Proof state:
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
c : α
hy : x * c ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors (x * c)

Tactic:
simp [hx, right_ne_zero_of_mul hy]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → x ∣ y

Tactic:
rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
  (prod_normalizedFactors hy).dvd_iff_dvd_right]

Result:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_modEq_x2n_sub {n j} (h : j ≤ 2 * n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n] :=
  (le_total j n).elim (xn_modEq_x2n_sub_lem a1) fun jn => by
    have : 2 * n - j + j ≤ n + j

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] :=
  xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rwa [tsub_tsub_cancel_of_le h, add_comm] at t

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j

Tactic:
exact Nat.add_le_add_left jn _

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
let t := xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] :=
  xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ 2 * n - j + j ≤ n + j

Tactic:
rw [tsub_add_cancel_of_le h, two_mul]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
have : 2 * n - j + j ≤ n + j := by
  rw [tsub_add_cancel_of_le h, two_mul]; exact Nat.add_le_add_left jn _

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α β : Type
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)

Tactic:
rfl

Result:
no goals

Proof state:
α β : Type
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ find? p (pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)

Tactic:
simp only [pmap_eq_map_attach, find?_map]

Result:
α β : Type
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_zero (S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).aroots S = 0

Proof state:
T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ aroots 0 S = 0

Tactic:
rw [← C_0, aroots_C]

Result:
no goals