harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_drop : ∀ {s}, Valid s → ∀ n, (s.drop n).toString.1 = s.toString.1.drop n
  | _, h, _ => let ⟨_, _, _, h⟩ := h.validFor; by simp [(h.drop _).toString, h.toString]

Proof state:
x✝¹ : Substring
h✝ : x✝¹.Valid
x✝ : Nat
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝¹
⊢ (x✝¹.drop x✝).toString.data = List.drop x✝ x✝¹.toString.data

Tactic:
simp [(h.drop _).toString, h.toString]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lt_neg_iff {x y : PGame} : y < -x ↔ x < -y

Proof state:
x y : PGame
⊢ y < -x ↔ x < -y

Tactic:
rw [← neg_neg x, neg_lt_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BEq.lean
theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
⊢ (a != b) = (b != a)

Tactic:
rw [bne, BEq.comm, bne]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_mulSingle_disjoint {b' : B} (hb : b ≠ 1) (hb' : b' ≠ 1) {i j : A} :
    Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
b b' : B
hb : b ≠ 1
hb' : b' ≠ 1
i j : A
⊢ Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j

Tactic:
rw [mulSupport_mulSingle_of_ne hb, mulSupport_mulSingle_of_ne hb', disjoint_singleton]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem mem_pure (x y : α) : x ∈ (pure y : List α) ↔ x = y

Proof state:
α : Type u
x y : α
⊢ x ∈ pure y ↔ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem tendsto_filterAt_iff {ι : Type*} {l : Filter ι} {f : ι → Set X} {x : X} :
    Tendsto f l (v.filterAt x) ↔
      (∀ᶠ i in l, f i ∈ v.setsAt x) ∧ ∀ ε > (0 : ℝ), ∀ᶠ i in l, f i ⊆ closedBall x ε

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set X
x : X
⊢ Tendsto f l (v.filterAt x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε

Tactic:
simp only [filterAt, tendsto_inf, nhds_basis_closedBall.smallSets.tendsto_right_iff,
  tendsto_principal, and_comm, mem_powerset_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_map {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
    (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
  ext fun t ht => by simp [*, hf ht]

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ((map f μ).restrict s) t = (map f (μ.restrict (f ⁻¹' s))) t

Tactic:
simp [*, hf ht]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem eq_orthogonalProjection_of_mem_orthogonal' {u v z : E}
    (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) : (orthogonalProjection K u : E) = v :=
  eq_orthogonalProjection_of_mem_orthogonal hv (by simpa [hu] )

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u v z : E
hv : v ∈ K
hz : z ∈ Kᗮ
hu : u = v + z
⊢ u - v ∈ Kᗮ

Tactic:
simpa [hu]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_eq_ite_iff {a : Bool} {p : Prop} [h : Decidable p] {x y u v : α} :
  (cond a x y = ite p u v) ↔ ite a x y = ite p u v

Proof state:
α : Type u_1
a : Bool
p : Prop
h : Decidable p
x y u v : α
⊢ ((bif a then x else y) = if p then u else v) ↔ (if a = true then x else y) = if p then u else v

Tactic:
simp [Bool.cond_eq_ite]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem range_sigma_eq_iUnion_range {γ : α → Type*} (f : Sigma γ → β) :
    range f = ⋃ a, range fun b => f ⟨a, b⟩ :=
  Set.ext <| by simp

Proof state:
α : Type u_1
β : Type u_2
γ : α → Type u_12
f : Sigma γ → β
⊢ ∀ (x : β), x ∈ range f ↔ x ∈ ⋃ a, range fun b => f ⟨a, b⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
  getElem_attachWith h

Proof state:
α : Type ?u.41235
xs : List α
i : Nat
h : i < xs.attach.length
⊢ i < xs.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Tor.lean
/-- The higher `Tor'` groups for `X` and `Y` are zero if `X` is projective. -/
lemma isZero_Tor'_succ_of_projective (X Y : C) [Projective X] (n : ℕ) :
    IsZero (((Tor' C (n + 1)).obj X).obj Y)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
inst✝³ : Abelian C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((Tor' C (n + 1)).obj X).obj Y)

Tactic:
apply Functor.isZero_leftDerived_obj_projective_succ

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
lemma toNat_ne_zero : toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀

Proof state:
c : Cardinal.{u}
⊢ toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀

Tactic:
simp [not_or]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem nodup_aroots_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0)
    (h : f.Splits (algebraMap F K)) : (f.aroots K).Nodup ↔ f.Separable

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (algebraMap F K) f
⊢ (f.aroots K).Nodup ↔ f.Separable

Tactic:
rw [← (algebraMap F K).id_comp, ← splits_map_iff] at h

Result:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id K) (map (algebraMap F K) f)
⊢ (f.aroots K).Nodup ↔ f.Separable

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id K) (map (algebraMap F K) f)
⊢ (f.aroots K).Nodup ↔ f.Separable

Tactic:
rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_eq_sInf_isMaximal : jacobson R = sInf {I : Ideal R | I.IsMaximal}

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ jacobson R = sInf {I | I.IsMaximal}

Tactic:
simp_rw [jacobson, Module.jacobson, Ideal.isMaximal_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
lemma fderiv_eq_deriv_mul {f : 𝕜 → 𝕜} {x y : 𝕜} : (fderiv 𝕜 f x : 𝕜 → 𝕜) y = (deriv f x) * y

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = deriv f x * y

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem edist_equiv_symm_fst (x₁ x₂ : α) :
    edist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) =
      edist x₁ x₂

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ edist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = edist x₁ x₂

Tactic:
simp only [edist_nndist, nndist_equiv_symm_fst p α β x₁ x₂]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem intCast_le_cast {m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
rw [← cast_le (K := K), cast_intCast]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitePos_iff_infinitesimal_inv_pos {x : ℝ*} :
    InfinitePos x ↔ Infinitesimal x⁻¹ ∧ 0 < x⁻¹ :=
  ⟨fun hip =>
    ⟨infinitesimal_def.mpr fun r hr =>
        ⟨lt_trans (coe_lt_coe.2 (neg_neg_of_pos hr)) (inv_pos.2 (hip 0)),
          inv_lt_of_inv_lt₀ (coe_lt_coe.2 hr) (by convert hip r⁻¹)⟩,
      inv_pos.2 <| hip 0⟩,
    fun ⟨hi, hp⟩ r =>
    @_root_.by_cases (r = 0) (↑r < x) (fun h => Eq.substr h (inv_pos.mp hp)) fun h =>
      lt_of_le_of_lt (coe_le_coe.2 (le_abs_self r))
        ((inv_lt_inv₀ (inv_pos.mp hp) (coe_lt_coe.2 (abs_pos.2 h))).mp
          ((infinitesimal_def.mp hi) |r|⁻¹ (inv_pos.2 (abs_pos.2 h))).2)⟩

Proof state:
x : ℝ*
hip : x.InfinitePos
r : ℝ
hr : 0 < r
⊢ (↑r)⁻¹ < x

Tactic:
convert hip r⁻¹

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_eq_codom_of_domain_subset {s : Set α} (h : r.dom ⊆ s) : r.image s = r.codom

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
h : r.dom ⊆ s
⊢ r.inv.codom ⊆ s

Tactic:
rwa [← codom_inv] at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
h : r.dom ⊆ s
⊢ r.image s = r.codom

Tactic:
apply r.inv.image_eq_dom_of_codomain_subset (by rwa [← codom_inv] at h)

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
theorem whiskerLeft_naturality_id (f : a' ⟶ G.obj a) :
    f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.mapId a =
      f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : OplaxNatTrans G H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.mapId a =
    f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality_id]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem coe_cycleRange_of_lt {n : ℕ} {i j : Fin n} (h : j < i) :
    (cycleRange i j : ℕ) = j + 1

Proof state:
n : ℕ
i j : Fin n
h : j < i
⊢ ↑(i.cycleRange j) = ↑j + 1

Tactic:
rw [coe_cycleRange_of_le h.le, if_neg h.ne]

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
lemma one_sub (h : IsIdempotentElem a) : IsIdempotentElem (1 - a)

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ IsIdempotentElem (1 - a)

Tactic:
rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]

Result:
no goals
-- Mathlib/RingTheory/Nakayama.lean
theorem eq_bot_of_le_smul_of_le_jacobson_bot (I : Ideal R) (N : Submodule R M) (hN : N.FG)
    (hIN : N ≤ I • N) (hIjac : I ≤ jacobson ⊥) : N = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ ⊥.jacobson
⊢ N = ⊥

Tactic:
rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccLimitRecOn_of_isMin (hb : IsMin b) : isSuccLimitRecOn b hm hs hl = hm b hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsMin b
⊢ isSuccLimitRecOn b hm hs hl = hm b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

Result:
no goals
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem ncoeff_smul (A : VertexOperator R V) (r : R) (n : ℤ) : (r • A) [[n]] = r • A [[n]]

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
r : R
n : ℤ
⊢ (r • A)[[n]] = r • A[[n]]

Tactic:
rw [ncoeff, ncoeff, coeff_smul, Pi.smul_apply]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosed_set_pi {i : Set ι} {s : ∀ a, Set (π a)} (hs : ∀ a ∈ i, IsClosed (s a)) :
    IsClosed (pi i s)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ a ∈ i, IsClosed (s a)
⊢ IsClosed (⋂ a ∈ i, eval a ⁻¹' s a)

Tactic:
exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ a ∈ i, IsClosed (s a)
⊢ IsClosed (i.pi s)

Tactic:
rw [pi_def]

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ a ∈ i, IsClosed (s a)
⊢ IsClosed (⋂ a ∈ i, eval a ⁻¹' s a)
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairingIn_one_four_iff [NoZeroDivisors R] :
    P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.root j = (2 : R) • P.root i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : NoZeroSMulDivisors R N
inst✝ : NoZeroDivisors R
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.root j = 2 • P.root i

Tactic:
rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
  ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
  (algebraMap_injective S R).eq_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Prod.lean
lemma prod_fac :
    (W₁.Q.prod W₂.Q) ⋙ prodLift F hF = F

Proof state:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₁.Q.prod W₂.Q ⋙ prodLift F hF = F

Tactic:
rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
  Functor.uncurry_obj_curry_obj]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma divisorsAntidiag_ofNat (n : ℕ) :
    divisorsAntidiag ofNat(n) =
      (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by
          simp +contextual [disjoint_left, eq_comm]) := rfl

Proof state:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ Disjoint (map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal)
    (map (negNatCast.prodMap negNatCast) n.divisorsAntidiagonal)

Tactic:
simp +contextual [disjoint_left, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_projIcc (x : ℝ) :
    arcsin (projIcc (-1) 1 (neg_le_self zero_le_one) x) = arcsin x

Proof state:
x : ℝ
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = arcsin x

Tactic:
rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
      Function.comp_apply]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosure_univ : supClosure (Set.univ : Set α) = Set.univ

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure Set.univ = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addU_of_Z_eq_zero_left {P Q : Fin 3 → F} (hPz : P z = 0) : addU P Q = 0

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ addU P Q = 0

Tactic:
rw [addU, hPz, zero_mul, div_zero]

Result:
no goals
-- Mathlib/Data/Complex/BigOperators.lean
@[simp]
lemma re_expect (f : α → ℂ) : (𝔼 i ∈ s, f i).re = 𝔼 i ∈ s, (f i).re :=
  map_expect (LinearMap.mk reAddGroupHom.toAddHom (by simp)) f s

Proof state:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑reAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑reAddGroupHom).toFun x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_nsmul [NormedSpace ℝ F] (n : ℕ) (f : α → F) :
    eLpNorm (n • f) p μ = n * eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : α → F
⊢ eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using eLpNorm_const_smul (n : ℝ) f ..

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem pullbackObjIso_inv_comp_fst (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).inv ≫ (pullback.fst f g).app d = pullback.fst (f.app d) (g.app d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).inv ≫ (pullback.fst f g).app d = pullback.fst (f.app d) (g.app d)

Tactic:
simp [pullbackObjIso]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_lift'_closure_iff {F : Filter X} :
    ClusterPt x (F.lift' closure) ↔ ClusterPt x F

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ ClusterPt x (F.lift' closure) ↔ ClusterPt x F

Tactic:
simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_id (l : Vector α n) : map (id : α → α) l = l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ map id l = l

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean
@[simp, reassoc]
lemma stupidTruncMap_comp :
    stupidTruncMap (φ ≫ φ') e = stupidTruncMap φ e ≫ stupidTruncMap φ' e

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ stupidTruncMap (φ ≫ φ') e = stupidTruncMap φ e ≫ stupidTruncMap φ' e

Tactic:
simp [stupidTruncMap, stupidTrunc]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_self' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) :
    X.σ i ≫ X.δ j = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
rw [δ_comp_σ_self]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictAnti_of_lt_pred (hf : ∀ a, ¬ IsMin a → f a < f (pred a)) : StrictAnti f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ StrictAnti f

Tactic:
simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a < f (pred a)

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem CompleteLattice.isStronglyCoatomic [IsLowerModularLattice α] [IsCoatomistic α] :
    IsStronglyCoatomic α

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
exact CompleteLattice.isStronglyAtomic

Result:
no goals

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Result:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic'_source {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    (stereographic' n v).source = {v}ᶜ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (stereographic' n v).source = {v}ᶜ

Tactic:
simp [stereographic']

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_option {v : Option ι → V} : LinearIndependent K v ↔
    LinearIndependent K (v ∘ (↑) : ι → V) ∧
      v none ∉ Submodule.span K (range (v ∘ (↑) : ι → V))

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : Option ι → V
⊢ LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ span K (range (v ∘ some))

Tactic:
simp only [← linearIndependent_option', Option.casesOn'_none_coe]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_iff_comp_neg {a : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (-x)) (-a)

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

Tactic:
simp_rw [← differentiableAt_comp_neg, neg_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_restrict₀ (hs : NullMeasurableSet s (μ.restrict t)) :
    (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
  ext fun u hu => by
    simp only [Set.inter_assoc, restrict_apply hu,
      restrict_apply₀ (hu.nullMeasurableSet.inter hs)]

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict (s ∩ t)) u

Tactic:
simp only [Set.inter_assoc, restrict_apply hu,
  restrict_apply₀ (hu.nullMeasurableSet.inter hs)]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_symm_naturality {X X' Y Y' Z : C} [ExactPairing Y Y'] (f : X ⟶ X')
    (g : X' ⟶ Y ⊗ Z) :
    (tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) =
      _ ◁ f ≫ (tensorLeftHomEquiv X' Y Y' Z).symm g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Y ⊗ Z
⊢ (tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) = Y' ◁ f ≫ (tensorLeftHomEquiv X' Y Y' Z).symm g

Tactic:
simp [tensorLeftHomEquiv]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂)
    (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R M) : map (g.comp f : M →ₛₗ[σ₁₃] M₃) p = map g (map f p) :=
  SetLike.coe_injective <| by simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]

Proof state:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomSurjective σ₁₂
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomSurjective σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R M
⊢ ↑(map (g.comp f) p) = ↑(map g (map f p))

Tactic:
simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_mem_spectrum_of_nonneg [Nontrivial A] {a : A} (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ∈ spectrum ℝ a

Tactic:
simpa using spectrum.algebraMap_mem ℝ <| nnnorm_mem_spectrum_of_nonneg ha

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
protected lemma mul_eq_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b = b ↔ a = 1

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ a * b = b ↔ a = 1

Tactic:
simpa using ENNReal.mul_left_inj hb₀ hb (b := 1)

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem coeff_derivativeFun (f : R⟦X⟧) (n : ℕ) :
    coeff R n f.derivativeFun = coeff R (n + 1) f * (n + 1)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (coeff R n) f.derivativeFun = (coeff R (n + 1)) f * (↑n + 1)

Tactic:
rw [derivativeFun, coeff_mk]

Result:
no goals