harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/DirectSum/Idempotents.lean
theorem completeOrthogonalIdempotents_idempotent [Fintype I]:
    CompleteOrthogonalIdempotents (idempotent V) where
  idem := isIdempotentElem_idempotent V
  ortho i j hij

Proof state:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ (fun x1 x2 => idempotent V x1 * idempotent V x2 = 0) i j

Tactic:
simp only

Result:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ idempotent V i * idempotent V j = 0

Proof state:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
⊢ (decompose V) (∑ i : I, idempotent V i) = (decompose V) 1

Tactic:
refine DFunLike.ext _ _ fun i ↦ ?_

Result:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ((decompose V) (∑ i : I, idempotent V i)) i = ((decompose V) 1) i

Proof state:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
⊢ ∑ i : I, idempotent V i = 1

Tactic:
apply (decompose V).injective

Result:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
⊢ (decompose V) (∑ i : I, idempotent V i) = (decompose V) 1

Proof state:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ idempotent V i * idempotent V j = 0

Tactic:
rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
  of_eq_of_ne (h := hij), Submodule.coe_zero]

Result:
no goals

Proof state:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ∑ a : I, ((decompose V) (idempotent V a)) i = ((decompose V) 1) i

Tactic:
simp [idempotent, of_apply]

Result:
no goals

Proof state:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ((decompose V) (∑ i : I, idempotent V i)) i = ((decompose V) 1) i

Tactic:
rw [decompose_sum, DFinsupp.finset_sum_apply]

Result:
case a
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ∑ a : I, ((decompose V) (idempotent V a)) i = ((decompose V) 1) i
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_compl (hs : MeasurableSet s) (hfi : Integrable f μ) :
    ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ - ∫ x in s, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : Integrable f μ
⊢ ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← integral_add_compl (μ := μ) hs hfi, add_sub_cancel_left]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_oreDiv (r : R) (x : X) (s : S) :
    r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Proof state:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Tactic:
with_unfolding_all rfl

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem le_isGLB_iff (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ lowerBounds s

Tactic:
rw [h.lowerBounds_eq]

Result:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem nilradical_eq_bot_iff {R : Type*} [CommSemiring R] : nilradical R = ⊥ ↔ IsReduced R

Proof state:
R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R = ⊥ ↔ IsReduced R

Tactic:
simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_comp_subtypeL_eq_zero_iff {U V : Submodule 𝕜 E}
    [HasOrthogonalProjection U] : orthogonalProjection U ∘L V.subtypeL = 0 ↔ U ⟂ V :=
  ⟨fun h u hu v hv => by
    convert orthogonalProjection_inner_eq_zero v u hu using 2
    have : orthogonalProjection U v = 0 := DFunLike.congr_fun h (⟨_, hv⟩ : V)
    rw [this, Submodule.coe_zero, sub_zero], Submodule.IsOrtho.orthogonalProjection_comp_subtypeL⟩

Proof state:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
h : (orthogonalProjection U).comp V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ v = v - ↑((orthogonalProjection U) v)

Tactic:
have : orthogonalProjection U v = 0 := DFunLike.congr_fun h (⟨_, hv⟩ : V)

Result:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
h : (orthogonalProjection U).comp V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
this : (orthogonalProjection U) v = 0
⊢ v = v - ↑((orthogonalProjection U) v)

Proof state:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
h : (orthogonalProjection U).comp V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
this : (orthogonalProjection U) v = 0
⊢ v = v - ↑((orthogonalProjection U) v)

Tactic:
rw [this, Submodule.coe_zero, sub_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
h : (orthogonalProjection U).comp V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ ⟪v, u⟫_𝕜 = 0

Tactic:
convert orthogonalProjection_inner_eq_zero v u hu using 2

Result:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
h : (orthogonalProjection U).comp V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ v = v - ↑((orthogonalProjection U) v)
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem approx_eta {n : ℕ} (x : CofixA F (n + 1)) : x = CofixA.intro (head' x) (children' x)

Proof state:
F : PFunctor.{u}
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)

Tactic:
cases x

Result:
case intro
F : PFunctor.{u}
n : ℕ
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))

Proof state:
case intro
F : PFunctor.{u}
n : ℕ
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isNilpotent_toEnd_of_isNilpotent [IsNilpotent L M] (x : L) :
    _root_.IsNilpotent (toEnd R L M x)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
⊢ ∃ k, (toEnd R L M) x ^ k = 0

Tactic:
have := exists_forall_pow_toEnd_eq_zero R L M

Result:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
this : ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ∃ k, (toEnd R L M) x ^ k = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
⊢ _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
change ∃ k, toEnd R L M x ^ k = 0

Result:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
⊢ ∃ k, (toEnd R L M) x ^ k = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
this : ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ∃ k, (toEnd R L M) x ^ k = 0

Tactic:
tauto

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_trim_ae {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ≥0∞}
    (hf : AEMeasurable f (μ.trim hm)) : ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
  lintegral_trim hm hf.measurable_mk]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_ssubset_univ [Fintype α] {s : Set α} [Fintype s] :
    s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
theorem symmetry (X Y : C) :
    (Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom ≫
        (Limits.BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom =
      𝟙 (tensorObj ℬ X Y)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫
      ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom =
    𝟙 (tensorObj ℬ X Y)

Tactic:
apply (ℬ _ _).isLimit.hom_ext

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    (((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫
          ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom) ≫
        (ℬ X Y).cone.π.app j =
      𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app j

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((ℬ Y X).isLimit.lift (BinaryFan.swap (ℬ X Y).cone) ≫ (ℬ X Y).isLimit.lift (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.snd (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.snd (ℬ X Y).cone

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom ≫ (BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom =
    𝟙 (tensorObj ℬ X Y)

Tactic:
dsimp [tensorHom, Limits.BinaryFan.braiding]

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫
      ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom =
    𝟙 (tensorObj ℬ X Y)

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫
        ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right }

Tactic:
dsimp [Limits.IsLimit.conePointUniqueUpToIso]

Result:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((ℬ Y X).isLimit.lift (BinaryFan.swap (ℬ X Y).cone) ≫ (ℬ X Y).isLimit.lift (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.snd (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.snd (ℬ X Y).cone
-- Mathlib/Data/Rel.lean
theorem preimage_bot (s : Set β) : (⊥ : Rel α β).preimage s = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set β
⊢ ⊥.preimage s = ∅

Tactic:
rw [preimage, inv_bot, image_bot]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem isCoprime_zero_left : IsCoprime 0 x ↔ IsUnit x :=
  ⟨fun ⟨a, b, H⟩ => isUnit_of_mul_eq_one x b <| by rwa [mul_zero, zero_add, mul_comm] at H, fun H =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 H
    ⟨1, b, by rwa [one_mul, zero_add]⟩⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
⊢ x * b = 1

Tactic:
rwa [mul_zero, zero_add, mul_comm] at H

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 1 * 0 + b * x = 1

Tactic:
rwa [one_mul, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/Lemmas.lean
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
    (m.insert k v).contains k

Proof state:
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
m : HashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β
⊢ (m.insert k v).contains k = true

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem limsInf_bot : limsInf (⊥ : Filter α) = ⊤ :=
  top_unique <| le_sSup <| by simp

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊤ ∈ {a | ∀ᶠ (n : α) in ⊥, a ≤ n}

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_eq_iInf : s.einfsep = ⨅ d : s.offDiag, (uncurry edist) (d : α × α)

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ⨅ d, uncurry edist ↑d

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d

Tactic:
simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a

Proof state:
case succ
a n✝ : ℕ
ha : a ≤ (n✝ + 1) / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
  ha]

Result:
no goals

Proof state:
case zero
a : ℕ
ha : a ≤ 0 / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
simp

Result:
no goals

Proof state:
n a : ℕ
ha : a ≤ n / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
cases n

Result:
case zero
a : ℕ
ha : a ≤ 0 / 2
⊢ (↑a).valMinAbs = ↑a

case succ
a n✝ : ℕ
ha : a ≤ (n✝ + 1) / 2
⊢ (↑a).valMinAbs = ↑a
-- Mathlib/Data/Sym/Basic.lean
theorem map_mk {f : α → β} {m : Multiset α} {hc : Multiset.card m = n} :
    map f (mk m hc) = mk (m.map f) (by simp [hc]) :=
  rfl

Proof state:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a b : α
f : α → β
m : Multiset α
hc : m.card = n
⊢ (Multiset.map f m).card = n

Tactic:
simp [hc]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_eq_zero_iff : ⌈a⌉ = 0 ↔ a ∈ Ioc (-1 : α) 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ = 0 ↔ a ∈ Ioc (-1) 0

Tactic:
simp [ceil_eq_iff]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem mapsTo (h : LeftInvOn f' f s) (hf : SurjOn f s t) :
    MapsTo f' t s := fun y hy => by
  let ⟨x, hs, hx⟩ := hf hy
  rwa [← hx, h hs]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s

Tactic:
let ⟨x, hs, hx⟩ := hf hy

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s

Tactic:
rwa [← hx, h hs]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem ae_uIoc_iff [LinearOrder α] {a b : α} {P : α → Prop} :
    (∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ x ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ x ∂μ, x ∈ Ioc b a → P x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x

Tactic:
simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.closure_subset_of_isOpen {K : Set X} (hK : IsCompact K)
    {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ i ∈ K, {y | Inseparable i y} ⊆ U

Tactic:
exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen U
hKU : K ⊆ U
⊢ closure K ⊆ U

Tactic:
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ i ∈ K, {y | Inseparable i y} ⊆ U
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_singleton {a : α} : mapIdx f #v[a] = #v[f 0 a]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
a : α
⊢ mapIdx f { toArray := #[a], size_toArray := ⋯ } = { toArray := #[f 0 a], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Artinian/Ring.lean
theorem isNilpotent_nilradical : IsNilpotent (nilradical R)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson 0)

Tactic:
exact isNilpotent_jacobson_bot

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (nilradical R)

Tactic:
rw [nilradical, ← jacobson_eq_radical]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson 0)
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_one' : ‖(1 : E)‖ = 0

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ = 0

Tactic:
rw [← dist_one_right, dist_self]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- Given a cocartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : b ⟶ b'` lifting `𝟙 S` such that `φ ≫ ψ = φ ≫ ψ'`. Then we must have `ψ = ψ'`. -/
protected lemma ext (φ : a ⟶ b) [IsCocartesian p f φ] {b' : 𝒳} (ψ ψ' : b ⟶ b')
    [IsHomLift p (𝟙 S) ψ] [IsHomLift p (𝟙 S) ψ'] (h : φ ≫ ψ = φ ≫ ψ') : ψ = ψ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift (𝟙 S) ψ
inst✝ : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' h.symm]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vsub_vadd_eq_vsub_sub (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g

Tactic:
rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
  add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_pos_iff_mem_nonZeroDivisors {I : Ideal S} :
    0 < absNorm I ↔ I ∈ (Ideal S)⁰

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ 0 < absNorm I ↔ I ∈ (Ideal S)⁰

Tactic:
rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.pos_iff_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem unitOfList_nil :
    unitOfList ([] : List α) = ∅

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ unitOfList [] = ∅

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty []).val.val = Raw₀.empty.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty []).val.val = Raw₀.empty.val

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey' {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} :
    (alterKey k f l).length =
      if containsKey k l && (f (getValue? k l)).isNone then
        l.length - 1
      else if !containsKey k l && (f (getValue? k l)).isSome then
        l.length + 1
      else
        l.length

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (alterKey k f l).length =
    if (containsKey k l && (f (getValue? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValue? k l)).isSome) = true then l.length + 1 else l.length

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if (containsKey k l && (f (getValue? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValue? k l)).isSome) = true then l.length + 1 else l.length

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if (containsKey k l && (f (getValue? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValue? k l)).isSome) = true then l.length + 1 else l.length

Tactic:
cases h : containsKey k l <;> split <;> split <;> simp_all [length_eraseKey, length_insertEntry]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_ofSeq (s : Seq α) : ∀ n, drop (ofSeq s) n = ofSeq (s.drop n)
  | 0 => rfl
  | n + 1 => by
    simp only [drop, Nat.add_eq, Nat.add_zero, Seq.drop]
    rw [dropn_ofSeq s n, tail_ofSeq]

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).tail = ↑(s.drop n).tail

Tactic:
rw [dropn_ofSeq s n, tail_ofSeq]

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (↑s).drop (n + 1) = ↑(s.drop (n + 1))

Tactic:
simp only [drop, Nat.add_eq, Nat.add_zero, Seq.drop]

Result:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).tail = ↑(s.drop n).tail
-- Mathlib/Topology/ContinuousOn.lean
lemma Topology.IsInducing.continuousOn_iff {f : α → β} {g : β → γ} (hg : IsInducing g)
    {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
simp_rw [ContinuousOn, hg.continuousWithinAt_iff]

Result:
no goals