harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_limsup {s : ℕ → Set α} (hs : ∀ n, MeasurableSet <| s n) :
    MeasurableSet <| Filter.limsup s Filter.atTop

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (limsup s atTop)

Tactic:
simpa only [← blimsup_true] using measurableSet_blimsup fun n _ => hs n

Result:
no goals
-- Mathlib/Data/List/InsertIdx.lean
theorem insertIdx_eraseIdx_getElem {l : List α} {n : ℕ} (hn : n < length l) :
    insertIdx n l[n] (l.eraseIdx n) = l

Proof state:
α : Type u
l : List α
n : ℕ
hn : n < l.length
⊢ insertIdx n l[n] (l.eraseIdx n) = l

Tactic:
simp [hn.ne]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma φ_snd : φ f g ≫ biprod.snd = biprod.snd ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ φ f g ≫ biprod.snd = biprod.snd ≫ g

Tactic:
dsimp [φ]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.snd = biprod.snd ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.snd = biprod.snd ≫ g

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem ext : ∀ {s t : AList β}, s.entries = t.entries → s = t
  | ⟨l₁, h₁⟩, ⟨l₂, _⟩, H => by congr

Proof state:
α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : l₁.NodupKeys
l₂ : List (Sigma β)
nodupKeys✝ : l₂.NodupKeys
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem tsum_eapproxDiff (f : α → ℝ≥0∞) (hf : Measurable f) (a : α) :
    (∑' n, (eapproxDiff f n a : ℝ≥0∞)) = f a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∑' (n : ℕ), ↑((eapproxDiff f n) a) = f a

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
  iSup_eapprox_apply hf a]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem binomial_eq [DecidableEq α] (h : a ≠ b) :
    multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)

Tactic:
simp [multinomial, Finset.sum_pair h, Finset.prod_pair h]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Filter.HasBasis.clusterPt_iff_frequently {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X}
    (hx : (𝓝 x).HasBasis p s) : ClusterPt x F ↔ ∀ i, p i → ∃ᶠ x in F, x ∈ s i

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : (𝓝 x).HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i

Tactic:
simp only [hx.clusterPt_iff F.basis_sets, Filter.frequently_iff, inter_comm (s _),
  Set.Nonempty, id, mem_inter_iff]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} :
    ¬Infinitesimal x → Infinite y → Infinite (x * y) := fun hx hy => by
  rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx

Proof state:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (x * y).Infinite

Tactic:
rw [mul_comm]

Result:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Proof state:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Tactic:
exact infinite_mul_of_infinite_not_infinitesimal hy hx

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma opcyclesMap'_sub :
    opcyclesMap' (φ - φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ -
      opcyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (φ - φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ - opcyclesMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, opcyclesMap'_add, opcyclesMap'_neg]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp, norm_cast] lemma coe_covBy_coe : (a : WithTop α) ⋖ b ↔ a ⋖ b :=
  Set.OrdConnected.apply_covBy_apply_iff OrderEmbedding.withTopCoe <| by
    simp [WithTop.range_coe, ordConnected_Iio]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (range ⇑OrderEmbedding.withTopCoe).OrdConnected

Tactic:
simp [WithTop.range_coe, ordConnected_Iio]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem setLIntegral_compProd_univ_right (κ : Kernel α β) [IsSFiniteKernel κ]
    (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : Measurable f)
    {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ z in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫⁻ x in s, ∫⁻ y, 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
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a

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

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Iio_mul_Iic_subset' [LocallyFiniteOrderBot α] (a b : α) : Iio a * Iic b ⊆ Iio (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Iio_mul_Iic_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ ↑(Iio a * Iic b) ⊆ ↑(Iio (a * b))

Tactic:
simpa using Set.Iio_mul_Iic_subset' _ _

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0

Proof state:
n : ℕ
⊢ finRange n = [] ↔ n = 0

Tactic:
rw [← length_eq_zero, length_finRange]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive (attr := simp)]
lemma covBySMul_zero : CovBySMul M 0 A B ↔ A = ∅

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
A B : Set X
⊢ CovBySMul M 0 A B ↔ A = ∅

Tactic:
simp [CovBySMul]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_Iic : Iic b \ Iic a = Ioc a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iic b \ Iic a = Ioc a b

Tactic:
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom :
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom =
      ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom =
    ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j

Tactic:
simp [singleObjCyclesSelfIso, singleObjOpcyclesSelfIso]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma app_unitForward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : Cᵒᵖ)
    (p : YonedaCollection (restrictedYonedaObj η) X.unop) :
    η.app X (unitForward η X.unop p) = p.yonedaEquivFst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : Cᵒᵖ
p : YonedaCollection (restrictedYonedaObj η) (unop X)
⊢ η.app X (unitForward η (unop X) p) = p.yonedaEquivFst

Tactic:
simpa [unitForward] using p.snd.app_val

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Colimits.lean
theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
    (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
rw [← cocone_naturality F f, comp_apply]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem map_cons (a : α) (s : Stream' α) : map f (a::s) = f a::map f s

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ map f (a :: s) = f a :: map f s

Tactic:
rw [← Stream'.eta (map f (a::s)), map_eq]

Result:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balRight (l : RBNode α) (v : α) (r : RBNode α) :
    (balRight l v r).reverse = balLeft r.reverse v l.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balRight v r).reverse = r.reverse.balLeft v l.reverse

Tactic:
rw [← reverse_reverse (balLeft ..)]

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balRight v r).reverse = (r.reverse.balLeft v l.reverse).reverse.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balRight v r).reverse = (r.reverse.balLeft v l.reverse).reverse.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_reverse_iff : l.reverse ~r l'.reverse ↔ l ~r l'

Proof state:
α : Type u
l l' : List α
⊢ l.reverse ~r l'.reverse ↔ l ~r l'

Tactic:
simp [isRotated_reverse_comm_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.inverse_comp_apply_of_left {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃}
    (hg : g.IsInvertible) : (g ∘L f).inverse v = f.inverse (g.inverse v)

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
v : M₃
hg : g.IsInvertible
⊢ (g.comp f).inverse v = f.inverse (g.inverse v)

Tactic:
simp only [hg.inverse_comp_of_left, coe_comp', Function.comp_apply]

Result:
no goals
-- Mathlib/Control/Basic.lean
theorem guard_true {h : Decidable True} : @guard F _ True h = pure ()

Proof state:
F : Type → Type v
inst✝ : Alternative F
h : Decidable True
⊢ guard True = pure ()

Tactic:
simp [guard, if_pos]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem mem_product {l₁ : List α} {l₂ : List β} {a : α} {b : β} :
    (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Tactic:
simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, exists_prop, and_left_comm,
  exists_and_left, exists_eq_left, exists_eq_right]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_function {α β : Type*} [Fintype α] [Mul β] :
    commProb (α → β) = (commProb β) ^ Fintype.card α

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α

Tactic:
rw [commProb_pi, Finset.prod_const, Finset.card_univ]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_iUnion : (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty

Proof state:
α : Type u_1
ι : Sort u_5
s : ι → Set α
⊢ (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty

Tactic:
simp [nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem some_mem_insertTop {s : Finset α} {a : α} : ↑a ∈ insertTop s ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ ↑a ∈ insertTop s ↔ a ∈ s

Tactic:
simp [insertTop]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem tendsto_const_nhds_iff [T1Space X] {l : Filter Y} [NeBot l] {c d : X} :
    Tendsto (fun _ => c) l (𝓝 d) ↔ c = d

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
l : Filter Y
inst✝ : l.NeBot
c d : X
⊢ Tendsto (fun x => c) l (𝓝 d) ↔ c = d

Tactic:
simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem lift_bind (ma : m α) (f : α → m β) :
    ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a))

Proof state:
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β ε : Type u_1
ma : m α
f : α → m β
⊢ ExceptT.lift (ma >>= f) = do
    let a ← ExceptT.lift ma
    ExceptT.lift (f a)

Tactic:
simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.lift_fst_snd {X Y : C} [HasBinaryProduct X Y] :
    prod.lift prod.fst prod.snd = 𝟙 (X ⨯ Y)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd = 𝟙 (X ⨯ Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/
lemma gaussianReal_map_const_add (y : ℝ) :
    (gaussianReal μ v).map (y + ·) = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
exact gaussianReal_map_add_const y

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x => y + x) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
simp_rw [add_comm y]

Result:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_iff_comp_sub_const {a b : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (x - b)) (a + b)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (x - b)) (a + b)

Tactic:
simp [sub_eq_add_neg, differentiableAt_comp_add_const]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem symmetric_symmetrizeRel (V : Set (α × α)) : SymmetricRel (symmetrizeRel V)

Proof state:
α : Type ua
V : Set (α × α)
⊢ SymmetricRel (symmetrizeRel V)

Tactic:
simp [SymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem of_algebraMap_eq [Algebra R A]
    (h : ∀ x, algebraMap R A x = algebraMap S A (algebraMap R S x)) : IsScalarTower R S A :=
  ⟨fun x y z => by simp_rw [Algebra.smul_def, RingHom.map_mul, mul_assoc, h]⟩

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z

Tactic:
simp_rw [Algebra.smul_def, RingHom.map_mul, mul_assoc, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    W.addXYZ P Q = addU P Q • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addXYZ P Q = addU P Q • ![1, 1, 0]

Tactic:
erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx, addZ_of_X_eq hx,
  smul_fin3, mul_one, mul_one, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) :
    dfoldrM.loop n α f (i+1) h x = f ⟨i, by omega⟩ x >>= dfoldrM.loop n α f i (by omega) := rfl

Proof state:
m : Type ?u.714 → Type ?u.693
n : Nat
α : Fin (n + 1) → Type ?u.714
i : Nat
h : i + 1 < n + 1
inst✝ : Monad m
f : (i : Fin n) → α i.succ → m (α i.castSucc)
x : α ⟨i + 1, h⟩
⊢ i < n + 1

Tactic:
omega

Result:
no goals

Proof state:
m : Type ?u.714 → Type ?u.693
n : Nat
α : Fin (n + 1) → Type ?u.714
i : Nat
h : i + 1 < n + 1
inst✝ : Monad m
f : (i : Fin n) → α i.succ → m (α i.castSucc)
x : α ⟨i + 1, h⟩
⊢ i < n

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_div_of_mul_eq' (h : a * c = b) : a = b / c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * c = b
⊢ a = b / c

Tactic:
simp [← h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b

Proof state:
a b : Prop
⊢ a ∨ a ∨ b ↔ a ∨ b

Tactic:
rw [←propext or_assoc, or_self]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem continuousAt_dslope_same : ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a

Tactic:
simp only [dslope, continuousAt_update_same, ← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Reorder an average.

The difference with `Finset.expect_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.expect_bij` is that the bijection is a non-dependent function, rather
than being allowed to use membership of the domain of the average. -/
lemma expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a))
    (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
h : ∀ a ∈ s, f a = g (i a)
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem mul_star_self [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (x * star x)

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (x * star x)

Tactic:
simpa only [star_star] using star_mul_self (star x)

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem left_mem_segment (x y : E) : x ∈ [x -[𝕜] y] :=
  ⟨1, 0, zero_le_one, le_refl 0, add_zero 1, by rw [zero_smul, one_smul, add_zero]⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : MulActionWithZero 𝕜 E
x y : E
⊢ 1 • x + 0 • y = x

Tactic:
rw [zero_smul, one_smul, add_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_int_mul_two_pi_add_pi (n : ℤ) : cos (n * (2 * π) + π) = -1

Proof state:
n : ℤ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum (k : ℕ)
    (f : Finset σ × σ → MvPolynomial σ R) :
    ∑ t ∈ pairs σ k with #t.1 < k, f t =
      ∑ a ∈ antidiagonal k with a.fst < k, ∑ A ∈ powersetCard a.fst univ, ∑ j, f (A, j)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k), f t =
    ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)

Tactic:
rw [filter_pairs_lt, sum_product, sum_disjiUnion]

Result:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y) =
    ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y) =
    ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)

Tactic:
refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_ <;>
  simp +contextual [@eq_comm _ _ k, Nat.add_sub_cancel', le_of_lt]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem nhds_le_nhdsSet_iff [T1Space X] {s : Set X} {x : X} : 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s

Tactic:
rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem indefiniteDiagonal_assoc :
    indefiniteDiagonal (Unit ⊕ l) l R =
      Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm
        (Matrix.fromBlocks 1 0 0 (indefiniteDiagonal l l R))

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))

Tactic:
ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩ <;>
  simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
    Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
    Sum.elim_inl, if_true, eq_self_iff_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
    DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂,
    Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
    Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff, reduceCtorEq] <;>
  congr 1

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a

Tactic:
rw [inter_comm, nhdsWithin_inter_of_mem h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_true_right  : atLeastTwo a b true  = (a || b)

Proof state:
a b : Bool
⊢ a.atLeastTwo b true = (a || b)

Tactic:
cases a <;> cases b <;> simp [atLeastTwo]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Proof state:
b : Bool
x n : ℕ
⊢ bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
cases b <;> simp <;> omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_X_pow [CommRing S] [IsDomain S] [Algebra T S] (n : ℕ) :
    (X ^ n : T[X]).aroots S = n • ({0} : Multiset S)

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
n : ℕ
⊢ (X ^ n).aroots S = n • {0}

Tactic:
rw [aroots_pow, aroots_X]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem prod_properDivisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α}
    (h : p.Prime) : (∏ x ∈ (p ^ k).properDivisors, f x) = ∏ x ∈ range k, f (p ^ x)

Proof state:
α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ range k, f (p ^ x)

Tactic:
simp [h, properDivisors_prime_pow]

Result:
no goals