harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v

Proof state:
u w v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v

Tactic:
omega

Result:
no goals

Proof state:
u w v k₁ k₂ : Nat
⊢ isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v

Tactic:
simp [isLt]

Result:
u w v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false)

Proof state:
b : Bool
⊢ ((!b) = true) = (b = false)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Part.lean
theorem eq_none_iff {o : Part α} : o = none ↔ ∀ a, a ∉ o :=
  ⟨fun e => e.symm ▸ not_mem_none, fun h => ext (by simpa)⟩

Proof state:
α : Type u_1
o : Part α
h : ∀ (a : α), a ∉ o
⊢ ∀ (a : α), a ∈ o ↔ a ∈ none

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_add_one (a : α) : round (a + 1) = round a + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round a + 1

Tactic:
rw [← round_add_int a 1, cast_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma fromCols_col0_isTotallyUnimodular_iff (A : Matrix m n R) :
    (fromCols A (col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromCols (col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_col,
  fromRows_row0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem succ_nth_stream_eq_none_iff :
    IntFractPair.stream v (n + 1) = none ↔
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
rw [IntFractPair.stream]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ((IntFractPair.stream v n).bind fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ((IntFractPair.stream v n).bind fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
cases IntFractPair.stream v n <;> simp [imp_false]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma isComplex₁ (S : ComposableArrows C 1) : S.IsComplex where
  zero i hi

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : autoParam (i + 2 ≤ 1) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
theorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α)
    (g : γ → β) : (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) :=
  haveI := Classical.decEq γ
  Finset.induction_on s rfl (by simp +contextual [Prod.ext_iff])

Proof state:
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Finset γ
f : γ → α
g : γ → β
this : DecidableEq γ
⊢ ∀ ⦃a : γ⦄ {s : Finset γ},
    a ∉ s →
      (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) →
        (∏ x ∈ insert a s, f x, ∏ x ∈ insert a s, g x) = ∏ x ∈ insert a s, (f x, g x)

Tactic:
simp +contextual [Prod.ext_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_of_uIcc_subset_left (h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s :=
  ordConnected_iff_uIcc_subset.2 fun y hy z hz =>
    calc
      [[y, z]] ⊆ [[y, x]] ∪ [[x, z]] := uIcc_subset_uIcc_union_uIcc
      _ = [[x, y]] ∪ [[x, z]]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]

Tactic:
rw [uIcc_comm]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.transcendental_ringHom_iff_of_comp_eq
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental S B ↔ Algebra.Transcendental R A

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : EquivLike FRS R S
inst✝² : RingEquivClass FRS R S
inst✝¹ : EquivLike FAB A B
inst✝ : RingEquivClass FAB A B
f : FRS
g : FAB
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental S B ↔ Algebra.Transcendental R A

Tactic:
simp_rw [Algebra.transcendental_iff_not_isAlgebraic,
  Algebra.isAlgebraic_ringHom_iff_of_comp_eq f g h]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ratCast_lt {x y : ℚ} : (x : ℝ) < (y : ℝ) ↔ x < y

Proof state:
x y : ℚ
⊢ ↑x < ↑y ↔ x < y

Tactic:
erw [mk_lt]

Result:
x y : ℚ
⊢ const abs ↑x < const abs ↑y ↔ x < y

Proof state:
x y : ℚ
⊢ const abs ↑x < const abs ↑y ↔ x < y

Tactic:
exact const_lt

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Scheme.homOfLE_apply {U V : X.Opens} (e : U ≤ V) (x : U) :
    ((X.homOfLE e).base x).1 = x

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((ConcreteCategory.hom (X.homOfLE e).base) x) = ↑x

Tactic:
rw [homOfLE_base]

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) x) = ↑x

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) x) = ↑x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) :
    c * a * star c ≤ c * b * star c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c

Tactic:
simpa only [star_star] using conjugate_le_conjugate hab (star c)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem contDiffAt_norm_smul_iff (ht : t ≠ 0) :
    ContDiffAt ℝ n (‖·‖) x ↔ ContDiffAt ℝ n (‖·‖) (t • x) where
  mp h := h.contDiffAt_norm_smul ht
  mpr hd

Proof state:
case h.e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
⊢ x = t⁻¹ • t • x

Tactic:
rw [smul_smul, inv_mul_cancel₀ ht, one_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
convert hd.contDiffAt_norm_smul (inv_ne_zero ht)

Result:
case h.e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
⊢ x = t⁻¹ • t • x
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem insert_union_distrib (a : α) (s t : Finset α) :
    insert a (s ∪ t) = insert a s ∪ insert a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t

Tactic:
simp only [insert_union, union_insert, insert_idem]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma natCast_le_rank_iff [Nontrivial R] {n : ℕ} :
    n ≤ Module.rank R M ↔ ∃ f : Fin n → M, LinearIndependent R f :=
  ⟨exists_linearIndependent_of_le_rank,
    fun H ↦ by simpa using H.choose_spec.cardinal_lift_le_rank⟩

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
H : ∃ f, LinearIndependent R f
⊢ ↑n ≤ Module.rank R M

Tactic:
simpa using H.choose_spec.cardinal_lift_le_rank

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (wf : P.Factors f)
    (wg : P.Factors g) : P.Factors (f + g) :=
  (factors_iff _ _).mpr ⟨P.factorThru f wf + P.factorThru g wg, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
wf : P.Factors f
wg : P.Factors g
⊢ (P.factorThru f wf + P.factorThru g wg) ≫ (representative.obj P).arrow = f + g

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W.addY P Q = addU P Q ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = addU P Q ^ 3

Tactic:
rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
  mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictAnti_of_add_one_lt : (∀ a, ¬ IsMax a → f (a + 1) < f a) → StrictAnti 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 + 1) < f a) → StrictAnti f

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

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_neg_sub_two (n : ℤ) : U R (-n - 2) = -U R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (-n - 2) = -U R n

Tactic:
simpa [sub_eq_add_neg, add_comm] using U_neg R (n + 2)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegral_add_eq_add (hf : Periodic f T) (t s : ℝ)
    (h_int : ∀ t₁ t₂, IntervalIntegrable f MeasureSpace.volume t₁ t₂) :
    ∫ x in t..s + T, f x = (∫ x in t..s, f x) + ∫ x in t..t + T, f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x

Tactic:
rw [hf.intervalIntegral_add_eq t s, integral_add_adjacent_intervals (h_int t s) (h_int s _)]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem mem_iSup_of_mem {S : ι → Subsemigroup M} (i : ι) : ∀ {x : M}, x ∈ S i → x ∈ iSup S

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
tauto

Result:
no goals

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
have : S i ≤ iSup S := le_iSup _ _

Result:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem not_perm_cons_nil {l : List α} {a : α} : ¬((a::l) ~ []) :=
  fun h => by simpa using h.length_eq

Proof state:
α : Type u_1
l : List α
a : α
h : a :: l ~ []
⊢ False

Tactic:
simpa using h.length_eq

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem prod_eq_prod_of_nonempty'
    {eX eX' : PartialHomeomorph X X'} {eY eY' : PartialHomeomorph Y Y'}
    (h : (eX'.prod eY').source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX'.prod eY').source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
theorem complex_d_comp_π_f_zero :
    P.complex.d 1 0 ≫ P.π.f 0 = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ P.complex.d 1 0 ≫ P.π.f 0 = 0

Tactic:
rw [← P.π.comm 1 0, single_obj_d, comp_zero]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- Colex is an extension of the base order. -/
lemma singleton_le_singleton : (toColex {a} : Colex α) ≤ toColex {b} ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ { ofColex := {a} } ≤ { ofColex := {b} } ↔ a ≤ b

Tactic:
simp [toColex_le_singleton, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_mul_const'' (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    ∫⁻ a, f a * r ∂μ = (∫⁻ a, f a ∂μ) * r

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul'' r hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_mapFinIdx {l : Array α} {f : Nat → α → β} :
    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
⊢ mapIdx f l = l.mapFinIdx fun i a x => f i a

Tactic:
simp [mapFinIdx_eq_mapIdx]

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem toMonoidWithZeroHom_eq_coe (f : α →+* β) : (f.toMonoidWithZeroHom : α → β) = f

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ⇑f.toMonoidWithZeroHom = ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldl_eq_foldl_toList {t : RBNode α} : t.foldl f init = t.toList.foldl f init

Proof state:
α : Type u_1
α✝ : Type u_2
f : α✝ → α → α✝
init : α✝
t : RBNode α
⊢ foldl f init t = List.foldl f init t.toList

Tactic:
induction t generalizing init <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
    (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i

Proof state:
n : Nat
p : Nat → Bool
⊢ find? p (iota n) = none ↔ ∀ (i : Nat), 0 < i → i ≤ n → (!p i) = true

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_polynomialX : (W'.baseChange B).toProjective.polynomialX =
    MvPolynomial.map f (W'.baseChange A).toProjective.polynomialX

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toProjective.polynomialX = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialX

Tactic:
rw [← map_polynomialX, map_baseChange]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_lt_iff {x : ℝ} :
    schnirelmannDensity A < x ↔ ∃ n : ℕ, 0 < n ∧ #{a ∈ Ioc 0 n | a ∈ A} / n < x

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x

Tactic:
rw [← not_le, le_schnirelmannDensity_iff]

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n) ↔
    ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n) ↔
    ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem coeff_truncFun (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) :
    (truncFun n φ).coeff m = if m < n then coeff R m φ else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun n φ) = if m < n then (coeff R m) φ else 0

Tactic:
classical
simp [truncFun, MvPolynomial.coeff_sum]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun n φ) = if m < n then (coeff R m) φ else 0

Tactic:
simp [truncFun, MvPolynomial.coeff_sum]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) :
    a * b ≤ b ↔ (a ^ ω) ∣ b

Proof state:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b

Tactic:
rw [← mul_eq_right_iff_opow_omega0_dvd]

Result:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b

Proof state:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b

Tactic:
exact (isNormal_mul_right ha).le_iff_eq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt

Proof state:
o₁ o₂ : Ordering
⊢ o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt

Tactic:
cases o₁ <;> cases o₂ <;> decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSomeRev?_push_of_isSome (l : Array α) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isSome = true
toList✝ : List α
⊢ findSomeRev? f ({ toList := toList✝ }.push a) = f a

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
l : Array α
h : (f a).isSome = true
⊢ findSomeRev? f (l.push a) = f a

Tactic:
cases l

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isSome = true
toList✝ : List α
⊢ findSomeRev? f ({ toList := toList✝ }.push a) = f a
-- Mathlib/Data/Nat/Count.lean
theorem count_succ' (n : ℕ) :
    count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun k => p (k + 1)) n + if p 0 then 1 else 0

Tactic:
rw [count_add', count_one]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem continuousAt_iff_isLittleO {α : Type*} {E : Type*} [NormedRing E] [NormOneClass E]
    [TopologicalSpace α] {f : α → E} {x : α} :
    (ContinuousAt f x) ↔ (fun (y : α) ↦ f y - f x) =o[𝓝 x] (fun (_ : α) ↦ (1 : E))

Proof state:
α : Type u_17
E : Type u_18
inst✝² : NormedRing E
inst✝¹ : NormOneClass E
inst✝ : TopologicalSpace α
f : α → E
x : α
⊢ ContinuousAt f x ↔ (fun y => f y - f x) =o[𝓝 x] fun x => 1

Tactic:
simp [ContinuousAt, ← tendsto_sub_nhds_zero_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma coe_resLE_base (x : V) : ((f.resLE U V e).base x).val = f.base x

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ ↑((ConcreteCategory.hom (resLE f U V e).base) x) = (ConcreteCategory.hom f.base) ↑x

Tactic:
simp [resLE, morphismRestrict_base]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
@[simp] lemma degree_add_degree_leadingCoeff_inv (p : K[X]) :
    degree p + degree (C (leadingCoeff p)⁻¹) = degree p

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ p.degree + (C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
rw [← degree_mul, degree_mul_leadingCoeff_self_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_arrow_comp_eq_zero [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}
    [HasImage f] [Epi (factorThruImageSubobject f)] (h : f ≫ g = 0) :
    (imageSubobject f).arrow ≫ g = 0 :=
  zero_of_epi_comp (factorThruImageSubobject f) <| by simp [h]

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImageSubobject f)
h : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow ≫ g = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.pow_apply_eq_pow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s]

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s]

Tactic:
rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]

Result:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (↑n - ↑m)) a = a

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (↑n - ↑m)) a = a

Tactic:
simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_mul_iff_right : Coprime k (m * n) ↔ Coprime k m ∧ Coprime k n

Proof state:
k m n : Nat
⊢ k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime n

Tactic:
rw [@coprime_comm k, @coprime_comm k, @coprime_comm k, coprime_mul_iff_left]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.map {p : R[X]} (h : p.Separable) {f : R →+* S} : (p.map f).Separable :=
  let ⟨a, b, H⟩ := h
  ⟨a.map f, b.map f, by
    rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]⟩

Proof state:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * derivative (Polynomial.map f p) = 1

Tactic:
rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
  Polynomial.map_one]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_intCast_im (z : ℂ) (n : ℤ) : (z / n).im = z.im / n

Proof state:
z : ℂ
n : ℤ
⊢ (z / ↑n).im = z.im / ↑n

Tactic:
rw [div_intCast]

Result:
no goals
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
lemma card_inv_mul_of_doubling_lt_three_halves (h : #(A * A) < (3 / 2 : ℚ) * #A) :
    #(A⁻¹ * A) = #(A * A)

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
⊢ #(A⁻¹ * A) = #(A * A)

Tactic:
simp_rw [← smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves h ha, card_smul_finset]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A⁻¹ * A) = #(A * A)

Tactic:
obtain ⟨a, ha⟩ := nonempty_of_doubling h

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
⊢ #(A⁻¹ * A) = #(A * A)
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_finset_coe {s : Set α} (h : s.Finite) : ∃ s' : Finset α, ↑s' = s

Proof state:
α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ↑s' = s

Tactic:
cases h.nonempty_fintype

Result:
case intro
α : Type u
s : Set α
h : s.Finite
val✝ : Fintype ↑s
⊢ ∃ s', ↑s' = s

Proof state:
case intro
α : Type u
s : Set α
h : s.Finite
val✝ : Fintype ↑s
⊢ ∃ s', ↑s' = s

Tactic:
exact ⟨s.toFinset, s.coe_toFinset⟩

Result:
no goals