harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma shift_neg (a : ℤ) :
    (-γ).shift a = -γ.shift a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
⊢ (shiftAddHom K L n a) (-γ) = -γ.shift a

Tactic:
apply _root_.map_neg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
⊢ (-γ).shift a = -γ.shift a

Tactic:
change shiftAddHom K L n a (-γ) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
⊢ (shiftAddHom K L n a) (-γ) = -γ.shift a
-- Mathlib/Topology/Perfect.lean
theorem preperfect_iff_nhds : Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
⊢ Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Tactic:
simp only [Preperfect, accPt_iff_nhds]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem pullbackIsoPullback_inv_fst :
    (pullbackIsoPullback f g).inv ≫ pullback.fst _ _ = fun p => (p.1 : X × Y).fst

Proof state:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = fun p => (↑p).1

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma lt_sub_one_iff {k : Fin (n + 2)} : k < k - 1 ↔ k = 0

Proof state:
n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0

Proof state:
x y : Nat
⊢ ite (0 < y ∧ y ≤ x) ((x - y).div y + 1) 0 = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0

Tactic:
rfl

Result:
no goals

Proof state:
x y : Nat
⊢ x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0

Tactic:
show Nat.div x y = _

Result:
x y : Nat
⊢ x.div y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0

Proof state:
x y : Nat
⊢ x.div y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0

Tactic:
rw [Nat.div]

Result:
x y : Nat
⊢ ite (0 < y ∧ y ≤ x) ((x - y).div y + 1) 0 = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.aestronglyMeasurable_union_iff [PseudoMetrizableSpace β] {s t : Set α} :
    AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
      AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
s t : Set α
⊢ AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aestronglyMeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_vsub_right (p₁ p₂ : P) : midpoint R p₁ p₂ -ᵥ p₂ = (⅟ 2 : R) • (p₁ -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ : P
⊢ midpoint R p₁ p₂ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
rw [midpoint_comm, midpoint_vsub_left]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem measure_lt_top_of_memLp_indicator (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) {c : E} (hc : c ≠ 0)
    {s : Set α} (hs : MeasurableSet s) (hcs : MemLp ((const α c).piecewise s hs (const α 0)) p μ) :
    μ s < ⊤

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
this : support ⇑(const α c) = Set.univ
⊢ μ s < ⊤

Tactic:
simpa only [memLp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support,
  support_indicator, Set.inter_univ, this] using hcs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
⊢ μ s < ⊤

Tactic:
have : Function.support (const α c) = Set.univ := Function.support_const hc

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
this : support ⇑(const α c) = Set.univ
⊢ μ s < ⊤
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ofReal_mul_neg_iff (x : ℝ) (z : K) :
    x * z < 0 ↔ (x < 0 ∧ 0 < z) ∨ (0 < x ∧ z < 0)

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ ↑x * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0

Tactic:
simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma isOpen_sphere {r : ℝ} (hr : r ≠ 0) : IsOpen (sphere x r)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (sphere x r)

Tactic:
rw [← closedBall_diff_ball, sdiff_eq]

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r ⊓ (ball x r)ᶜ)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r ⊓ (ball x r)ᶜ)

Tactic:
exact (isOpen_closedBall x hr).inter (isClosed_ball x r).isOpen_compl

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_sub [DecidableEq α] [AddGroup G] {f g : α →₀ G} :
    support (f - g) ⊆ support f ∪ support g

Proof state:
α : Type u_1
G : Type u_9
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support

Tactic:
rw [sub_eq_add_neg, ← support_neg g]

Result:
α : Type u_1
G : Type u_9
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support

Proof state:
α : Type u_1
G : Type u_9
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support

Tactic:
exact support_add

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

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

Tactic:
rw [Int.add_left_neg, ← add_bmod_bmod, Int.add_left_neg]

Result:
no goals

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

Tactic:
apply (bmod_add_cancel_right x).mp

Result:
x : Int
n : Nat
⊢ (-x.bmod n + x).bmod n = (-x + x).bmod n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂) :
    (l₁ ++ l₂).insert a = l₁.insert a ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₂
⊢ List.insert a (l₁ ++ l₂) = List.insert a l₁ ++ l₂

Tactic:
simp [insert_append, h]

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem LieModule.compLieHom [Module R M] [LieModule R L₂ M] :
    @LieModule R L₁ M _ _ _ _ _ (LieRingModule.compLieHom M f) :=
  { __ := LieRingModule.compLieHom M f
    smul_lie := fun t x m => by
      simp only [LieRingModule.compLieHom_apply, smul_lie, LieHom.map_smul]
    lie_smul := fun t x m => by
      simp only [LieRingModule.compLieHom_apply, lie_smul] }

Proof state:
R : Type u
L₁ : Type v
L₂ : Type w
M : Type w₁
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst✝¹ : Module R M
inst✝ : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, lie_smul]

Result:
no goals

Proof state:
R : Type u
L₁ : Type v
L₂ : Type w
M : Type w₁
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst✝¹ : Module R M
inst✝ : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, smul_lie, LieHom.map_smul]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).FG ↔ S.FG :=
  ⟨fun h ↦ by
    rw [← S.range_val, ← Algebra.map_top]
    exact FG.map _ h, fun h ↦
    fg_of_fg_map _ S.val Subtype.val_injective <| by
      rw [Algebra.map_top, range_val]
      exact h⟩

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ⊤.FG
⊢ (map S.val ⊤).FG

Tactic:
exact FG.map _ h

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ (map S.val ⊤).FG

Tactic:
rw [Algebra.map_top, range_val]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.FG

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ⊤.FG
⊢ S.FG

Tactic:
rw [← S.range_val, ← Algebra.map_top]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ⊤.FG
⊢ (map S.val ⊤).FG

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.FG

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nsmul_add [AddCommMonoid G] [AddMonoid H] [AddConstMapClass F G H a b]
    (f : F) (n : ℕ) (x : G) : f (n • a + x) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
rw [add_comm, map_add_nsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
  ext_getElem hl (by simp_all)

Proof state:
α : Type u_1
l₁ l₂ : List α
hl : l₁.length = l₂.length
h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
⊢ ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_sub_Ico_left (a b c : α) : Ico a b - Ico a c = Ico (max a c) b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico a c = Ico (a ⊔ c) b

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_smul :
    mpullback I I' f (c • V) = c • mpullback I I' f V

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
c : 𝕜
x : M
⊢ mpullback I I' f (c • V) x = (c • mpullback I I' f V) x

Tactic:
simp [mpullback_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullback I I' f (c • V) = c • mpullback I I' f V

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
c : 𝕜
x : M
⊢ mpullback I I' f (c • V) x = (c • mpullback I I' f V) x
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
@[simp]
lemma coe_map_mul_map_inv (g : GL n R) : g.val.map f * g.val⁻¹.map f = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g * (↑g)⁻¹).map ⇑f = 1

Tactic:
simp only [isUnits_det_units, mul_nonsing_inv, map_zero, _root_.map_one, Matrix.map_one]

Result:
no goals

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1

Tactic:
rw [← Matrix.map_mul]

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g * (↑g)⁻¹).map ⇑f = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_neg_eq_ite {x : BitVec w} :
    (-x).toInt = if x = intMin w then x.toInt else -(x.toInt)

Proof state:
w : Nat
x : BitVec w
⊢ (-x).toInt = if x = intMin w then x.toInt else -x.toInt

Tactic:
by_cases hx : x = intMin w <;>
  simp [hx, neg_intMin, toInt_neg_of_ne_intMin]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem isUnit_of_subsingleton [Monoid M] [Subsingleton M] (a : M) : IsUnit a :=
  ⟨⟨a, a, by subsingleton, by subsingleton⟩, rfl⟩

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : M
⊢ a * a = 1

Tactic:
subsingleton

Result:
no goals
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem lt_of_le [OrderedCancelAddCommMonoid α] (p : (a:α) ≤ b) (H : a' + b < b' + a) :
    a' < b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ b' + a ≤ b' + b

Tactic:
apply add_le_add_left p

Result:
no goals

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' + b < b' + b

Tactic:
apply H.trans_le

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ b' + a ≤ b' + b

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' < b'

Tactic:
rw [← add_lt_add_iff_right b]

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' + b < b' + b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_zero : range' s 0 step = #[]

Proof state:
s step : Nat
⊢ range' s 0 step = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem subset_closedBall_norm [NormOneClass A] (a : A) : σ a ⊆ Metric.closedBall (0 : 𝕜) ‖a‖ :=
  fun k hk => by simp [norm_le_norm_of_mem hk]

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
hk : k ∈ σ a
⊢ k ∈ Metric.closedBall 0 ‖a‖

Tactic:
simp [norm_le_norm_of_mem hk]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
@[to_additive]
lemma isTorsionFree_iff_torsion_eq_bot {G} [CommGroup G] :
    IsTorsionFree G ↔ CommGroup.torsion G = ⊥

Proof state:
G : Type u_3
inst✝ : CommGroup G
⊢ IsTorsionFree G ↔ CommGroup.torsion G = ⊥

Tactic:
rw [IsTorsionFree, eq_bot_iff, SetLike.le_def]

Result:
G : Type u_3
inst✝ : CommGroup G
⊢ (∀ (g : G), g ≠ 1 → ¬IsOfFinOrder g) ↔ ∀ ⦃x : G⦄, x ∈ CommGroup.torsion G → x ∈ ⊥

Proof state:
G : Type u_3
inst✝ : CommGroup G
⊢ (∀ (g : G), g ≠ 1 → ¬IsOfFinOrder g) ↔ ∀ ⦃x : G⦄, x ∈ CommGroup.torsion G → x ∈ ⊥

Tactic:
simp [not_imp_not, CommGroup.mem_torsion]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
/-- A multifork `c : Multifork I` in the category of types is limit iff the
map `c.toSections : c.pt → I.sections` is a bijection. -/
lemma isLimit_types_iff : Nonempty (IsLimit c) ↔ Function.Bijective c.toSections

Proof state:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ Nonempty (IsLimit c) ↔ Function.Bijective c.toSections

Tactic:
rw [Types.isLimit_iff_bijective_sectionOfCone, ← toSections_fac, EquivLike.comp_bijective]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
@[simp]
lemma preimage_id (G : Subpresheaf F) :
    G.preimage (𝟙 F) = G

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ G.preimage (𝟙 F) = G

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem xor_comm : ∀ (x y : Bool), (x ^^ y) = (y ^^ x)

Proof state:
⊢ ∀ (x y : Bool), (x ^^ y) = (y ^^ x)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_comp_add_right (a : E) :
    DifferentiableWithinAt 𝕜 (fun x ↦ f (x + a)) s x ↔
      DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ DifferentiableWithinAt 𝕜 (fun x => f (x + a)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_right]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UInt.lean
theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits

Proof state:
⊢ size = 2 ^ System.Platform.numBits

Tactic:
rw [USize.size]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem concat_eq_append (as : List α) (a : α) : as.concat a = as ++ [a]

Proof state:
α : Type u
as : List α
a : α
⊢ as.concat a = as ++ a :: nil

Tactic:
induction as <;> simp [concat, *]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem nonPrincipals_eq_empty_iff : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

Proof state:
R : Type u
inst✝ : CommRing R
⊢ nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

Tactic:
simp [Set.eq_empty_iff_forall_not_mem, isPrincipalIdealRing_iff, nonPrincipals_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj [LinearOrderedField R] (x : V → R) :
    Matrix.toLinearMap₂' R (G.lapMatrix R) x x = 0 ↔ ∀ i j : V, G.Adj i j → x i = x j

Proof state:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : LinearOrderedField R
x : V → R
⊢ (((toLinearMap₂' R) (lapMatrix R G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j

Tactic:
simp (disch := intros; positivity)
  [lapMatrix_toLinearMap₂', sum_eq_zero_iff_of_nonneg, sub_eq_zero]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_lt {x y : PartENat} : withTopEquiv x < withTopEquiv y ↔ x < y

Proof state:
x y : PartENat
⊢ withTopEquiv x < withTopEquiv y ↔ x < y

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_inj : G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma univ_div_univ [Fintype α] : (univ / univ : Finset α) = univ

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : DivisionMonoid α
inst✝ : Fintype α
⊢ univ / univ = univ

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Dynamics/Flow.lean
theorem isInvariant_iff_image : IsInvariant ϕ s ↔ ∀ t, ϕ t '' s ⊆ s

Proof state:
τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s

Tactic:
simp_rw [IsInvariant, mapsTo']

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[bound]
lemma div_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 :=
  div_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b

Tactic:
rwa [one_mul]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
    volume A = 2 ^ nrRealPlaces K * volume (plusPart A)

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
hm : MeasurableSet A
⊢ volume A = 2 ^ nrRealPlaces K * volume (plusPart A)

Tactic:
simp only [← measure_congr (iUnion_negAt_plusPart_ae A hA),
  measure_iUnion (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
  volume_negAt_plusPart _ hm, tsum_fintype, sum_const, card_univ, Fintype.card_set, nsmul_eq_mul,
  Nat.cast_pow, Nat.cast_ofNat, nrRealPlaces]

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem UCompactlyGeneratedSpace.isOpen [UCompactlyGeneratedSpace.{u} X] {s : Set X}
    (hs : ∀ (S : CompHaus.{u}) (f : C(S, X)), IsOpen (f ⁻¹' s)) : IsOpen s

Proof state:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        ((fun x =>
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s))

Tactic:
exact fun ⟨S, f⟩ ↦ hs S f

Result:
no goals

Proof state:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced,
  isOpen_sigma_iff]

Result:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        ((fun x =>
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s))
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_surjective_eq_zero_iff :
    #{f : α → β | Surjective f} = 0 ↔ #α < #β ∨ (#α ≠ 0 ∧ #β = 0)

Proof state:
α β : Type u
⊢ #↑{f | Surjective f} = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0

Tactic:
rw [mk_surjective_eq_zero_iff_lift, lift_lt]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem MonoidHom.comp_id_grp {G : Grp.{u}} {H : Type u} [Monoid H] (f : G →* H) :
    f.comp (Grp.Hom.hom (𝟙 G)) = f

Proof state:
G : Grp
H : Type u
inst✝ : Monoid H
f : ↑G →* H
⊢ f.comp (Grp.Hom.hom (𝟙 G)) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorial/BigOperators.lean
theorem ascFactorial_eq_prod_range (n : ℕ) : ∀ k, n.ascFactorial k = ∏ i ∈ range k, (n + i)
  | 0 => rfl
  | k + 1 => by rw [ascFactorial, prod_range_succ, mul_comm, ascFactorial_eq_prod_range n k]

Proof state:
n k : ℕ
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)

Tactic:
rw [ascFactorial, prod_range_succ, mul_comm, ascFactorial_eq_prod_range n k]

Result:
no goals