harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Semicontinuous.lean
theorem upperSemicontinuousOn_univ_iff : UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f : α → β
⊢ UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f

Tactic:
simp [UpperSemicontinuousOn, UpperSemicontinuous, upperSemicontinuousWithinAt_univ_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_segments (a b c d : E) :
    convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = convexHull 𝕜 {a, b, c, d}

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c d : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}

Tactic:
simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
  convexHull_insert (singleton_nonempty _), convexJoin_assoc,
  convexHull_singleton]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.continuous_iff {β : Type*} [TopologicalSpace β]
    {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :
    Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

Tactic:
rw [hB.eq_generateFrom, continuous_generateFrom_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem isBase_restrict_iff (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X

Tactic:
simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_or_distrib_left {f : Filter α} [NeBot f] {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p ∨ q x) ↔ p ∨ ∃ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem eq_loopyOn_or_rankPos (M : Matroid α) : M = loopyOn M.E ∨ RankPos M

Proof state:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅

Tactic:
apply em

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M = loopyOn M.E ∨ M.RankPos

Tactic:
rw [← empty_isBase_iff, rankPos_iff]

Result:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ∨ ¬M.IsBase ∅
-- Mathlib/Data/Nat/PSub.lean
theorem sub_eq_psub (m : ℕ) : ∀ n, m - n = (psub m n).getD 0
  | 0 => rfl
  | n + 1 => (pred_eq_ppred (m - n)).trans <| by rw [sub_eq_psub m n, psub]; cases psub m n <;> rfl

Proof state:
m n : ℕ
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0

Tactic:
cases psub m n <;> rfl

Result:
no goals

Proof state:
m n : ℕ
⊢ (m - n).ppred.getD 0 = (m.psub (n + 1)).getD 0

Tactic:
rw [sub_eq_psub m n, psub]

Result:
m n : ℕ
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
-- Mathlib/Order/Atoms.lean
theorem isCoatom_iff {p : Prop} : IsCoatom p ↔ ¬ p

Proof state:
p : Prop
⊢ ¬p → ∀ (b : Prop), (p → b) → b → ¬p → b

Tactic:
tauto

Result:
no goals

Proof state:
p : Prop
⊢ IsCoatom p ↔ ¬p

Tactic:
simp [IsCoatom, show ⊤ = True from rfl, fun q r : Prop => show q < r ↔ _ ∧ _ from .rfl]

Result:
p : Prop
⊢ ¬p → ∀ (b : Prop), (p → b) → b → ¬p → b
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem swapTrue_eq_true (x : I → Bool) : SwapTrue o x (term I ho) = true

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
⊢ SwapTrue o x (term I ho) = true

Tactic:
simp only [SwapTrue, ord_term_aux, ite_true]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₁_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R)
    (φ : MvPolynomial σ R) : (bind₁ g) (bind₁ f φ) = bind₁ (fun i => bind₁ g (f i)) φ

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
φ : MvPolynomial σ R
⊢ (bind₁ g) ((bind₁ f) φ) = (bind₁ fun i => (bind₁ g) (f i)) φ

Tactic:
simp [bind₁, ← comp_aeval]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_cons (a : α) (l : List α) :
    sublists (a :: l) = sublists l >>= (fun x => [x, a :: x]) :=
  show sublists ([a] ++ l) = _ by
  rw [sublists_append]
  simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

Proof state:
α : Type u
a : α
l : List α
⊢ (do
      let x ← l.sublists
      map (fun x_1 => x_1 ++ x) [a].sublists) =
    do
    let x ← l.sublists
    [x, a :: x]

Tactic:
simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
⊢ ([a] ++ l).sublists = do
    let x ← l.sublists
    [x, a :: x]

Tactic:
rw [sublists_append]

Result:
α : Type u
a : α
l : List α
⊢ (do
      let x ← l.sublists
      map (fun x_1 => x_1 ++ x) [a].sublists) =
    do
    let x ← l.sublists
    [x, a :: x]
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_floor_right_pure (n : ℤ) : Tendsto (floor : α → ℤ) (𝓝[≥] n) (pure n)

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[≥] ↑n) (pure n)

Tactic:
simpa only [floor_intCast] using tendsto_floor_right_pure_floor (n : α)

Result:
no goals
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_union [DecidableEq α] : (s ∪ t).pimage f = s.pimage f ∪ t.pimage f :=
  coe_inj.1 <| by
  simp only [coe_pimage, coe_union, ← PFun.image_union]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
s t : Finset α
inst✝ : DecidableEq α
⊢ ↑(pimage f (s ∪ t)) = ↑(pimage f s ∪ pimage f t)

Tactic:
simp only [coe_pimage, coe_union, ← PFun.image_union]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
@[simp] lemma wcovBy_insert (s : Finset α) (a : α) : s ⩿ insert a s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⩿ insert a s

Tactic:
simp [← coe_wcovBy_coe]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem pair_unpair' {n a b} (H : unpair n = (a, b)) : pair a b = n

Proof state:
n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n

Tactic:
simpa [H] using pair_unpair n

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem sum_card [Fintype α] (h : ∀ a, #{b ∈ B | a ∈ b} = n) :
    ∑ s ∈ B, #s = Fintype.card α * n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #(filter (fun b => a ∈ b) B) = n
⊢ ∑ s ∈ B, #s = Fintype.card α * n

Tactic:
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingNorm_comp (f : ∀ i, γ i → β i) {x : ∀ i, γ i} (hf₁ : ∀ i, Injective (f i))
    (hf₂ : ∀ i, f i 0 = 0) : (hammingNorm fun i => f i (x i)) = hammingNorm x

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf₁ : ∀ (i : ι), Injective (f i)
hf₂ : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) = hammingNorm x

Tactic:
simpa only [← hammingDist_zero_right, hf₂] using hammingDist_comp f hf₁ (y := fun _ ↦ 0)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a

Proof state:
a b : Prop
h : b = False
⊢ (a ∨ b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem leadingCoeff_prod : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
simpa using leadingCoeff_multiset_prod (s.1.map f)

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem mul_lowerClosure : s * lowerClosure t = lowerClosure (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))

Tactic:
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
  LowerSet.coe_iSup₂]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(lowerClosure t) = ⋃ i ∈ s, ↑(i • lowerClosure t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(lowerClosure t) = ⋃ i ∈ s, ↑(i • lowerClosure t)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma nontrivial_iff {n : ℕ} : Nontrivial (ZMod n) ↔ n ≠ 1

Proof state:
n : ℕ
⊢ Nontrivial (ZMod n) ↔ n ≠ 1

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
lemma part_mem (ha : a ∈ s) : P.part a ∈ P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ∈ P.parts

Tactic:
simp [part, ha, choose_mem]

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

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x

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

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.add_nsmul_eq [AddMonoid α] [AddGroup β] (h : Antiperiodic f c) (n : ℕ) :
    f (x + n • c) = (-1) ^ n • f x

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x

Tactic:
rw [h.odd_nsmul_antiperiodic]

Result:
case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ -f x = (-1) ^ (2 * k + 1) • f x

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ -f x = (-1) ^ (2 * k + 1) • f x

Tactic:
simp [pow_add]

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f x = (-1) ^ (2 * k) • f x

Tactic:
simp

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k) • c) = (-1) ^ (2 * k) • f x

Tactic:
rw [h.even_nsmul_periodic]

Result:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f x = (-1) ^ (2 * k) • f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℕ
⊢ f (x + n • c) = (-1) ^ n • f x

Tactic:
rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩

Result:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k) • c) = (-1) ^ (2 * k) • f x

case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x
-- Mathlib/Data/Nat/Count.lean
theorem count_eq_card_fintype (n : ℕ) : count p n = Fintype.card { k : ℕ // k < n ∧ p k }

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (Fintype.card ↑fun x => x < n ∧ p x) = Fintype.card { k // k < n ∧ p k }

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }

Tactic:
rw [count_eq_card_filter_range, ← Fintype.card_ofFinset, ← CountSet.fintype]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (Fintype.card ↑fun x => x < n ∧ p x) = Fintype.card { k // k < n ∧ p k }
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₃_app_three : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨3, by valid⟩ = app₃ :=
  rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.217301, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
⊢ 3 < 3 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.uniformEquicontinuous_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → β → α} (hα : (𝓤 α).HasBasis p s) :
    UniformEquicontinuous F ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact (hs : IsCompact s) :
    TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoLocallyUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s

Tactic:
rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
  tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
  tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Tactic:
haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

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

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoLocallyUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem GroupWithZero.mul_right_injective (h : x ≠ 0) :
    Function.Injective fun y => x * y := fun y y' w => by
  simpa only [← mul_assoc, inv_mul_cancel₀ h, one_mul] using congr_arg (fun y => x⁻¹ * y) w

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y => x * y) y = (fun y => x * y) y'
⊢ y = y'

Tactic:
simpa only [← mul_assoc, inv_mul_cancel₀ h, one_mul] using congr_arg (fun y => x⁻¹ * y) w

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f : 𝕜 → 𝕜` is concave on `s`, then for any point `x ∈ s` the slope of the secant line of `f`
through `x` is antitone on `s \ {x}`. -/
lemma ConcaveOn.slope_anti (hfc : ConcaveOn 𝕜 s f) (hx : x ∈ s) :
    AntitoneOn (slope f x) (s \ {x})

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn (slope f x) (s \ {x})

Tactic:
rw [← neg_neg f, slope_neg_fun]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn ((-slope (-f)) x) (s \ {x})

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn ((-slope (-f)) x) (s \ {x})

Tactic:
exact (ConvexOn.slope_mono hfc.neg hx).neg

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem monomial_add_single : monomial (s + Finsupp.single n e) a = monomial s a * X n ^ e

Proof state:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial s) a * X n ^ e

Tactic:
rw [X_pow_eq_monomial, monomial_mul, mul_one]

Result:
no goals
-- Mathlib/Topology/Order/ProjIcc.lean
theorem isQuotientMap_projIcc : IsQuotientMap (projIcc a b h) :=
  isQuotientMap_iff.2 ⟨projIcc_surjective h, fun s =>
    ⟨fun hs => hs.preimage continuous_projIcc, fun hs => ⟨_, hs, by ext; simp⟩⟩⟩

Proof state:
case h
α : Type u_1
inst✝² : LinearOrder α
a b : α
h : a ≤ b
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
x✝ : { x // x ∈ Icc a b }
⊢ x✝ ∈ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) ↔ x✝ ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
a b : α
h : a ≤ b
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
⊢ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) = s

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : LinearOrder α
a b : α
h : a ≤ b
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
x✝ : { x // x ∈ Icc a b }
⊢ x✝ ∈ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) ↔ x✝ ∈ s
-- Mathlib/Data/NNReal/Defs.lean
lemma toNNReal_le_toNNReal_iff_of_pos {r p : ℝ} (hr : 0 < r) : r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Proof state:
r p : ℝ
hr : 0 < r
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
simp [toNNReal_le_toNNReal_iff', hr.not_le]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.cellFrontier_zero_eq_empty [RelCWComplex C D] {j : cell C 0} :
    cellFrontier 0 j = ∅

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ cellFrontier 0 j = ∅

Tactic:
simp [cellFrontier, sphere_eq_empty_of_subsingleton]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_relfinrank (h1 : A ≤ B) (h2 : B ≤ C) :
    relfinrank A B * relfinrank B C = relfinrank A C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank h1 h2))

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap_comm :
    homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem edist_le_coe {x y : α} {c : ℝ≥0} : edist x y ≤ c ↔ nndist x y ≤ c

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y ≤ ↑c ↔ nndist x y ≤ c

Tactic:
rw [edist_nndist, ENNReal.coe_le_coe]

Result:
no goals
-- Mathlib/Algebra/Colimit/DirectLimit.lean
theorem exists_eq_one (x) :
    ⟦x⟧ = (1 : DirectLimit G f) ↔ ∃ i h, f x.1 i h x.2 = 1

Proof state:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_4
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ ⟦x⟧ = 1 ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

Tactic:
rw [one_def x.1, Quotient.eq]

Result:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_4
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ (setoid f) x ⟨x.fst, 1⟩ ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

Proof state:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_4
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ (setoid f) x ⟨x.fst, 1⟩ ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

Tactic:
exact ⟨fun ⟨i, h, _, eq⟩ ↦ ⟨i, h, eq.trans (map_one _)⟩,
  fun ⟨i, h, eq⟩ ↦ ⟨i, h, h, eq.trans (map_one _).symm⟩⟩

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_le_cardinal (n : ℕ) : (count p n : Cardinal) ≤ Cardinal.mk { k | p k }

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k // k < n ∧ p k } ≤ Cardinal.mk ↑{k | p k}

Tactic:
exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}

Tactic:
rw [count_eq_card_fintype, ← Cardinal.mk_fintype]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k // k < n ∧ p k } ≤ Cardinal.mk ↑{k | p k}
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t_fst_snd (i j : 𝒰.J) :
    t 𝒰 f g i j ≫ pullback.fst _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j : 𝒰.J
⊢ t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.snd (𝒰.map j ≫ f) g =
    pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_snd,
  pullback.lift_snd, Category.comp_id, pullbackAssoc_inv_snd, pullbackSymmetry_hom_comp_snd_assoc]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem dense_discrete {s : Set α} : Dense s ↔ s = univ

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
s : Set α
⊢ Dense s ↔ s = univ

Tactic:
simp [dense_iff_closure_eq]

Result:
no goals