harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Basic.lean
theorem pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ico a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ico_subset a b)

Result:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ico (a i) (b i) ∈ 𝓝 (x i)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ico (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ico_mem_nhds (ha i) (hb i)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Ascoli.lean
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the uniform
structures of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same
uniform structure on `ι`.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.

This is a version of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsUniformInducing`
for convenuence. -/
lemma EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' [UniformSpace ι]
    {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
    IsUniformInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔
    IsUniformInducing ((⋃₀ 𝔖).restrict ∘ F)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).restrict ∘ F)

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
    ← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.constr_apply_fintype [Fintype ι] (b : Basis ι R M) (f : ι → M') (x : M) :
    (constr (M' := M') b S f : M → M') x = ∑ i, b.equivFun x i • f i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
S : Type u_10
inst✝³ : Semiring S
inst✝² : Module S M'
inst✝¹ : SMulCommClass R S M'
inst✝ : Fintype ι
b : Basis ι R M
f : ι → M'
x : M
⊢ ((b.constr S) f) x = ∑ i : ι, b.equivFun x i • f i

Tactic:
simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma monotone_of_le_add_one : (∀ a, ¬ IsMax a → f a ≤ f (a + 1)) → Monotone f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a ≤ f (a + 1)) → Monotone f

Tactic:
simpa [Order.succ_eq_add_one] using monotone_of_le_succ (f := f)

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem CompactlyGeneratedSpace.isClosed [CompactlyGeneratedSpace X] {s : Set X}
    (hs : ∀ ⦃K⦄, IsCompact K → IsClosed (s ∩ K)) : IsClosed s

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
⊢ IsClosed s

Tactic:
refine isClosed' fun K _ _ _ f hf ↦ ?_

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsClosed (f ⁻¹' s)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsClosed (f ⁻¹' (s ∩ range f))

Tactic:
exact (hs (isCompact_range hf)).preimage hf

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsClosed (f ⁻¹' s)

Tactic:
rw [← Set.preimage_inter_range]

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous f
⊢ IsClosed (f ⁻¹' (s ∩ range f))
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_pow (a : R[X]) (n : ℕ) : (a ^ n).toFinsupp = a.toFinsupp ^ n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp ^ n

Tactic:
rw [← ofFinsupp_pow]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R[X]
n : ℕ
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n

Tactic:
cases a

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp ^ n
-- Mathlib/Data/Fintype/Basic.lean
theorem List.toFinset_finRange (n : ℕ) : (List.finRange n).toFinset = Finset.univ

Proof state:
n : ℕ
⊢ (finRange n).toFinset = univ

Tactic:
ext

Result:
case h
n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ

Proof state:
case h
n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem exp_one_gt_d9 : 2.7182818283 < exp 1 :=
  lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)

Proof state:
⊢ 2.7182818283 < 2244083 / 825552 - 1 / 10 ^ 10

Tactic:
norm_num

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_one_hom {Z : C} (f : Z ⟶ M.X) : (f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Mon_ C
Z : C
f : Z ⟶ M.X
⊢ (f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f

Tactic:
rw [tensorHom_def_assoc, M.mul_one, rightUnitor_naturality]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem dist_apply_le_dist (x : α) : dist (f x) (g x) ≤ dist f g

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
x : α
⊢ dist (f x) (g x) ≤ dist f g

Tactic:
simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem setValue_eq (f : α ≃ β) (a : α) (b : β) : setValue f a b a = b

Proof state:
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
f : α ≃ β
a : α
b : β
⊢ (f.setValue a b) a = b

Tactic:
simp [setValue, swap_apply_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
    x >>> y = x >>> y.toNat

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x >>> y = x >>> y.toNat

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.of_comp_iff {g : β → γ} (hg : IsUniformInducing g) {f : α → β} :
    IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f

Tactic:
rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
  Function.comp_def, Function.comp_def]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Array α) (H₁) :
    (l.pmap g H₁).countP f =
      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m)))

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Array α
H₁ : ∀ (a : α), a ∈ l → p a
⊢ countP f (pmap g l H₁) =
    countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      l.attach

Tactic:
simp [pmap_eq_map_attach, countP_map, Function.comp_def]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_diff_Ico_self (h : a ≤ b) : Icc a b \ Ico a b = {b}

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}

Tactic:
simp [← coe_inj, h]

Result:
no goals
-- Mathlib/Data/Fintype/Fin.lean
theorem card_filter_univ_eq_vector_get_eq_count [DecidableEq α] (a : α) (v : List.Vector α n) :
    #{i | v.get i = a} = v.toList.count a

Proof state:
case nil
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
⊢ #(filter (fun i => Vector.nil.get i = a) univ) = List.count a Vector.nil.toList

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #(filter (fun i => xs.get i = a) univ) = List.count a xs.toList
⊢ #(filter (fun i => (x ::ᵥ xs).get i = a) univ) = List.count a (x ::ᵥ xs).toList

Tactic:
simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
  hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
v : List.Vector α n
⊢ #(filter (fun i => v.get i = a) univ) = List.count a v.toList

Tactic:
induction' v with n x xs hxs

Result:
case nil
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
⊢ #(filter (fun i => Vector.nil.get i = a) univ) = List.count a Vector.nil.toList

case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #(filter (fun i => xs.get i = a) univ) = List.count a xs.toList
⊢ #(filter (fun i => (x ::ᵥ xs).get i = a) univ) = List.count a (x ::ᵥ xs).toList
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem faithfulSMul_tower_top [FaithfulSMul R A] : FaithfulSMul S A

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Function.Injective ⇑(algebraMap R A)
⊢ Function.Injective ⇑(algebraMap S A)

Tactic:
exact injective_tower_top S ‹_›

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul R A
⊢ FaithfulSMul S A

Tactic:
rw [faithfulSMul_iff_algebraMap_injective] at *

Result:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Function.Injective ⇑(algebraMap R A)
⊢ Function.Injective ⇑(algebraMap S A)
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_eq_self : s.mulIndicator f = f ↔ mulSupport f ⊆ s

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ s.mulIndicator f = f ↔ mulSupport f ⊆ s

Tactic:
simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_hcongr {β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'}
    (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (bind m f) (bind m f')

Proof state:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (m.bind f) (m.bind f')

Tactic:
subst h

Result:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (m.bind f) (m.bind f')

Proof state:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ a ∈ m, f a = f' a
⊢ HEq (m.bind f) (m.bind f')

Tactic:
simp [bind_congr hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (m.bind f) (m.bind f')

Tactic:
simp only [heq_eq_eq] at hf

Result:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ a ∈ m, f a = f' a
⊢ HEq (m.bind f) (m.bind f')
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasStrictDerivAt.cpow (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x)
    (h0 : f x ∈ slitPlane) : HasStrictDerivAt (fun x => f x ^ g x)
      (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Proof state:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa using (hf.cpow hg h0).hasStrictDerivAt

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ0_j [Fact (IsUnit (3 : R))] : (ofJ0 R).j = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ (ofJ0 R).j = 0

Tactic:
rw [j, ofJ0_c₄]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0
-- Mathlib/Data/List/Infix.lean
@[simp] lemma take_isPrefix_take {m n : ℕ} : l.take m <+: l.take n ↔ m ≤ n ∨ l.length ≤ n

Proof state:
α : Type u_1
l : List α
m n : ℕ
⊢ take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n

Tactic:
simp [prefix_take_iff, take_prefix]

Result:
α : Type u_1
l : List α
m n : ℕ
⊢ m ⊓ l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n

Proof state:
α : Type u_1
l : List α
m n : ℕ
⊢ m ⊓ l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_le_toNNRat_iff (hp : 0 ≤ p) : toNNRat q ≤ toNNRat p ↔ q ≤ p

Proof state:
p q : ℚ
hp : 0 ≤ p
⊢ q.toNNRat ≤ p.toNNRat ↔ q ≤ p

Tactic:
simp [← coe_le_coe, toNNRat, hp]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem colLen_eq_card (μ : YoungDiagram) {j : ℕ} : μ.colLen j = (μ.col j).card

Proof state:
μ : YoungDiagram
j : ℕ
⊢ μ.colLen j = (μ.col j).card

Tactic:
simp [col_eq_prod]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem eq_one_iff' {a : ℕ} (ha0 : (a : ZMod p) ≠ 0) :
    legendreSym p a = 1 ↔ IsSquare (a : ZMod p)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = 1 ↔ IsSquare ↑a

Tactic:
rw [eq_one_iff]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a

case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0

Proof state:
case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0

Tactic:
exact mod_cast ha0

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem mk_eq_inl_mul_inr (g : G) (n : N) : (⟨n, g⟩ : N ⋊[φ] G) = inl n * inr g

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g } = inl n * inr g

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Whiskering.lean
theorem pentagon :
    whiskerRight (associator F G H).hom K ≫
        (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
      (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom

Proof state:
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (F.associator G H).hom K ≫ (F.associator (G ⋙ H) K).hom ≫ whiskerLeft F (G.associator H K).hom =
    ((F ⋙ G).associator H K).hom ≫ (F.associator G (H ⋙ K)).hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Nat/Prime/Factorial.lean
theorem Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Prime p), p ∣ n ! ↔ p ≤ n
  | 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_lt hp.pos)
  | n + 1, p, hp => by
    rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
    exact
      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩

Proof state:
n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1

Tactic:
rw [h]

Result:
no goals

Proof state:
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1

Tactic:
exact
  ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
    (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩

Result:
no goals

Proof state:
n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1

Tactic:
rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]

Result:
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
-- Mathlib/Data/Multiset/Interval.lean
theorem card_Ioo :
    #(Finset.Ioo s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioo s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 2

Tactic:
rw [Finset.card_Ioo_eq_card_Icc_sub_two, card_Icc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_distrib_left  : ∀ (x y z : Bool), (x && (y || z)) = (x && y || x && z)

Proof state:
⊢ ∀ (x y z : Bool), (x && (y || z)) = (x && y || x && z)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[simp] lemma neg_iff : MeromorphicOn (-f) U ↔ MeromorphicOn f U :=
  ⟨fun h ↦ by simpa only [neg_neg] using h.neg, neg⟩

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicOn (-f) U
⊢ MeromorphicOn f U

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_add_mod_of_lt (h : c < b) : (a * b + c) % b = c

Proof state:
a b c : ℕ
h : c < b
⊢ (a * b + c) % b = c

Tactic:
rw [Nat.mul_add_mod', Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Iio_True : Iio True = {False}

Proof state:
⊢ Iio True = {False}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_le])

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_X_mul' [DecidableEq σ] (m) (s : σ) (p : MvPolynomial σ R) :
    coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
refine (coeff_monomial_mul' _ _ _ _).trans ?_

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
  one_mul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    map f.toLinearMap (1 : Submodule R A) = 1

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map f.toLinearMap 1 ↔ x✝ ∈ 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap 1 = 1

Tactic:
ext

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map f.toLinearMap 1 ↔ x✝ ∈ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2))

Proof state:
m : Type u → Type u_1
α β σ : Type u
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (do
          let a ← x
          let _ ← y
          pure a).run
      s =
    do
    let p ← x.run s
    let p' ← y.run p.snd
    pure (p.fst, p'.snd)

Tactic:
simp

Result:
no goals

Proof state:
m : Type u → Type u_1
α β σ : Type u
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (x <* y).run s = do
    let p ← x.run s
    let p' ← y.run p.snd
    pure (p.fst, p'.snd)

Tactic:
show (x >>= fun a => y >>= fun _ => pure a).run s = _

Result:
m : Type u → Type u_1
α β σ : Type u
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (do
          let a ← x
          let _ ← y
          pure a).run
      s =
    do
    let p ← x.run s
    let p' ← y.run p.snd
    pure (p.fst, p'.snd)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_eq_none' : x.map f = none ↔ x = none

Proof state:
α✝¹ : Type u_1
x : Option α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ Option.map f x = none ↔ x = none

Tactic:
cases x <;> simp [map_none', map_some', eq_self_iff_true]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_singleton (x : α) : toList (singleton x) = [x]

Proof state:
α : Type u_1
x : α
⊢ (singleton x).toList = [x]

Tactic:
simp [singleton]

Result:
no goals