harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U)
    (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) :
    EqOn f g U

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
⊢ EqOn f g U

Tactic:
have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
hfg' : f - g =ᶠ[𝓝 z₀] 0
⊢ EqOn f g U

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
z : E
h : f z = g z
⊢ (f - g) z = 0 z

Tactic:
simp [h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
hfg' : f - g =ᶠ[𝓝 z₀] 0
⊢ EqOn f g U

Tactic:
simpa [sub_eq_zero] using fun z hz =>
  (hf.sub hg).eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀ hfg' hz

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_epi_kernel_lift [S.HasHomology] [HasKernel S.g] :
    S.Exact ↔ Epi (kernel.lift S.g S.f S.zero)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ S.Exact ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
rw [exact_iff_epi_toCycles]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Arrow.mk S.toCycles ≅ Arrow.mk (kernel.lift S.g S.f ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Arrow.mk S.toCycles ≅ Arrow.mk (kernel.lift S.g S.f ⋯)

Tactic:
exact Arrow.isoMk (Iso.refl _) S.cyclesIsoKernel (by aesop_cat)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ (Iso.refl (Arrow.mk S.toCycles).left).hom ≫ (Arrow.mk (kernel.lift S.g S.f ⋯)).hom =
    (Arrow.mk S.toCycles).hom ≫ S.cyclesIsoKernel.hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_subset_Icc (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) : [[a₁, b₁]] ⊆ Icc a₂ b₂

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
rw [mem_Icc] at ha hb

Result:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_iff_lt_rowLen {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ ↔ j < μ.rowLen i

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ

Tactic:
push_neg

Result:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ

Tactic:
exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩

Result:
no goals

Proof state:
μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x✝ : ℕ
hmj : x✝ ≤ j
⊢ i ≤ i

Tactic:
rfl

Result:
no goals

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ j < μ.rowLen i

Tactic:
rw [rowLen, Nat.lt_find_iff]

Result:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ

Proof state:
μ : YoungDiagram
i j : ℕ
h : ∀ m ≤ j, (i, m) ∈ μ
⊢ j ≤ j

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The coheight of an element is infinite iff there exist series of arbitrary length ending in that
element.
-/
lemma coheight_eq_top_iff {x : α} :
    coheight x = ⊤ ↔ ∀ n, ∃ p : LTSeries α, p.head = x ∧ p.length = n

Proof state:
case h.e'_2.h.a.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.last p = x ∧ p.length = n) → ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
intro ⟨p, hp, hl⟩

Result:
case h.e'_2.h.a.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ ∃ p, RelSeries.head p = x ∧ p.length = n

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x ∧ (RelSeries.reverse p).length = n

Tactic:
constructor <;> simpa

Result:
no goals

Proof state:
case h.e'_2.h.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) ↔ ∃ p, RelSeries.last p = x ∧ p.length = n

Tactic:
constructor <;> (intro ⟨p, hp, hl⟩; use p.reverse; constructor <;> simpa)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ coheight x = ⊤ ↔ ∀ (n : ℕ), ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
convert height_eq_top_iff (α := αᵒᵈ) (x := x) using 2 with n

Result:
case h.e'_2.h.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) ↔ ∃ p, RelSeries.last p = x ∧ p.length = n

Proof state:
case h.e'_2.h.a.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
use p.reverse

Result:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x ∧ (RelSeries.reverse p).length = n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Vector α n} {l₂ : Vector β n} {z : γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = some z ↔
      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
l₂ : Vector β n
z : γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } l₂)[i]? = some z ↔
    ∃ x y, { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
z : γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
          { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
      some z ↔
    ∃ x y,
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]? = some x ∧
        { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? = some y ∧ f x y = z

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
z : γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
          { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
      some z ↔
    ∃ x y,
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]? = some x ∧
        { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? = some y ∧ f x y = z

Tactic:
simp [Array.getElem?_zipWith_eq_some]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
l₁ : Vector α n
l₂ : Vector β n
z : γ
i : Nat
⊢ (zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
l₂ : Vector β n
z : γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } l₂)[i]? = some z ↔
    ∃ x y, { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
-- Mathlib/Data/Fin/Basic.lean
theorem cast_inj (eq : n = m) {a b : Fin n} : a.cast eq = b.cast eq ↔ a = b

Proof state:
n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a = Fin.cast eq b ↔ a = b

Tactic:
simp [← val_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_deriv_comp_mul_deriv {f f' g g' : ℝ → ℝ}
    (hf : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
    (hg : ∀ x ∈ uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (uIcc a b))
    (hg' : Continuous g') : (∫ x in a..b, (g' ∘ f) x * f' x) = (g ∘ f) b - (g ∘ f) a

Proof state:
a b : ℝ
f f' g g' : ℝ → ℝ
hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)
hf' : ContinuousOn f' [[a, b]]
hg' : Continuous g'
⊢ ∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a

Tactic:
simpa [mul_comm] using integral_deriv_comp_smul_deriv hf hg hf' hg'

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isNat_rpow_pos {a b : ℝ} {nb ne : ℕ}
    (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) :
    IsNat (a ^ b) ne

Proof state:
a b : ℝ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, rpow_natCast]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_div_const_uIcc (ha : a ≠ 0) (b c : α) :
    (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]

Tactic:
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem HasBasis.pi_self {α : Type*} {κ : Type*} {f : Filter α} {p : κ → Prop} {s : κ → Set α}
    (h : f.HasBasis p s) :
    (pi fun _ ↦ f).HasBasis (fun Ik : Set ι × κ ↦ Ik.1.Finite ∧ p Ik.2)
      (fun Ik ↦ Ik.1.pi (fun _ ↦ s Ik.2))

Proof state:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Tactic:
rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi))
  with ⟨k₀, hk₀, hk₀'⟩

Result:
case intro.intro
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
k₀ : κ
hk₀ : p k₀
hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Proof state:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
⊢ (pi fun x => f).HasBasis (fun Ik => Ik.1.Finite ∧ p Ik.2) fun Ik => Ik.1.pi fun x => s Ik.2

Tactic:
refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)

Result:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Proof state:
case intro.intro
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
k₀ : κ
hk₀ : p k₀
hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Tactic:
exact ⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem IsLUB.nonempty [NoMinOrder α] (hs : IsLUB s a) : s.Nonempty :=
  let ⟨a', ha'⟩ := exists_lt a
  nonempty_iff_ne_empty.2 fun h =>
    not_le_of_lt ha' <| hs.right <| by rw [h, upperBounds_empty]; exact mem_univ _

Proof state:
α : Type u
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ upperBounds s

Tactic:
rw [h, upperBounds_empty]

Result:
α : Type u
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ

Proof state:
α : Type u
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ

Tactic:
exact mem_univ _

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem add_eq_right_iff_mul_omega0_le {a b : Ordinal} : a + b = b ↔ a * ω ≤ b

Proof state:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b

Tactic:
nth_rw 1 [← this]

Result:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Proof state:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

Tactic:
rw [← nfp_add_zero a, ← deriv_zero_right]

Result:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x => a + x) 0 ≤ b

Proof state:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Tactic:
rwa [← add_assoc, ← mul_one_add, one_add_omega0]

Result:
no goals

Proof state:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b

Tactic:
have := Ordinal.add_sub_cancel_of_le h

Result:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b

Proof state:
a b : Ordinal.{u_1}
⊢ a + b = b ↔ a * ω ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b

Proof state:
case refine_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x => a + x) c = b
⊢ deriv (fun x => a + x) 0 ≤ deriv (fun x => a + x) c

Tactic:
exact (isNormal_deriv _).monotone (Ordinal.zero_le _)

Result:
no goals

Proof state:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x => a + x) 0 ≤ b

Tactic:
obtain ⟨c, hc⟩ := (isNormal_add_right a).fp_iff_deriv.1 h

Result:
case refine_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x => a + x) c = b
⊢ deriv (fun x => a + x) 0 ≤ b

Proof state:
case refine_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x => a + x) c = b
⊢ deriv (fun x => a + x) 0 ≤ b

Tactic:
rw [← hc]

Result:
case refine_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x => a + x) c = b
⊢ deriv (fun x => a + x) 0 ≤ deriv (fun x => a + x) c
-- Mathlib/RingTheory/Filtration.lean
theorem stable_iff_exists_pow_smul_eq_of_ge :
    F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ n + 1 ≥ h.choose

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
refine ⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n hn => ?_⟩⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ I • F.N n = F.N (n + 1)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ I • F.N n = F.N (n + 1)

Tactic:
rw [h.choose_spec n hn, h.choose_spec (n + 1) (by omega), smul_smul, ← pow_succ',
  tsub_add_eq_add_tsub hn]

Result:
no goals
-- Mathlib/NumberTheory/PrimeCounting.lean
theorem tendsto_primeCounting' : Tendsto π' atTop atTop

Proof state:
⊢ ¬BddAbove (Set.range π')

Tactic:
simp [Set.range_eq_univ.mpr surjective_primeCounting']

Result:
no goals

Proof state:
⊢ Tendsto π' atTop atTop

Tactic:
apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'

Result:
⊢ ¬BddAbove (Set.range π')
-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem ae_differentiableWithinAt_of_mem {f : E → F} (hf : LipschitzOnWith C f s) :
    ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
H : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : E
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
have : f = (A.symm ∘ A) ∘ f := by
  simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]

Result:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
H : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : E
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ f s x

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_pi

Result:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ LipschitzOnWith ?C (⇑A ∘ f) s

case C
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ ℝ≥0
-- Mathlib/RingTheory/Artinian/Module.lean
theorem isArtinian_iff_submodule_quotient (S : Submodule R P) :
    IsArtinian R P ↔ IsArtinian R S ∧ IsArtinian R (P ⧸ S)

Proof state:
R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
⊢ IsArtinian R P ↔ IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩

Result:
R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)
left✝ : IsArtinian R ↥S
right✝ : IsArtinian R (P ⧸ S)
⊢ IsArtinian R P

Proof state:
R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)
left✝ : IsArtinian R ↥S
right✝ : IsArtinian R (P ⧸ S)
⊢ IsArtinian R P

Tactic:
apply isArtinian_of_range_eq_ker S.subtype S.mkQ

Result:
R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)
left✝ : IsArtinian R ↥S
right✝ : IsArtinian R (P ⧸ S)
⊢ LinearMap.range S.subtype = LinearMap.ker S.mkQ

Proof state:
R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)
left✝ : IsArtinian R ↥S
right✝ : IsArtinian R (P ⧸ S)
⊢ LinearMap.range S.subtype = LinearMap.ker S.mkQ

Tactic:
rw [Submodule.ker_mkQ, Submodule.range_subtype]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
lemma rootMultiplicity_add {p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
    min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ (X - C a) ^ (rootMultiplicity a p ⊓ rootMultiplicity a q) ∣ p + q

Tactic:
exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ rootMultiplicity a p ⊓ rootMultiplicity a q ≤ rootMultiplicity a (p + q)

Tactic:
rw [le_rootMultiplicity_iff hzero]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ (X - C a) ^ (rootMultiplicity a p ⊓ rootMultiplicity a q) ∣ p + q
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem map_comp {f : S ⟶ S'} {f' : S' ⟶ S''} {h : StructuredArrow S'' T} :
    (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)

Tactic:
rw [eq_mk h]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ filterMap (some ∘ f) l = map f l

Tactic:
induction l <;> simp [*, filterMap_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ filterMap (some ∘ f) = map f

Tactic:
funext l

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ filterMap (some ∘ f) l = map f l