harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Irreducible.lean
theorem infPrime_iff_not_isMax : InfPrime a ↔ ¬IsMax a :=
  and_iff_left <| by simp

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem aeSeq_eq_fun_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α}
    (hx : x ∈ aeSeqSet hf p) (i : ι) : aeSeq hf p i x = f i x

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = f i x

Tactic:
simp only [aeSeq_eq_mk_of_mem_aeSeqSet hf hx i, mk_eq_fun_of_mem_aeSeqSet hf hx i]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsAdjointPair.comp {f : M → M₁} {g : M₁ → M} {f' : M₁ → M₂} {g' : M₂ → M₁}
    (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B' B'' f' g') :
    IsAdjointPair B B'' (f' ∘ f) (g ∘ g') := fun _ _ ↦ by
  rw [Function.comp_def, Function.comp_def, h', h]

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ (B'' ((f' ∘ f) x✝¹)) x✝ = (B x✝¹) ((g ∘ g') x✝)

Tactic:
rw [Function.comp_def, Function.comp_def, h', h]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem argmax_eq_none : l.argmax f = none ↔ l = []

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
l : List α
⊢ argmax f l = none ↔ l = []

Tactic:
simp [argmax]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToFun_le' (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
    ‖setToFun μ T hT f‖ ≤ max C 0 * ‖hf.toL1 f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ ‖setToFun μ T hT f‖ ≤ (C ⊔ 0) * ‖Integrable.toL1 f hf‖

Tactic:
rw [setToFun_eq hT hf]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ ‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ (C ⊔ 0) * ‖Integrable.toL1 f hf‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ ‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ (C ⊔ 0) * ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_setToL1_le_mul_norm' hT _

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_le_iff_codisjoint_right : ￢a ≤ b ↔ Codisjoint a b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ b ↔ Codisjoint a b

Tactic:
rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_zero [Nonempty ι] : f 0 = 0

Proof state:
case intro
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Nonempty ι
i : ι
h✝ : i ∈ Set.univ
⊢ f 0 = 0

Tactic:
exact map_coord_zero f i rfl

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Nonempty ι
⊢ f 0 = 0

Tactic:
obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι

Result:
case intro
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Nonempty ι
i : ι
h✝ : i ∈ Set.univ
⊢ f 0 = 0
-- Mathlib/Algebra/Group/Pi/Basic.lean
@[to_additive]
lemma comp_eq_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :
    g ∘ f = 1 ↔ f = 1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : One β
inst✝ : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f = 1 ↔ f = 1

Tactic:
simpa [hg0, const_one] using comp_eq_const_iff 1 f hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_le_length : countP p l ≤ l.length

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).length ≤ l.length

Tactic:
apply length_filter_le

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l ≤ l.length

Tactic:
simp only [countP_eq_length_filter]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).length ≤ l.length
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    succ (bsup.{_, v} o f) ≤ blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f

Proof state:
case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
⊢ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

Tactic:
by_contra! hf

Result:
case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ o.bsup f
⊢ False

Proof state:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (∃ i, ∃ (hi : i < o), f i hi = o.bsup f) → succ (o.bsup f) ≤ o.blsub f

Tactic:
rintro ⟨_, _, hf⟩

Result:
case refine_2.intro.intro
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ succ (o.bsup f) ≤ o.blsub f

Proof state:
case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ o.bsup f
⊢ False

Tactic:
exact
  ne_of_lt (succ_le_iff.1 h)
    (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

Result:
no goals

Proof state:
case refine_2.intro.intro
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ succ (o.bsup f) ≤ o.blsub f

Tactic:
rw [succ_le_iff, ← hf]

Result:
case refine_2.intro.intro
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f

Proof state:
case refine_2.intro.intro
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f

Tactic:
exact lt_blsub _ _ _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ succ (o.bsup f) ≤ o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

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

Result:
case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
⊢ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (∃ i, ∃ (hi : i < o), f i hi = o.bsup f) → succ (o.bsup f) ≤ o.blsub f
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub_eq_toIcoDiv_add (a b c : α) :
    toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b

Tactic:
apply toIcoDiv_eq_of_sub_zsmul_mem_Ico

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_right_comm]

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)

Tactic:
exact sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_eq_iff_covBy : succ a = b ↔ a ⋖ b :=
  ⟨by rintro rfl; exact covBy_succ _, CovBy.succ_eq⟩

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a

Tactic:
exact covBy_succ _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a = b → a ⋖ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem exists_sq_eq_neg_two_iff (hp : p ≠ 2) : IsSquare (-2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 3

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
rw [FiniteField.isSquare_neg_two_iff, card p]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@[reassoc (attr := simp)]
lemma isoLimit_inv_π (g : StructuredArrow Y L) :
    h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right =
      limit.π (StructuredArrow.proj Y L ⋙ F) g

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{u_6, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst✝ : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right = limit.π (StructuredArrow.proj Y L ⋙ F) g

Tactic:
simpa using h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_yield_eq_foldl
    (l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : (a : α) → a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → β
⊢ (forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init { toArray := toArray✝, size_toArray := size_toArray✝ }.attach

Tactic:
simp [List.foldl_map]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : (a : α) → a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → β
⊢ (forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init { toArray := toArray✝, size_toArray := size_toArray✝ }.attach
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpTo.continuous (h : HasFTaylorSeriesUpTo n f p) : Continuous f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
⊢ Continuous f

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ Continuous f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ ContinuousOn f univ

Tactic:
exact h.continuousOn

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ Continuous f

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ ContinuousOn f univ
-- Mathlib/Data/Seq/Seq.lean
theorem length_toList (s : Seq α) (h : s.Terminates) : (toList s h).length = length s h

Proof state:
α : Type u
s : Seq α
h h✝ : s.Terminates
⊢ s.length h ≤ s.length h✝

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u
s : Seq α
h : s.Terminates
⊢ ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1

Tactic:
intro _

Result:
α : Type u
s : Seq α
h h✝ : s.Terminates
⊢ s.length h ≤ s.length h✝

Proof state:
α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).length = s.length h

Tactic:
rw [toList, length_take_of_le_length]

Result:
α : Type u
s : Seq α
h : s.Terminates
⊢ ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem Filter.Tendsto.atBot_add {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x + g x) l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => g x + f x) l atBot

Tactic:
exact hg.add_atBot hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x + g x) l atBot

Tactic:
conv in _ + _ => rw [add_comm]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => g x + f x) l atBot
-- Mathlib/Order/SymmDiff.lean
theorem compl_symmDiff : (a ∆ b)ᶜ = a ⇔ b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ∆ b)ᶜ = a ⇔ b

Tactic:
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_getD : Primrec₂ (@Option.getD α) :=
  Primrec.of_eq (option_casesOn Primrec₂.left Primrec₂.right .right) fun ⟨o, a⟩ => by
    cases o <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
o : Option α
a : α
⊢ (Option.casesOn ((fun a x => a) (o, a).1 (o, a).2) ((fun x b => b) (o, a).1 (o, a).2) fun b => b) =
    (o, a).1.getD (o, a).2

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem some_single_none [Zero M] (m : M) : (single none m : Option α →₀ M).some = 0

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
m : M
a✝ : α
⊢ (single none m).some a✝ = 0 a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
m : M
⊢ (single none m).some = 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
m : M
a✝ : α
⊢ (single none m).some a✝ = 0 a✝
-- Mathlib/Data/Fin/Basic.lean
/-- By moving `succ` to the outside of this expression, we create opportunities for further
simplification using `succAbove_zero` or `succ_succAbove_zero`. -/
@[simp] lemma succ_succAbove_one {n : ℕ} [NeZero n] (i : Fin (n + 1)) :
    i.succ.succAbove 1 = (i.succAbove 0).succ

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ

Tactic:
rw [← succ_zero_eq_one']

Result:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ

Tactic:
convert succ_succAbove_succ i 0

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem natTrans_app_f_app (P : Karoubi (SimplicialObject C)) :
    Γ₂N₂.natTrans.app P =
      (N₂ ⋙ Γ₂).map P.decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ natTrans.app P = (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
dsimp only [natTrans]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
              (toKaroubi (SimplicialObject C))).preimage
          (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans)).app
      P =
    (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
              (toKaroubi (SimplicialObject C))).preimage
          (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans)).app
      P =
    (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
simp only [whiskeringLeft_obj_preimage_app, Functor.id_map, assoc]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem gcd_dvd_right : gcd x y ∣ y :=
  (Submodule.IsPrincipal.mem_iff_generator_dvd _).mp (Ideal.subset_span (by simp))

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ y ∈ {x, y}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem Inv2.upper_lt_size {decls : Array (Decl α)} (hinv : Inv2 decls upper map) :
    upper ≤ decls.size

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
upper : Nat
map : HashMap α Nat
decls : Array (Decl α)
hinv : Inv2 decls upper map
⊢ upper ≤ decls.size

Tactic:
cases hinv <;> omega

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem balanced_ball_zero : Balanced 𝕜 (Metric.ball (0 : E) r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.ball 0 r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).ball 0 r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).ball 0 r)

Tactic:
exact (normSeminorm _ _).balanced_ball_zero r

Result:
no goals
-- Mathlib/Algebra/Module/Defs.lean
theorem Module.ext' {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] (P Q : Module R M)
    (w : ∀ (r : R) (m : M), (haveI := P; r • m) = (haveI := Q; r • m)) :
    P = Q

Proof state:
R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q

Tactic:
ext

Result:
case smul.h.h
R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Proof state:
case smul.h.h
R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Tactic:
exact w _ _

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map₂_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
    (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) :
    map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
ε : Type u_8
ε' : Type u_9
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

Tactic:
cases a <;> cases b <;> cases c <;> simp [h_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_arrow :
    (imageSubobjectIso f).hom ≫ image.ι f = (imageSubobject f).arrow

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).hom ≫ image.ι f = (imageSubobject f).arrow

Tactic:
simp [imageSubobjectIso]

Result:
no goals