harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem hasSum_mFourier_series_apply_of_summable (h : Summable (mFourierCoeff f))
    (x : UnitAddTorus d) : HasSum (fun i ↦ mFourierCoeff f i • mFourier i x) (f x)

Proof state:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
x : UnitAddTorus d
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • (mFourier i) x) (f x)

Tactic:
simpa only [_root_.map_smul] using (ContinuousMap.evalCLM ℂ x).hasSum
  (hasSum_mFourier_series_of_summable h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} (h : m.1.WF)
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
k : α
fallback : β k
h : m.val.WF
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

Tactic:
simp only [getD_alter, h, beq_self_eq_true, reduceDIte, cast_eq_id, Option.map_id_fun, id_eq]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.toENat_le_natCast_iff {c : Cardinal} {n : ℕ} :
    toENat c ≤ n ↔ c ≤ n

Proof state:
c : Cardinal.{u_3}
n : ℕ
⊢ toENat c ≤ ↑n ↔ c ≤ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem head_think (s : WSeq α) : head (think s) = (head s).think

Proof state:
α : Type u
s : WSeq α
⊢ s.think.head = s.head.think

Tactic:
simp [head]

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_zero : birthday 0 = 0

Proof state:
⊢ birthday 0 = 0

Tactic:
simp [inferInstanceAs (IsEmpty PEmpty)]

Result:
no goals
-- Mathlib/Topology/MetricSpace/DilationEquiv.lean
@[simp]
lemma _root_.IsometryEquiv.toDilationEquiv_ratio (e : X ≃ᵢ Y) : ratio e.toDilationEquiv = 1

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio e.toDilationEquiv = 1

Tactic:
rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_pos_iff {a : α} {l : Array α} : 0 < count a l ↔ a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ 0 < count a l ↔ a ∈ l

Tactic:
simp only [count, countP_pos_iff, beq_iff_eq, exists_eq_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_zero : W.φ 0 = 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 0 = 1

Tactic:
rw [φ, ψ_zero, zero_pow two_ne_zero, mul_zero, zero_sub, zero_add, ψ_one, one_mul, zero_sub,
  ψ_neg, neg_neg, ψ_one]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem eq_true_of_not_eq_false' {a : Bool} : !a = false → a = true

Proof state:
a : Bool
⊢ (!decide (a = false)) = true → a = true

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_zero_left : hammingDist (0 : ∀ i, β i) = hammingNorm :=
  funext fun x => by rw [hammingDist_comm, hammingDist_zero_right]

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x

Tactic:
rw [hammingDist_comm, hammingDist_zero_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem sumCoords_self_apply : b.sumCoords (b i) = 1

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ b.sumCoords (b i) = 1

Tactic:
simp only [Basis.sumCoords, LinearMap.id_coe, LinearEquiv.coe_coe, id, Basis.repr_self,
  Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp, Finsupp.sum_single_index]

Result:
no goals
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_zero : cauchyBound (0 : K[X]) = 1

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
⊢ cauchyBound 0 = 1

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem equivRealProd_apply_le' (z : ℂ) : ‖equivRealProd z‖ ≤ 1 * ‖z‖

Proof state:
z : ℂ
⊢ ‖equivRealProd z‖ ≤ 1 * ‖z‖

Tactic:
simpa using equivRealProd_apply_le z

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
lemma cartanMatrix_le_zero_of_ne [Finite ι] [NoZeroDivisors R]
    [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N]
    (i j : b.support) (h : i ≠ j) :
    b.cartanMatrix i j ≤ 0 :=
  b.pairingIn_le_zero_of_ne (by rwa [ne_eq, ← Subtype.ext_iff]) i.property j.property

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
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
i j : ↑b.support
h : i ≠ j
⊢ ↑i ≠ ↑j

Tactic:
rwa [ne_eq, ← Subtype.ext_iff]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem map_inv_lt_map_inv_iff (f : F) {a b : β} :
    EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsLimit.iSup_Iio {o : Ordinal} (h : IsLimit o) : ⨆ a : Iio o, a.1 = o

Proof state:
o : Ordinal.{u_4}
h : o.IsLimit
⊢ ⨆ a, ↑a = o

Tactic:
rw [← sSup_eq_iSup', h.sSup_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getThenInsertIfNew?_fst [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
    (m.getThenInsertIfNew? k v).1 = m.get? k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
v : β k
⊢ (m.getThenInsertIfNew? k v).fst = m.get? k

Tactic:
simp_to_raw using Raw₀.getThenInsertIfNew?_fst

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/Lemmas.lean
theorem empty_find? [BEq α] [Hashable α] {a : α} :
    (∅ : HashMap α β).find? a = none

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
⊢ ∅.find? a = none

Tactic:
simp [find?, Imp.find?]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.union_indep_iff_forall_not_mem_closure_left (hI : M.Indep I) (hJ : M.Indep J) :
    M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure ((I \ {e}) ∪ J)

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
simp_rw [union_comm I J, hJ.union_indep_iff_forall_not_mem_closure_right hI, union_comm]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem swap_apply_apply (f : Perm α) (x y : α) : swap (f x) (f y) = f * swap x y * f⁻¹

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = f * swap x y * f⁻¹

Tactic:
rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_insertManyIfNewUnit_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit m l) k fallback = ()

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
l : List α
k : α
fallback : Unit
⊢ getD (insertManyIfNewUnit m l) k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem dist_center_eq_dist_center_of_mem_sphere' {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) : dist s.center p₁ = dist s.center p₂

Proof state:
P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist s.center p₁ = dist s.center p₂

Tactic:
rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem upperSemicontinuousWithinAt_univ_iff :
    UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f : α → β
x : α
⊢ UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x

Tactic:
simp [UpperSemicontinuousWithinAt, UpperSemicontinuousAt, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive even_iff_exists_two_nsmul]
lemma isSquare_iff_exists_sq (a : α) : IsSquare a ↔ ∃ r, a = r ^ 2

Proof state:
α : Type u_2
inst✝ : Monoid α
a : α
⊢ IsSquare a ↔ ∃ r, a = r ^ 2

Tactic:
simp [IsSquare, pow_two]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem cardinalMk_eq_cardinalMk_field_pow_rank (K V : Type u) [Ring K] [StrongRankCondition K]
    [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
    #V = #K ^ Module.rank K V

Proof state:
K V : Type u
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V = #K ^ Module.rank K V

Tactic:
simpa using lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem coequalizer.π_colimMap_desc {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g']
    (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') (h : Y' ⟶ Z)
    (wh : f' ≫ h = g' ≫ h) :
    coequalizer.π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ coequalizer.desc h wh =
      q ≫ h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ desc h wh = q ≫ h

Tactic:
rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_neg_left (w : ι → ℝ) (f g : ∀ i, E i) : ⟪-f, g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ wInner w (-f) g = -wInner w f g

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem sigma_sum [AddCommMonoid N] (f : (Σi : ι, αs i) → M → N) :
    l.sum f = ∑ i ∈ splitSupport l, (split l i).sum fun (a : αs i) b => f ⟨i, a⟩ b

Proof state:
ι : Type u_4
M : Type u_5
N : Type u_7
αs : ι → Type u_13
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : AddCommMonoid N
f : (i : ι) × αs i → M → N
⊢ l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b => f ⟨i, a⟩ b

Tactic:
simp only [sum, sigma_support, sum_sigma, split_apply]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem one_mul (a : Rat) : 1 * a = a

Proof state:
a : Rat
⊢ 1 * a = a

Tactic:
simp [mul_def, normalize_self]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma ofComplex_apply_of_im_pos {z : ℂ} (hz : 0 < z.im) :
    ofComplex z = ⟨z, hz⟩

Proof state:
z : ℂ
hz : 0 < z.im
⊢ ↑ofComplex z = ⟨z, hz⟩

Tactic:
simpa only [coe_mk_subtype] using ofComplex_apply ⟨z, hz⟩

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Map.lean
theorem tendsto_atTop_iff {l : Filter γ} {f : γ → α} (e : α ≃o β) :
    Tendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Defs.lean
theorem Algebra.transcendental_iff_not_isAlgebraic :
    Algebra.Transcendental R A ↔ ¬ Algebra.IsAlgebraic R A

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

Tactic:
simp [isAlgebraic_def, transcendental_def, Transcendental]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    m.isEmpty = true → getD m a fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ m.isEmpty = true → getD m a fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_interval_add_interval_comm (hab : IntervalIntegrable f μ a b)
    (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
    ((∫ x in a..b, f x ∂μ) + ∫ x in c..d, f x ∂μ) =
      (∫ x in a..d, f x ∂μ) + ∫ x in c..b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ

Tactic:
rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
  integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
@[simp]
lemma Polarization_apply (x : M) :
    P.Polarization x = ∑ i, P.coroot' i x • P.coroot 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
inst✝ : Fintype ι
x : M
⊢ P.Polarization x = ∑ i : ι, (P.coroot' i) x • P.coroot i

Tactic:
simp [Polarization]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq {t₁ t₂ : Triangle ℝ P}
    {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃)
    (h₁ : t₁.points i₁ = t₂.points i₁) (h₃ : t₁.points i₃ = t₂.points i₃)
    (h₂ : (2 : ℤ) • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) =
      (2 : ℤ) • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)) :
    t₁.circumsphere = t₂.circumsphere

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂

Tactic:
rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
  t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
  Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_smul' [Monoid S] [DistribMulAction S R] (s : S) (a : ℍ[R,c₁,0,c₃]) :
    star (s • a) = s • star a :=
  QuaternionAlgebra.ext (by simp) (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm

Proof state:
S : Type u_1
R : Type u_3
c₁ c₃ : R
inst✝² : CommRing R
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
s : S
a : ℍ[R,c₁,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_int_lt_one_iff_dvd (k : ℤ) : ‖(k : ℤ_[p])‖ < 1 ↔ (p : ℤ) ∣ k :=
  suffices ‖(k : ℚ_[p])‖ < 1 ↔ ↑p ∣ k by rwa [norm_intCast_eq_padic_norm]
  padicNormE.norm_int_lt_one_iff_dvd k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
this : ‖↑k‖ < 1 ↔ ↑p ∣ k
⊢ ‖↑k‖ < 1 ↔ ↑p ∣ k

Tactic:
rwa [norm_intCast_eq_padic_norm]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem exists_nhds_square {s : Set (X × X)} {x : X} (hx : s ∈ 𝓝 (x, x)) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (X × X)
x : X
hx : s ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Tactic:
simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_modify (h : m.1.WF) {k : α} {f : β k → β k} :
    (m.modify k f).1.size = m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
⊢ (m.modify k f).val.size = m.val.size

Tactic:
simp_to_model [modify] using List.length_modifyKey

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem Set.Subsingleton.minimal_mem_iff (h : s.Subsingleton) : Minimal (· ∈ s) x ↔ x ∈ s

Proof state:
α : Type u_1
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Minimal (fun x => x ∈ s) x ↔ x ∈ s

Tactic:
obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_perm_eq_two_power : #(Equiv.Perm α) = 2 ^ #α

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #(Perm α) = 2 ^ #α

Tactic:
rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.total : biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ fst ≫ inl + snd ≫ inr = 𝟙 (X ⊞ Y)

Tactic:
ext <;> simp [add_comp]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
@[simp] lemma eq_update_self_iff : f = update f a b ↔ f a = b

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ f = update f a b ↔ f a = b

Tactic:
simp [eq_update_iff]

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_op_distrib {f g : α → β} {b₁ b₂ : β} :
    (s.fold op (b₁ * b₂) fun x => f x * g x) = s.fold op b₁ f * s.fold op b₂ g

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
s : Finset α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)

Tactic:
simp only [fold, fold_distrib]

Result:
no goals
-- Mathlib/Analysis/Convex/Visible.lean
@[simp, refl] lemma IsVisible.rfl : IsVisible 𝕜 s x x

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x : P
⊢ IsVisible 𝕜 s x x

Tactic:
simp [IsVisible]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c

Proof state:
a b c : Nat
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
rw [Nat.add_comm, Nat.sub_le_iff_le_add]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem card_powerset (s : Multiset α) : card (powerset s) = 2 ^ card s :=
  Quotient.inductionOn s <| by simp

Proof state:
α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), (powerset ⟦a⟧).card = 2 ^ card ⟦a⟧

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem convs_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) :
    g.convs m = g.convs n

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.convs m = g.convs n

Tactic:
simp only [convs, dens_stable_of_terminated n_le_m terminatedAt_n,
  nums_stable_of_terminated n_le_m terminatedAt_n]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_apply_eq_condDistrib [Nonempty Ω] {ω : Ω} :
    condExpKernel μ m ω = @condDistrib Ω Ω Ω mΩ _ _ mΩ (m ⊓ mΩ) id id μ _ (id ω)

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : Nonempty Ω
ω : Ω
⊢ (condExpKernel μ m) ω = (condDistrib id id μ) (id ω)

Tactic:
simp [condExpKernel_eq, Kernel.comap_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
    (i.cast h).succ = i.succ.cast (by rw [h]) := rfl

Proof state:
n n' : Nat
i : Fin n
h : n = n'
⊢ n + 1 = n' + 1

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_sigma {α} {E : α → Type*} : IsEmpty (Sigma E) ↔ ∀ a, IsEmpty (E a)

Proof state:
α : Type u_5
E : α → Type u_4
⊢ IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_sigma, not_exists]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_top : Icc a ⊤ = Ici a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.Finset.aestronglyMeasurable_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) :
    AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.prod_apply] using s.aestronglyMeasurable_prod' hf

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_comp [NormedSpace ℝ E]
    ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
    AEStronglyMeasurable (fun x ↦ ∫ y, f y ∂η x) (κ a) :=
  ⟨fun x ↦ ∫ y, hf.mk f y ∂η x, hf.stronglyMeasurable_mk.integral_kernel, by
    filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (fun x => ∫ (y : γ), f y ∂η x) =ᶠ[ae (κ a)] fun x => ∫ (y : γ), AEStronglyMeasurable.mk f hf y ∂η x

Tactic:
filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_mul : ∀ a b, (a * b : ℝ).cauchy = a.cauchy * b.cauchy
  | ⟨a⟩, ⟨b⟩ => show (mul _ _).cauchy = _ by rw [mul_def]

Proof state:
a b : Cauchy abs
⊢ (Real.mul { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy * { cauchy := b }.cauchy

Tactic:
rw [mul_def]

Result:
no goals
-- Mathlib/Data/Sym/Card.lean
theorem card_image_offDiag (s : Finset α) : #(s.offDiag.image Sym2.mk) = (#s).choose 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image Sym2.mk s.offDiag) = (#s).choose 2

Tactic:
rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
  Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]

Result:
no goals