harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem MeasurableSet.of_union_cover {s t u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (h : univ ⊆ s ∪ t) (hsu : MeasurableSet (((↑) : s → α) ⁻¹' u))
    (htu : MeasurableSet (((↑) : t → α) ⁻¹' u)) : MeasurableSet u

Proof state:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ u = Subtype.val '' (Subtype.val ⁻¹' u) ∪ Subtype.val '' (Subtype.val ⁻¹' u)

Tactic:
simp [image_preimage_eq_inter_range, ← inter_union_distrib_left, univ_subset_iff.1 h]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ MeasurableSet u

Tactic:
convert (hs.subtype_image hsu).union (ht.subtype_image htu)

Result:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ u = Subtype.val '' (Subtype.val ⁻¹' u) ∪ Subtype.val '' (Subtype.val ⁻¹' u)
-- Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean
lemma isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) :
    IsPullback c.fst.left c.snd.left Y.hom Z.hom :=
  ⟨by simp, ⟨((IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).symm
    ((IsLimit.ofConeEquiv (ConstructProducts.conesEquiv X _).symm).symm hc)).ofIsoLimit
    (PullbackCone.isoMk _)⟩⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y Z : Over X
c : BinaryFan Y Z
hc : IsLimit c
⊢ CommSq c.fst.left c.snd.left Y.hom Z.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_smul_nonzero [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
    (a • p).aroots S = p.aroots S

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (a • p).aroots S = p.aroots S

Tactic:
rw [smul_eq_C_mul, aroots_C_mul _ ha]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.DifferentiableWithinAt.lieBracketWithin_congr_mono
    (hV : DifferentiableWithinAt 𝕜 V s x) (hVs : EqOn V₁ V t) (hVx : V₁ x = V x)
    (hW : DifferentiableWithinAt 𝕜 W s x) (hWs : EqOn W₁ W t) (hWx : W₁ x = W x)
    (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) :
    lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : DifferentiableWithinAt 𝕜 W s x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueDiffWithinAt 𝕜 t x
h₁ : t ⊆ s
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, hV.fderivWithin_congr_mono, hW.fderivWithin_congr_mono, hVs, hVx,
  hWs, hWx, hxt, h₁]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem colimit_sound {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j')
    (w : F.map f x = x') : colimit.ι F j x = colimit.ι F j' x'

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w : F.map f x = x'
⊢ colimit.ι F j x = colimit.ι F j' x'

Tactic:
rw [← w, Colimit.w_apply]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem eq_div_of_mul_eq_right {a b c : R} (ha : a ≠ 0) (h : a * b = c) : b = c / a

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = c / a

Tactic:
rw [← h, mul_div_cancel_left₀ _ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_singleton' (l : List α) : (l.flatMap fun x => [x]) = l

Proof state:
α : Type u_1
l : List α
⊢ flatMap (fun x => [x]) l = l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Cardinal.lean
theorem cardinalMk_eq [IsEmpty σ] : #(MvPolynomial σ R) = #R

Proof state:
σ R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) = #R

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
    m.contains a = true → m.get? a = some (m.getD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ m.contains a = true → m.get? a = some (m.getD a fallback)

Tactic:
simp_to_model using List.getValueCast?_eq_some_getValueCastD

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem eval_relabel {r : α → β} {a : β → Bool} {c : Clause α} :
    (relabel r c).eval a = c.eval (a ∘ r)

Proof state:
α : Type u_1
β : Type u_2
r : α → β
a : β → Bool
c : Clause α
⊢ eval a (relabel r c) = eval (a ∘ r) c

Tactic:
induction c <;> simp_all [relabel]

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_diagonal_diagonal [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n]
    (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : m → α) (b : n → β) :
    kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2)

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
m : Type u_9
n : Type u_10
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
m : Type u_9
n : Type u_10
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
m : Type u_9
n : Type u_10
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem one_nmul (a) : 1 ⨳ a = a

Proof state:
a : Ordinal.{u_1}
⊢ 1 ⨳ a = a

Tactic:
rw [nmul_comm, nmul_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.takeUntil {u v w : V} {p : G.Walk v w} (hc : p.IsTrail)
    (h : u ∈ p.support) : (p.takeUntil u h).IsTrail :=
  IsTrail.of_append_left (q := p.dropUntil u h) (by rwa [← take_spec _ h] at hc)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
rwa [← take_spec _ h] at hc

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem of_f {i j : ι} {hij : i ≤ j} {x : G i} : of L ι G f j (f i j hij x) = of L ι G f i x

Proof state:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)

Tactic:
refine Setoid.symm ⟨j, hij, refl j, ?_⟩

Result:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (f i j hij) x = (f j j ⋯) ((f i j hij) x)

Proof state:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (of L ι G f j) ((f i j hij) x) = (of L ι G f i) x

Tactic:
rw [of_apply, of_apply, Quotient.eq]

Result:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)

Proof state:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (f i j hij) x = (f j j ⋯) ((f i j hij) x)

Tactic:
simp only [DirectedSystem.map_self]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem NeBot.eq_pure_iff (hf : f.NeBot) {x : α} :
    f = pure x ↔ {x} ∈ f

Proof state:
α : Type u
f : Filter α
hf : f.NeBot
x : α
⊢ f = pure x ↔ {x} ∈ f

Tactic:
rw [← hf.le_pure_iff, le_pure_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem setLIntegral_compProd_univ_left (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : Measurable f) {t : Set γ}
    (ht : MeasurableSet t) :
    ∫⁻ z in Set.univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ x, ∫⁻ y in t, f (x, y) ∂η (a, x) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
t : Set γ
ht : MeasurableSet t
⊢ ∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [setLIntegral_compProd κ η a hf MeasurableSet.univ ht, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
theorem coverEntropy_restrict [UniformSpace X] {T : X → X} {F : Set X} (h : MapsTo T F F) :
    coverEntropy (h.restrict T F F) univ = coverEntropy T F

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
⊢ coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy T F

Tactic:
rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma neg_vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* (-A) = v ᵥ* A

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* -A = v ᵥ* A

Tactic:
rw [vecMul_neg, neg_vecMul, neg_neg]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f)
    (s : ι → NonUnitalSubsemiring R) :
    (map f (iInf s) : NonUnitalSubsemiring S) = ⨅ i, map f (s i)

Proof state:
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_mkArray_mkArray : (mkArray n (mkArray m a)).flatten = mkArray (n * m) a

Proof state:
n m : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n (mkArray m a)).flatten = mkArray (n * m) a

Tactic:
rw [← toList_inj]

Result:
n m : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n (mkArray m a)).flatten.toList = (mkArray (n * m) a).toList

Proof state:
n m : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n (mkArray m a)).flatten.toList = (mkArray (n * m) a).toList

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Polynomial.lean
theorem _root_.Algebra.adjoin_singleton_eq_range_aeval (x : A) :
    Algebra.adjoin R {x} = (Polynomial.aeval x).range

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ Algebra.adjoin R {x} = (aeval x).range

Tactic:
rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h)

Proof state:
case cons
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : β), a ∈ map f tail✝ → p a), pmap g (map f tail✝) H = pmap (fun a h => g (f a) h) tail✝ ⋯
H : ∀ (a : β), a ∈ map f (head✝ :: tail✝) → p a
⊢ pmap g (map f (head✝ :: tail✝)) H = pmap (fun a h => g (f a) h) (head✝ :: tail✝) ⋯

Tactic:
simp only [*, pmap, map]

Result:
no goals

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
l : List α
H : ∀ (a : β), a ∈ map f l → p a
⊢ pmap g (map f l) H = pmap (fun a h => g (f a) h) l ⋯

Tactic:
induction l

Result:
case nil
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
H : ∀ (a : β), a ∈ map f [] → p a
⊢ pmap g (map f []) H = pmap (fun a h => g (f a) h) [] ⋯

case cons
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : β), a ∈ map f tail✝ → p a), pmap g (map f tail✝) H = pmap (fun a h => g (f a) h) tail✝ ⋯
H : ∀ (a : β), a ∈ map f (head✝ :: tail✝) → p a
⊢ pmap g (map f (head✝ :: tail✝)) H = pmap (fun a h => g (f a) h) (head✝ :: tail✝) ⋯

Proof state:
case nil
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
H : ∀ (a : β), a ∈ map f [] → p a
⊢ pmap g (map f []) H = pmap (fun a h => g (f a) h) [] ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) :
    (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by simp; omega⟩

Proof state:
α : Type ?u.45246
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo l).snd.val.length = n / 2

Tactic:
simp

Result:
α : Type ?u.45246
n : Nat
l : { l // l.length = n }
⊢ l.val.length - (n + 1) / 2 = n / 2

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitRevInTwo l).snd = ⟨(splitInTwo l).snd.val, ⋯⟩

Tactic:
simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd]

Result:
no goals

Proof state:
α : Type ?u.45246
n : Nat
l : { l // l.length = n }
⊢ l.val.length - (n + 1) / 2 = n / 2

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem pair_eq_mk (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
    f.pair g =
      mk (fun x => (f x, g x)) (f.aestronglyMeasurable.prod_mk g.aestronglyMeasurable)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ f.pair g = mk (fun x => (↑f x, ↑g x)) ⋯

Tactic:
simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_neg_left : IsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g

Tactic:
simp only [IsBigOWith_def, norm_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
/-- For the versions of this lemma where `μ.singularPart ν` or `ν.withDensity (μ.rnDeriv ν)` are
isolated, see `MeasureTheory.Measure.measure_sub_singularPart` and
`MeasureTheory.Measure.measure_sub_rnDeriv`. -/
lemma rnDeriv_add_singularPart (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] :
    ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ

Tactic:
rw [add_comm, singularPart_add_rnDeriv]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem comp_zero (g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 :=
  ext fun c ↦ by rw [comp_apply, zero_apply, zero_apply, g.map_zero]

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ (g.comp 0) c = 0 c

Tactic:
rw [comp_apply, zero_apply, zero_apply, g.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_eq_none_iff {xs : List α} : xs.getLast? = none ↔ xs = []

Proof state:
α : Type u_1
xs : List α
⊢ xs.getLast? = none ↔ xs = []

Tactic:
rw [getLast?_eq_head?_reverse, head?_eq_none_iff, reverse_eq_nil_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_two_zsmul_eq_sign_iff {θ : Angle} :
    ((2 : ℤ) • θ).sign = θ.sign ↔ θ = π ∨ |θ.toReal| < π / 2

Proof state:
θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_le_of_injective_injective [AddCommGroup M₁] [Module R' M₁]
    (i : R' → R) (j : M →+ M₁) (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Module.rank R M ≤ Module.rank R' M₁

Proof state:
R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M₁
inst✝ : Module R' M₁
i : R' → R
j : M →+ M₁
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem iterate_pos_le_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) :
    f^[n] x ≤ x + n * m ↔ f x ≤ x + m

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_le_iff_map_le f.monotone (strictMono_id.add_const (m : ℝ)) hn

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_eq_image₂ (x y : E) :
    openSegment 𝕜 x y =
      (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' { p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1 }

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = (fun p => p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
simp only [openSegment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepSets_zero_left : IndepSets s1 s2 (0 : Kernel α Ω) μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s1 s2 : Set (Set Ω)
⊢ IndepSets s1 s2 0 μ

Tactic:
simp [IndepSets]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_def (f : ι → E) (n : ι) :
    gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt 𝕜 f i) (f n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
⊢ gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))

Tactic:
rw [← sum_attach, attach_eq_univ, gramSchmidt]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem biInter_basis_nhds [T1Space X] {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (h : (𝓝 x).HasBasis p s) : ⋂ (i) (_ : p i), s i = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ ⋂ i, ⋂ (_ : p i), s i = {x}

Tactic:
rw [← h.ker, ker_nhds]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma setLIntegral_indicator {s t : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ a in t, s.indicator f a ∂μ = ∫⁻ a in s ∩ t, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
rw [lintegral_indicator hs, Measure.restrict_restrict hs]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_mod (l : List α) (n : ℕ) : l.rotate (n % l.length) = l.rotate n

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate (n % l.length) = l.rotate n

Tactic:
simp [rotate]

Result:
no goals
-- Mathlib/Data/Rat/Sqrt.lean
theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ Rat.sqrt x * Rat.sqrt x = x :=
  ⟨fun ⟨n, hn⟩ => by rw [← hn, sqrt_eq, abs_mul_abs_self], fun h => ⟨Rat.sqrt x, h⟩⟩

Proof state:
x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, abs_mul_abs_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_mul_natCast (hx : 0 ≤ x) (y : ℝ) (n : ℕ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul hx, rpow_natCast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_pi_div_two_sub (θ : Angle) : cos (↑(π / 2) - θ) = sin θ

Proof state:
θ : Angle
⊢ (↑(π / 2) - θ).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑(π / 2) - ↑x✝).cos = (↑x✝).sin

Proof state:
case h
x✝ : ℝ
⊢ (↑(π / 2) - ↑x✝).cos = (↑x✝).sin

Tactic:
exact Real.cos_pi_div_two_sub _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_swapAt (a : Vector α n) (i x h) :
    ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) =
      ((a.toArray.swapAt i x (by simpa using h)).fst,
        (a.toArray.swapAt i x (by simpa using h)).snd) := rfl

Proof state:
α : Type ?u.48057
n : Nat
a : Vector α n
i : Nat
x : α
h : i < n
⊢ i < a.size

Tactic:
simpa using h

Result:
no goals