harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_le_aleph0_iff : #α ≤ ℵ₀ ↔ Countable α

Proof state:
α : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α

Tactic:
rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn_map [Monad m] [LawfulMonad m]
    (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
    forIn (o.map g) init f = forIn o init fun a y => f (g a) y

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
g : α → β
f : β → γ → m (ForInStep γ)
⊢ forIn (Option.map g o) init f = forIn o init fun a y => f (g a) y

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
b : β
⊢ b ∈ pmap f l H ↔ ∃ a h, f a ⋯ = b

Tactic:
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem app_right_eq_ι_comp_fst (b) :
    K.π.app (WalkingMulticospan.right b) = K.ι (J.fst b) ≫ I.fst b

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.fst b) ≫ I.fst b

Tactic:
rw [← K.w (WalkingMulticospan.Hom.fst b)]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem coe_singleton (a : α) : (({a} : Finset α) : Set α) = {a}

Proof state:
case h
α : Type u_1
a x✝ : α
⊢ x✝ ∈ ↑{a} ↔ x✝ ∈ {a}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
⊢ ↑{a} = {a}

Tactic:
ext

Result:
case h
α : Type u_1
a x✝ : α
⊢ x✝ ∈ ↑{a} ↔ x✝ ∈ {a}
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma balance_sub (f g : ι → G) : balance (f - g) = balance f - balance g

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f g : ι → G
⊢ balance (f - g) = balance f - balance g

Tactic:
simp only [balance, expect_sub_distrib, const_sub, sub_sub_sub_comm, Pi.sub_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma nil_reverse {p : G.Walk v w} : p.reverse.Nil ↔ p.Nil

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.reverse.Nil ↔ p.Nil

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem neg_div_self {a : K} (h : a ≠ 0) : -a / a = -1

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -a / a = -1

Tactic:
rw [neg_div, div_self h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]?

Proof state:
Cont : Type u_1
Elem : Type u_2
Dom : Cont → Nat → Prop
n : Nat
h : GetElem? Cont Nat Elem Dom
a : Cont
i : Fin n
⊢ getElem? a i = getElem? a ↑i

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_singleton' {μ : Measure α} {f : α → E} (hf : StronglyMeasurable f) (a : α) :
    ∫ a in {a}, f a ∂μ = (μ {a}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : StronglyMeasurable f
a : α
⊢ ∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a

Tactic:
simp only [Measure.restrict_singleton, integral_smul_measure, integral_dirac' f a hf]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- A multiplicative norm composed with the absolute value on integers equals the norm itself. -/
@[deprecated "Use AbsoluteValue.apply_natAbs_eq instead" (since := "2025-01-07")]
lemma MulRingNorm.apply_natAbs_eq {R : Type*} [Ring R] (x : ℤ) (f : MulRingNorm R) : f (natAbs x) =
    f x

Proof state:
R : Type u_2
inst✝ : Ring R
x : ℤ
f : MulRingNorm R
⊢ f ↑x.natAbs = f ↑x

Tactic:
obtain ⟨n, rfl | rfl⟩ := eq_nat_or_neg x <;>
simp only [natAbs_neg, natAbs_ofNat, cast_neg, cast_natCast, map_neg_eq_map]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem inv_right [IsIso sq] : (inv sq).right = inv sq.right :=
  IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Proof state:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.right ≫ (inv sq).right = 𝟙 f.right

Tactic:
rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem productMap_range : (productMap f g).range = f.range ⊔ g.range

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (productMap f g).range = f.range ⊔ g.range

Tactic:
rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
  ← AlgHom.range_comp,
  ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
  AlgHom.id_comp, AlgHom.id_comp]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem _root_.Algebra.adjoin_range_eq_range_freeAlgebra_lift (f : X → A) :
    Algebra.adjoin R (Set.range f) = (FreeAlgebra.lift R f).range

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ Algebra.adjoin R (Set.range f) = ((lift R) f).range

Tactic:
simp only [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
  Function.comp_def, lift_ι_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decompId_p_toKaroubi (X : C) : decompId_p ((toKaroubi C).obj X) = 𝟙 _

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ ((toKaroubi C).obj X).decompId_p = 𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' == rhs') = (lhs == rhs)

Proof state:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' == rhs') = (lhs == rhs)

Tactic:
simp[*]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem hasGenEigenvalue_of_hasEigenvalue {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k)
    (hμ : f.HasEigenvalue μ) : f.HasGenEigenvalue μ k :=
  hμ.lt <| by simpa using hk

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
hμ : f.HasEigenvalue μ
⊢ 0 < ↑k

Tactic:
simpa using hk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Pow.lean
theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e)

Proof state:
b : Int
e : Nat
⊢ b ^ (e + 1) = b * b ^ e

Tactic:
rw [Int.mul_comm, Int.pow_succ]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma nhdsSet_eq_comap (hf : IsInducing f) (s : Set X) :
    𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Tactic:
simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma toRatCDF_of_isRatStieltjesPoint {a : α} (h : IsRatStieltjesPoint f a) (q : ℚ) :
    toRatCDF f a q = f a q

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
h : IsRatStieltjesPoint f a
q : ℚ
⊢ toRatCDF f a q = f a q

Tactic:
rw [toRatCDF, if_pos h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
  | m, 0   => by simp
  | _, _+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)

Proof state:
m : Nat
⊢ m / 0 * 0 ≤ m

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.periodic [AddMonoid α] [InvolutiveNeg β]
    (h : Antiperiodic f c) : Periodic f (2 • c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Periodic f (2 • c)

Tactic:
simp [two_nsmul, ← add_assoc, h _]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem map_bind' (f : β → γ) (x : Option α) (g : α → Option β) :
    Option.map f (x.bind g) = x.bind fun a ↦ Option.map f (g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (x.bind g) = x.bind fun a => Option.map f (g a)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isLeast_hnot [CoheytingAlgebra α] (a : α) :
    IsLeast {w | Codisjoint a w} (￢a)

Proof state:
α : Type u
inst✝ : CoheytingAlgebra α
a : α
⊢ IsLeast {w | Codisjoint a w} (￢a)

Tactic:
simpa only [CoheytingAlgebra.top_sdiff, codisjoint_iff_le_sup] using isLeast_sdiff ⊤ a

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem mul_eq {α} [OrderedSemiring α] {a b : α} (ha : a = 0) (_ : 0 < b) : b * a = 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem coeff_inv (n) (φ : k⟦X⟧) :
    coeff k n φ⁻¹ =
      if n = 0 then (constantCoeff k φ)⁻¹
      else
        -(constantCoeff k φ)⁻¹ *
          ∑ x ∈ antidiagonal n,
            if x.2 < n then coeff k x.1 φ * coeff k x.2 φ⁻¹ else 0

Proof state:
k : Type u_2
inst✝ : Field k
n : ℕ
φ : k⟦X⟧
⊢ (coeff k n) φ⁻¹ =
    if n = 0 then ((constantCoeff k) φ)⁻¹
    else -((constantCoeff k) φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff k x.1) φ * (coeff k x.2) φ⁻¹ else 0

Tactic:
rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff k φ)⁻¹ φ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_coeff (i : ℕ) :
    f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Tactic:
simp only [eraseLead, coeff_erase]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma lintegral_eq_const [IsProbabilityMeasure μ] {f : α → ℝ≥0∞} {c : ℝ≥0∞}
    (hf : ∀ᵐ x ∂μ, f x = c) : ∫⁻ x, f x ∂μ = c

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫⁻ (x : α), f x ∂μ = c

Tactic:
simp [lintegral_congr_ae hf]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem MonoidHomClass.antilipschitz_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0}
    (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f :=
  AntilipschitzWith.of_le_mul_dist fun x y => by
    simpa only [dist_eq_norm_div, map_div] using h (x / y)

Proof state:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
x y : E
⊢ dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simpa only [dist_eq_norm_div, map_div] using h (x / y)

Result:
no goals
-- Mathlib/Data/Fintype/Sigma.lean
lemma Set.biUnion_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
    ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2

Proof state:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.prod_right_iff : IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)

Tactic:
simpa only [isCoprime_comm] using IsCoprime.prod_left_iff (R := R)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α} {fallback : β k}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).getD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).getD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.getD_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem not_empty_toList (v : Vector α (n + 1)) : ¬v.toList.isEmpty

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ ¬v.toList.isEmpty = true

Tactic:
simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0

Proof state:
n : Nat
⊢ range n ≠ [] ↔ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem count_nth_succ {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset) :
    count p (nth p n + 1) = n + 1

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ count p (nth p n + 1) = n + 1

Tactic:
rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) {h'} :
    getKey (unitOfList l) k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
h' : k' ∈ unitOfList l
⊢ (unitOfList l).getKey k' h' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_inter_mulSupport (f : α → M) (s : Set α) :
    ∏ᶠ i ∈ s ∩ mulSupport f, f i = ∏ᶠ i ∈ s, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_eq_of_sum_1 (hw : ∑ i ∈ t, w i = 1) :
    t.centerMass w z = ∑ i ∈ t, w i • z i

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
hw : ∑ i ∈ t, w i = 1
⊢ t.centerMass w z = ∑ i ∈ t, w i • z i

Tactic:
simp only [Finset.centerMass, hw, inv_one, one_smul]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
lemma isLocalDiffeomorphOn_iff {f : M → N} (s : Set M) :
    IsLocalDiffeomorphOn I J n f s ↔ ∀ x : s, IsLocalDiffeomorphAt I J n f x

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
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
⊢ IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
@[simp]
lemma count_univ : count (univ : Set α) = ENat.card α

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ count univ = ↑(ENat.card α)

Tactic:
simp [count_apply .univ, encard_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k : α} {h'} (contains : m.contains k):
    getKey (insertManyIfNewUnit m l).1 k h' = getKey m k contains

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
h' : (insertManyIfNewUnit m l).val.contains k = true
contains : m.contains k = true
⊢ (insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_get (xs : List α) (h : Nodup xs) (i : Fin xs.length) :
    formPerm xs (xs.get i) =
      xs.get ⟨((i.val + 1) % xs.length), (Nat.mod_lt _ (i.val.zero_le.trans_lt i.isLt))⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
i : Fin xs.length
⊢ xs.formPerm (xs.get i) = xs.get ⟨(↑i + 1) % xs.length, ⋯⟩

Tactic:
simp [formPerm_apply_getElem, h]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_prime {p : ℕ} (hp : p.Prime) : φ p = p - 1

Proof state:
p : ℕ
hp : Prime p
⊢ φ p = p - 1

Tactic:
rw [← pow_one p, totient_prime_pow hp] <;> simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sub_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x z - o.oangle y z = o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z - o.oangle y z = o.oangle x y

Tactic:
rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isOpen_const {p : Prop} : IsOpen { _x : X | p }

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p : Prop
⊢ IsOpen {_x | p}

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem polar_closure (s : Set E) : polar 𝕜 (closure s) = polar 𝕜 s :=
  ((dualPairing 𝕜 E).flip.polar_antitone subset_closure).antisymm <|
    (dualPairing 𝕜 E).flip.polar_gc.l_le <|
      closure_minimal ((dualPairing 𝕜 E).flip.polar_gc.le_u_l s) <| by
        simpa [LinearMap.flip_flip] using
          (isClosed_polar _ _).preimage (inclusionInDoubleDual 𝕜 E).continuous

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (((dualPairing 𝕜 E).flip.flip.polar ∘ ⇑OrderDual.ofDual) ((dualPairing 𝕜 E).flip.polar s))

Tactic:
simpa [LinearMap.flip_flip] using
  (isClosed_polar _ _).preimage (inclusionInDoubleDual 𝕜 E).continuous

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem HasSum.div_const (h : HasSum f a) (b : α) : HasSum (fun i ↦ f i / b) (a / b)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum f a
b : α
⊢ HasSum (fun i => f i / b) (a / b)

Tactic:
simp only [div_eq_mul_inv, h.mul_right b⁻¹]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem dist_iteratedFDerivWithin_zero (f : E → F) (s : Set E) (x : E)
    (g : E → F) (t : Set E) (y : E) :
    dist (iteratedFDerivWithin 𝕜 0 f s x) (iteratedFDerivWithin 𝕜 0 g t y) = dist (f x) (g y)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
g : E → F
t : Set E
y : E
⊢ dist (iteratedFDerivWithin 𝕜 0 f s x) (iteratedFDerivWithin 𝕜 0 g t y) = dist (f x) (g y)

Tactic:
simp only [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.dist_map]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
@[reassoc (attr := simp)]
lemma pullback_inv_snd_fst_of_left_isIso :
    inv (pullback.snd f g) ≫ pullback.fst f g = g ≫ inv f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (pullback.snd f g) ≫ pullback.fst f g = g ≫ inv f

Tactic:
rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepSet.measure_inter_eq_mul {μ : Measure Ω} (h : IndepSet s t μ) :
    μ (s ∩ t) = μ s * μ t

Proof state:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
h : IndepSet s t μ
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
simpa using Kernel.IndepSet.measure_inter_eq_mul _ _ h

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem restrict_apply (s t : Set α) (m : OuterMeasure α) : restrict s m t = m (t ∩ s)

Proof state:
α : Type u_1
s t : Set α
m : OuterMeasure α
⊢ ((restrict s) m) t = m (t ∩ s)

Tactic:
simp [restrict, inter_comm t]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_self : H.relindex H = 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relindex H = 1

Tactic:
rw [relindex, subgroupOf_self, index_top]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_span {s : Set M} (hs : s.Finite) : FG (span R s) :=
  ⟨hs.toFinset, by rw [hs.coe_toFinset]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ span R ↑hs.toFinset = span R s

Tactic:
rw [hs.coe_toFinset]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem frontier_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (sphere x r) = sphere x r

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r

Tactic:
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem ker_nhds [T1Space X] (x : X) : (𝓝 x).ker = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
⊢ (𝓝 x).ker = {x}

Tactic:
simp [ker_nhds_eq_specializes]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem smaller_factorization (o : Ordinal) :
    (fun (p : smaller C o) ↦ p.1) ∘ (range_equiv_smaller C o).toFun =
    (πs C o) ∘ (fun (p : range (π C (ord I · < o))) ↦ p.1)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ (fun p => ↑p) ∘ (range_equiv_smaller C o).toFun = ⇑(πs C o) ∘ fun p => ↑p

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem le_separableClosure_iff (L : IntermediateField F E) :
    L ≤ separableClosure F E ↔ Algebra.IsSeparable F L :=
  ⟨fun h ↦ ⟨fun x ↦ by simpa only [IsSeparable, minpoly_eq] using h x.2⟩,
    fun _ ↦ le_separableClosure _ _ _⟩

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ separableClosure F E
x : ↥L
⊢ IsSeparable F x

Tactic:
simpa only [IsSeparable, minpoly_eq] using h x.2

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp] lemma coe_lt_top (a : α) : (a : WithTop α) < ⊤

Proof state:
α : Type u_1
inst✝ : LT α
a : α
⊢ ↑a < ⊤

Tactic:
simp [lt_def]

Result:
no goals