harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem neg_mem (hx : x ∈ p) : -x ∈ p

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -x ∈ p

Tactic:
rw [← neg_one_smul R]

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -1 • x ∈ p

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -1 • x ∈ p

Tactic:
exact p.smul_mem _ hx

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_sub : (p - q).natDegree = (q - p).natDegree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).natDegree = (q - p).natDegree

Tactic:
rw [← natDegree_neg, neg_sub]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem nhds_top_basis : (𝓝 (⊤ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Ioi ·)

Proof state:
⊢ (𝓝 ⊤).HasBasis (fun x => True) fun x => Ioi ↑x

Tactic:
refine nhds_top_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩

Result:
x : EReal
hx : x < ⊤
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x

Proof state:
case intro.intro
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x

Tactic:
exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

Result:
no goals

Proof state:
x : EReal
hx : x < ⊤
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x

Tactic:
rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩

Result:
case intro.intro
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean
theorem inv_comp_image_ι_map {X Y : A} (f : X ⟶ Y) :
    (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f)

Proof state:
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma evalEval_polynomialY (x y : R) : W'.polynomialY.evalEval x y = 2 * y + W'.a₁ * x + W'.a₃

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = 2 * y + W'.a₁ * x + W'.a₃

Tactic:
eval_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ 2 * y + (W'.a₁ * x + W'.a₃) = 2 * y + W'.a₁ * x + W'.a₃

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.polynomialY = 2 * y + W'.a₁ * x + W'.a₃

Tactic:
simp only [polynomialY]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = 2 * y + W'.a₁ * x + W'.a₃

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ 2 * y + (W'.a₁ * x + W'.a₃) = 2 * y + W'.a₁ * x + W'.a₃

Tactic:
rw [← add_assoc]

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

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

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bind_pure : p.bind pure = p :=
  PMF.ext fun x => (bind_apply _ _ _).trans (_root_.trans
    (tsum_eq_single x fun y hy => by rw [pure_apply_of_ne _ _ hy.symm, mul_zero]) <|
    by rw [pure_apply_self, mul_one])

Proof state:
α : Type u_1
p : PMF α
x : α
⊢ p x * (pure x) x = p x

Tactic:
rw [pure_apply_self, mul_one]

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ p y * (pure y) x = 0

Tactic:
rw [pure_apply_of_ne _ _ hy.symm, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m

Proof state:
x : Int
m : Nat
p : x % ↑m < (↑m + 1) / 2
⊢ x.bmod m = x % ↑m

Tactic:
simp [bmod_def, p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_modify (h : m.1.WF) {k k' : α} {fallback : β} {f : β → β} :
    Const.getD (Const.modify m k f) k' fallback =
      if k == k' then
        Const.get? m k |>.map f |>.getD fallback
      else
        Const.getD m k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
fallback : β
f : β → β
⊢ getD (modify m k f) k' fallback =
    if (k == k') = true then (Option.map f (get? m k)).getD fallback else getD m k' fallback

Tactic:
simp_to_model [Const.modify] using List.Const.getValueD_modifyKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n

Proof state:
x y : Int
n : Nat
⊢ (x + y.bmod n).bmod n = (x + y).bmod n

Tactic:
rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem hasSum_mFourier_series_L2 (f : L²(UnitAddTorus d)) :
    HasSum (fun i ↦ mFourierCoeff f i • mFourierLp 2 i) f

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i => mFourierCoeff (↑↑f) i • mFourierLp 2 i) f

Tactic:
simpa [← coe_mFourierBasis, mFourierBasis_repr] using mFourierBasis.hasSum_repr f

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swapCore_self (r a : α) : swapCore a a r = r

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r

Tactic:
unfold swapCore

Result:
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullback.mapDesc_comp {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) (i' : S ⟶ S')
    [HasPullback f g] [HasPullback (f ≫ i) (g ≫ i)] [HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')]
    [HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
    pullback.mapDesc f g (i ≫ i') = pullback.mapDesc f g i ≫ pullback.mapDesc _ _ i' ≫
    (pullback.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y S T S' : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
i' : S ⟶ S'
inst✝³ : HasPullback f g
inst✝² : HasPullback (f ≫ i) (g ≫ i)
inst✝¹ : HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')
inst✝ : HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')
⊢ mapDesc f g (i ≫ i') = mapDesc f g i ≫ mapDesc (f ≫ i) (g ≫ i) i' ≫ (congrHom ⋯ ⋯).hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem realize_one (v : α → R) : Term.realize v (1 : ring.Term α) = 1

Proof state:
α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
v : α → R
⊢ Term.realize v 1 = 1

Tactic:
simp [one_def, funMap_one, constantMap]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma retractionOfSectionOfKerSqZero_comp_kerToTensor :
    (retractionOfSectionOfKerSqZero g hf' hg).comp (kerToTensor R P S) = LinearMap.id

Proof state:
case h.a
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
x : ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S) x) = ↑(LinearMap.id x)

Tactic:
simp [RingHom.mem_ker.mp x.2]

Result:
no goals

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
⊢ retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S = LinearMap.id

Tactic:
ext x

Result:
case h.a
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
x : ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S) x) = ↑(LinearMap.id x)
-- Mathlib/Topology/NhdsSet.lean
theorem union_mem_nhdsSet (h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) : s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Tactic:
rw [nhdsSet_union]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂

Tactic:
exact union_mem_sup h₁ h₂

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

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

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y

Proof state:
α : Type u_1
a : Array α
x y : α
⊢ x ∈ a.push y ↔ x ∈ a ∨ x = y

Tactic:
simp only [mem_def]

Result:
α : Type u_1
a : Array α
x y : α
⊢ x ∈ (a.push y).toList ↔ x ∈ a.toList ∨ x = y

Proof state:
α : Type u_1
a : Array α
x y : α
⊢ x ∈ (a.push y).toList ↔ x ∈ a.toList ∨ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem add_left [Distrib R] {a b x y : R} (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) :
    SemiconjBy (a + b) x y

Proof state:
R : Type u
inst✝ : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y

Tactic:
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_nonpos_ae (hs : MeasurableSet s) (hf : ∀ᵐ x ∂μ, x ∈ s → f x ≤ 0) :
    ∫ x in s, f x ∂μ ≤ 0 :=
  setIntegral_nonpos_of_ae_restrict <| by rwa [EventuallyLE, ae_restrict_iff' hs]

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
⊢ f ≤ᶠ[ae (μ.restrict s)] 0

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_flatMap {α} [BEq β] (l : Array α) (f : α → Array β) (x : β) :
    count x (l.flatMap f) = sum (map (count x ∘ f) l)

Proof state:
β : Type u_1
α : Type u_2
inst✝ : BEq β
l : Array α
f : α → Array β
x : β
⊢ count x (flatMap f l) = (map (count x ∘ f) l).sum

Tactic:
simp [count_eq_countP, countP_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem cocompact_eq_cofinite (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    cocompact X = cofinite

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ cocompact X = cofinite

Tactic:
simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} {h} :
    get m a h = getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.val.WF
a : α
fallback : β
h : m.contains a = true
⊢ get m a h = getD m a fallback

Tactic:
simp_to_model using List.getValue_eq_getValueD

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
private lemma ringChar_ne : ringChar ℂ ≠ ringChar F

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ ringChar ℂ ≠ ringChar F

Tactic:
simpa only [ringChar.eq_zero] using (CharP.ringChar_ne_zero_of_finite F).symm

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem stdOrthonormalBasis_map_eq :
    (euclidean.stdOrthonormalBasis K).toBasis.map (toMixed K).toLinearEquiv =
      mixedEmbedding.stdBasis K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (stdOrthonormalBasis K).toBasis.map (toMixed K).toLinearEquiv = stdBasis K

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem prime_dvd_prime_iff_eq {M : Type*} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M}
    (pp : Prime p) (qp : Prime q) : p ∣ q ↔ p = q

Proof state:
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q

Tactic:
rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp.map Prod.fst = l)
    (hr : lp.map Prod.snd = l') : lp = l.zip l'

Proof state:
α : Type u_1
β : Type u_2
l : List α
l' : List β
lp : List (α × β)
hl : map Prod.fst lp = l
hr : map Prod.snd lp = l'
⊢ lp = l.zip l'

Tactic:
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem forall_mem_cons (h : a ∉ s) (p : α → Prop) :
    (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x

Proof state:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
p : α → Prop
⊢ (∀ x ∈ cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x

Tactic:
simp only [mem_cons, or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
    Unbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r s

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s

Tactic:
simp_rw [← not_bounded_iff, bounded_inter_not H]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UInt.lean
theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits

Proof state:
x : USize
⊢ x.toNat < size

Tactic:
exact x.val.isLt

Result:
no goals

Proof state:
x : USize
⊢ x.toNat < 2 ^ System.Platform.numBits

Tactic:
rw [←USize.size_eq]

Result:
x : USize
⊢ x.toNat < size
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.int_odd_mul_antiperiodic [Ring α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Antiperiodic f (n * (2 * c) + c) := fun x => by
  rw [← add_assoc, h, h.int_even_mul_periodic]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Ring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
rw [← add_assoc, h, h.int_even_mul_periodic]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i :=
  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t • · ∈ _)) hs
    (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
    (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem)
  (iSup_le fun i ↦ smul_le_smul_right <| le_iSup _ i)

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ (fun x => t • x ∈ ⨆ i, T • S i) x → (fun x => t • x ∈ ⨆ i, T • S i) y → (fun x => t • x ∈ ⨆ i, T • S i) (x + y)

Tactic:
simp_rw [smul_add]

Result:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ t • x ∈ ⨆ i, T • S i → t • y ∈ ⨆ i, T • S i → t • x + t • y ∈ ⨆ i, T • S i

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ (fun x => t • x ∈ ⨆ i, T • S i) 0

Tactic:
simp_rw [smul_zero]

Result:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ 0 ∈ ⨆ i, T • S i

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ t • x ∈ ⨆ i, T • S i → t • y ∈ ⨆ i, T • S i → t • x + t • y ∈ ⨆ i, T • S i

Tactic:
apply add_mem

Result:
no goals

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
ι : Sort u_7
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ 0 ∈ ⨆ i, T • S i

Tactic:
apply zero_mem

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.eventuallyLE (h : f =o[l] g) : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖

Tactic:
simpa using h.def zero_lt_one

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Subtype.dense_iff {s : Set X} {t : Set s} : Dense t ↔ s ⊆ closure ((↑) '' t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : X) (h : x ∈ s), ↑⟨x, h⟩ ∈ closure (val '' t)) ↔ s ⊆ closure ↑t

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ Dense t ↔ s ⊆ closure ↑t

Tactic:
rw [IsInducing.subtypeVal.dense_iff, SetCoe.forall]

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : X) (h : x ∈ s), ↑⟨x, h⟩ ∈ closure (val '' t)) ↔ s ⊆ closure ↑t
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma leftDeriv_klFun_one : derivWithin klFun (Iio 1) 1 = 0

Proof state:
⊢ derivWithin klFun (Iio 1) 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.DifferentiableWithinAt.mlieBracketWithin_congr_mono
    (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x)
    (hVs : EqOn V₁ V t) (hVx : V₁ x = V x)
    (hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) s x)
    (hWs : EqOn W₁ W t) (hWx : W₁ x = W x)
    (hxt : UniqueMDiffWithinAt I t x) (h₁ : t ⊆ s) :
    mlieBracketWithin I V₁ W₁ t x = mlieBracketWithin I V W s x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V₁ W₁ t x = mlieBracketWithin I V W s x

Tactic:
rw [mlieBracketWithin_congr hVs hVx hWs hWx]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Tactic:
exact mlieBracketWithin_subset h₁ hxt hV hW

Result:
no goals