harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/ScottTopology.lean
lemma isOpen_iff [IsScottHausdorff α D] :
    IsOpen s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a : α⦄, IsLUB d a →
      a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α D
⊢ IsOpen s ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
simp [topology_eq_scottHausdorff (α := α) (D := D), IsOpen, scottHausdorff]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem summable_cantor_function (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) :
    Summable (cantorFunctionAux c f)

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c f)

Tactic:
apply (summable_geometric_of_lt_one h1 h2).summable_of_eq_zero_or_self

Result:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
cases h : f n <;> simp [h]

Result:
no goals

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b

Tactic:
intro n

Result:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
    (hy : f x' ∈ (chartAt H' y).source) :
    ContMDiffAt I I' n f x' ↔
      ContinuousAt f x' ∧
        ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (range I)
          (extChartAt I x x') :=
  (contMDiffWithinAt_iff_of_mem_source hx hy).trans <| by
    rw [continuousWithinAt_univ, preimage_univ, univ_inter]

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x' : M
y : M'
hx : x' ∈ (chartAt H x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f univ x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
rw [continuousWithinAt_univ, preimage_univ, univ_inter]

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem one_add_natPred (n : ℕ+) : 1 + n.natPred = n

Proof state:
n : ℕ+
⊢ 1 + n.natPred = ↑n

Tactic:
rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply_symm s_mble]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem MeasureTheory.StronglyMeasurable.integral_prod_right' [SFinite ν] ⦃f : α × β → E⦄
    (hf : StronglyMeasurable f) : StronglyMeasurable fun x => ∫ y, f (x, y) ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α × β → E
hf : StronglyMeasurable (uncurry (Function.curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν

Tactic:
exact hf.integral_prod_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν

Tactic:
rw [← uncurry_curry f] at hf

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α × β → E
hf : StronglyMeasurable (uncurry (Function.curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsert_snd_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
    (m.containsThenInsert a b).2 = (Raw₀.containsThenInsert ⟨m, h.size_buckets_pos⟩ a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.containsThenInsert a b).snd = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).snd.val

Tactic:
simp [Raw.containsThenInsert, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.node4L_lemma₅ {a b c d : ℕ} (lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9)
    (mr₁ : 2 * d ≤ b + c + 1) (mm₂ : c ≤ 3 * b) : c + d + 1 ≤ 3 * (a + b + 1)

Proof state:
a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₁ : 2 * d ≤ b + c + 1
mm₂ : c ≤ 3 * b
⊢ c + d + 1 ≤ 3 * (a + b + 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem _root_.Equiv.Perm.prod_comp (σ : Equiv.Perm α) (s : Finset α) (f : α → β)
    (hs : { a | σ a ≠ a } ⊆ s) : (∏ x ∈ s, f (σ x)) = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x

Tactic:
convert (prod_map s σ.toEmbedding f).symm

Result:
case h.e'_3.h.e'_4
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ s = map (Equiv.toEmbedding σ) s

Proof state:
case h.e'_3.h.e'_4
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ s = map (Equiv.toEmbedding σ) s

Tactic:
exact (map_perm hs).symm

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.rank_baseChange :
    Module.rank R (R ⊗[S] M') = Cardinal.lift.{u} (Module.rank S M')

Proof state:
R : Type u
S : Type u'
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : StrongRankCondition R
inst✝³ : StrongRankCondition S
inst✝² : Module S M'
inst✝¹ : Free S M'
inst✝ : Algebra S R
⊢ Module.rank R (R ⊗[S] M') = Cardinal.lift.{u, v'} (Module.rank S M')

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@[simp] lemma locallyLinear_bot : (⊥ : SimpleGraph α).LocallyLinear

Proof state:
α : Type u_1
⊢ ⊥.LocallyLinear

Tactic:
simp [LocallyLinear]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem mem_vectorSpan_pair_rev {p₁ p₂ : P} {v : V} :
    v ∈ vectorSpan k ({p₁, p₂} : Set P) ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v

Tactic:
rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem lt_logb_iff_rpow_lt (hy : 0 < y) : x < logb b y ↔ b ^ x < y

Proof state:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x < logb b y ↔ b ^ x < y

Tactic:
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_two_mul_add_two (n : ℕ) :
    fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Proof state:
n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]

Result:
n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Proof state:
n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
have : fib n ≤ 2 * fib (n + 1) :=
  le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)

Result:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Proof state:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
zify [this]

Result:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))

Proof state:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))

Tactic:
ring

Result:
no goals
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma Scheme.exists_le_and_germ_injective (X : Scheme.{u}) (x : X) [X.IsGermInjectiveAt x]
    (V : X.Opens) (hxV : x ∈ V) :
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧ U ≤ V ∧ Function.Injective (X.presheaf.germ U x hx)

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)

Result:
case intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
f : ↑Γ(X, U)
hf : X.basicOpen f ≤ V
hxf : ↑⟨x, hxV⟩ ∈ X.basicOpen f
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
exact ⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩

Result:
no goals

Proof state:
case intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx

Result:
case intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
f : ↑Γ(X, U)
hf : X.basicOpen f ≤ V
hxf : ↑⟨x, hxV⟩ ∈ X.basicOpen f
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem comap_pure {m : α → β} (a : α) (inj : Injective m) (large) :
    comap (pure <| m a) inj large = pure a :=
  coe_injective <|
    Filter.comap_pure.trans <| by
      rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

Proof state:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)

Tactic:
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.seq_tendstoUniformlyOn {l : Filter ι} (h : TendstoUniformlyOn F f l s)
    (u : ℕ → ι) (hu : Tendsto u atTop l) : TendstoUniformlyOn (fun n => F (u n)) f atTop s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q => (f q.2, F (u q.1) q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)

Tactic:
exact h.comp ((hu.comp tendsto_fst).prod_mk tendsto_snd)

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n => F (u n)) f atTop s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q => (f q.2, F (u q.1) q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem finIdxOf?_toList [BEq α] (a : α) (v : Vector α n) :
    v.toList.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast v.size_toArray.symm)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
v : Vector α n
⊢ List.finIdxOf? a v.toList = Option.map (Fin.cast ⋯) (v.finIdxOf? a)

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : Array α
⊢ List.finIdxOf? a { toArray := v, size_toArray := ⋯ }.toList =
    Option.map (Fin.cast ⋯) ({ toArray := v, size_toArray := ⋯ }.finIdxOf? a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : Array α
⊢ List.finIdxOf? a { toArray := v, size_toArray := ⋯ }.toList =
    Option.map (Fin.cast ⋯) ({ toArray := v, size_toArray := ⋯ }.finIdxOf? a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKey!_eq [BEq α] [Hashable α] [Inhabited α] {m : Raw α β} (h : m.WF) {a : α} :
    m.getKey! a = Raw₀.getKey! ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited α
m : Raw α β
h : m.WF
a : α
⊢ m.getKey! a = Raw₀.getKey! ⟨m, ⋯⟩ a

Tactic:
simp [Raw.getKey!, h.size_buckets_pos]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma isBlock_iff_smul_eq_of_nonempty :
    IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Tactic:
simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
lemma freeOn_rankPos (hE : E.Nonempty) : RankPos (freeOn E)

Proof state:
α : Type u_1
E : Set α
hE : E.Nonempty
⊢ (freeOn E).RankPos

Tactic:
simp [rankPos_iff, hE.ne_empty.symm]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_core_res (f : α → β) (s : Set α) (t : Set β) (x : α) :
    x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t

Tactic:
simp [mem_core, mem_res]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x

Proof state:
α : Type u_1
i : Nat
x : α
l : List α
⊢ (i, x) ∈ l.enum ↔ l[i]? = some x

Tactic:
simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[simp]
lemma map_add_inv_app (a b : A) (X : C) :
    F.map ((add hF s i a b).inv.app X) =
      (i b).hom.app ((s a).obj X) ≫ ((i a).hom.app X)⟦b⟧' ≫
        (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                  𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X)))) ≫
                (shiftFunctor D b).map ((i a).hom.app X)) ≫
              𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            (shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
          (i (a + b)).inv.app X)) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Tactic:
dsimp [add]

Result:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                  𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X)))) ≫
                (shiftFunctor D b).map ((i a).hom.app X)) ≫
              𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            (shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
          (i (a + b)).inv.app X)) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_hom_inv_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv =
    (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i

Tactic:
simp

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Tactic:
rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]

Result:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma pi_norm_sq (x : C⋆ᵐᵒᵈ (Π i, E i)) : ‖x‖ ^ 2 = ‖∑ i, ⟪x i, x i⟫_A‖

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ^ 2 = ‖∑ i : ι, ⟪x i, x i⟫_A‖

Tactic:
simp [pi_norm]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
`m ≥ 2` is less than `m ^ n`. -/
lemma Nat.geomSum_lt (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k ∈ s, m ^ k < m ^ n :=
  calc
    ∑ k ∈ s, m ^ k ≤ ∑ k ∈ range n, m ^ k := sum_le_sum_of_subset fun _ hk ↦
      mem_range.2 <| hs _ hk
    _ = (m ^ n - 1) / (m - 1) := Nat.geomSum_eq hm _
    _ ≤ m ^ n - 1 := Nat.div_le_self _ _
    _ < m ^ n := tsub_lt_self (by positivity) zero_lt_one

Proof state:
m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < m ^ n

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j

Proof state:
i j k : Int
⊢ i - k = j - k ↔ i = j

Tactic:
simp [Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem normalize?_eq_some (w : normalize? (s, x) = some (s', x')) :
    normalizeConstraint s x = s' ∧ normalizeCoeffs s x = x'

Proof state:
s : Constraint
x : Coeffs
s' : Constraint
x' : Coeffs
w : normalize? (s, x) = some (s', x')
⊢ normalizeConstraint s x = s' ∧ normalizeCoeffs s x = x'

Tactic:
simp_all [normalizeConstraint, normalizeCoeffs, normalize]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
theorem exists_measurableEmbedding_real : ∃ f : α → ℝ, MeasurableEmbedding f

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
⊢ ∃ f, MeasurableEmbedding f

Tactic:
obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ ↑s
⊢ ∃ f, MeasurableEmbedding f

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ ↑s
⊢ ∃ f, MeasurableEmbedding f

Tactic:
exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelIso_hom_π {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π _

Proof state:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π f

Tactic:
simp [explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[simp] lemma take_get (h : m < (a.take n).length) : (a.take n)[m] = a.get m

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m

Tactic:
rw [get_append_left]

Result:
no goals

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = a.get m

Tactic:
nth_rw 2 [← append_take_drop n a]

Result:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_span_finset_le_card (s : Finset M) : (s : Set M).finrank R ≤ s.card :=
  calc
    (s : Set M).finrank R ≤ (s : Set M).toFinset.card := finrank_span_le_card (M := M) s
    _ = s.card

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
⊢ (↑s).toFinset.card = s.card

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : (x ^ n).toNNReal = x.toNNReal ^ n

Proof state:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
  Real.coe_toNNReal x hx]

Result:
no goals