harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDeriv_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι}
    {f : ι → E → A'} {N : WithTop ℕ∞} (hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)) {x : E} {n : ℕ}
    (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (∏ j ∈ u, f j ·) x‖ ≤
      ∑ p ∈ u.sym n, (p : Multiset ι).multinomial *
        ∏ j ∈ u, ‖iteratedFDeriv 𝕜 ((p : Multiset ι).count j) (f j) x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
u : Finset ι
f : ι → E → A'
N : WithTop ℕ∞
hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun x => ∏ j ∈ u, f j x) x‖ ≤
    ∑ p ∈ u.sym n, ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖

Tactic:
simpa [iteratedFDerivWithin_univ] using
  norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ
    (mem_univ x) hn

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_one_sub (a b : α) : a * (1 - b) = a - a * b

Proof state:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b

Tactic:
rw [mul_sub, mul_one]

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_even (n : ℤ) (hn : Even n) : n.negOnePow = 1

Proof state:
case intro
k : ℤ
⊢ (k + k).negOnePow = 1

Tactic:
rw [negOnePow_add, units_mul_self]

Result:
no goals

Proof state:
n : ℤ
hn : Even n
⊢ n.negOnePow = 1

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
k : ℤ
⊢ (k + k).negOnePow = 1
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.equivFinsuppOfBasisRight_symm :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.toLinearMap =
    Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i)

Proof state:
case h.h
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
a✝ : κ
x✝ : M
⊢ (↑(equivFinsuppOfBasisRight 𝒞).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i => (mk R M N).flip (𝒞 i)) ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
simp [equivFinsuppOfBasisRight]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
⊢ ↑(equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun i => (mk R M N).flip (𝒞 i)

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
a✝ : κ
x✝ : M
⊢ (↑(equivFinsuppOfBasisRight 𝒞).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i => (mk R M N).flip (𝒞 i)) ∘ₗ Finsupp.lsingle a✝) x✝
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformity_translate_mul (a : α) : ((𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a)) = 𝓤 α :=
  le_antisymm (uniformContinuous_id.mul uniformContinuous_const)
    (calc
      𝓤 α =
          ((𝓤 α).map fun x : α × α => (x.1 * a⁻¹, x.2 * a⁻¹)).map fun x : α × α =>
            (x.1 * a, x.2 * a)

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ 𝓤 α = map (fun x => (x.1 * a, x.2 * a)) (map (fun x => (x.1 * a⁻¹, x.2 * a⁻¹)) (𝓤 α))

Tactic:
simp [Filter.map_map, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem union_left : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t u : Set X
⊢ SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

Tactic:
simpa only [separatedNhds_iff_disjoint, nhdsSet_union, disjoint_sup_left] using And.intro

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_multiset_sum_le (l : Multiset S[X]) :
    natDegree l.sum ≤ (l.map natDegree).foldr max 0 :=
  Quotient.inductionOn l (by simpa using natDegree_list_sum_le)

Proof state:
S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max 0 (Multiset.map natDegree ⟦a⟧)

Tactic:
simpa using natDegree_list_sum_le

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem coeff_truncateFun (x : 𝕎 R) (i : Fin n) : (truncateFun n x).coeff i = x.coeff i

Proof state:
p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff i (truncateFun n x) = x.coeff ↑i

Tactic:
rw [truncateFun, TruncatedWittVector.coeff_mk]

Result:
no goals
-- Mathlib/Deprecated/Logic.lean
theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : ∀ x : α, β x}
    (h : ∀ x, b₁ x = b₂ x) : (let x : α := a; b₁ x) = (let x : α := a; b₂ x)

Proof state:
α : Sort v
β : α → Sort u
a : α
b₁ b₂ : (x : α) → β x
h : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a;
    b₁ x) =
    let x := a;
    b₂ x

Tactic:
exact h _ ▸ rfl

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
/-- See `List.length_flatten` for the corresponding statement using `List.sum`. -/
@[deprecated length_flatten (since := "2024-10-17")]
lemma length_flatten' (L : List (List α)) : length (flatten L) = Nat.sum (map length L)

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten.length = Nat.sum (map length L)

Tactic:
induction L <;> [rfl; simp only [*, flatten, map, Nat.sum_cons, length_append]]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem top_covers (S : Sieve X) (f : Y ⟶ X) : (⊤ : GrothendieckTopology C).Covers S f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ ⊤.Covers S f

Tactic:
simp [covers_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem map_round (f : F) (hf : StrictMono f) (a : α) : round (f a) = round a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedField α
inst✝⁴ : LinearOrderedField β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ round (f a) = round a

Tactic:
simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
    genEigenspace f (a / b) 1 = LinearMap.ker (b • f - a • 1) :=
  calc
    genEigenspace f (a / b) 1 = genEigenspace f (b⁻¹ * a) 1

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (b⁻¹ * a)) 1 = LinearMap.ker (f - (b⁻¹ * a) • 1)

Tactic:
rw [genEigenspace_one]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (f - b⁻¹ • a • 1) = LinearMap.ker (b • (f - b⁻¹ • a • 1))

Tactic:
rw [LinearMap.ker_smul _ b hb]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (a / b)) 1 = (f.genEigenspace (b⁻¹ * a)) 1

Tactic:
rw [div_eq_mul_inv, mul_comm]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (f - (b⁻¹ * a) • 1) = LinearMap.ker (f - b⁻¹ • a • 1)

Tactic:
rw [smul_smul]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (b • (f - b⁻¹ • a • 1)) = LinearMap.ker (b • f - a • 1)

Tactic:
rw [smul_sub, smul_inv_smul₀ hb]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_preΨ₄ : (W.baseChange B).preΨ₄ = (W.baseChange A).preΨ₄.map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄

Tactic:
rw [← map_preΨ₄, map_baseChange]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem measure_liminf_atTop_eq_zero {s : ℕ → Set α} (h : (∑' i, μ (s i)) ≠ ∞) :
    μ (liminf s atTop) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
h : ∑' (i : ℕ), μ (s i) ≠ ⊤
⊢ μ (liminf s atTop) = 0

Tactic:
rw [← Nat.cofinite_eq_atTop, measure_liminf_cofinite_eq_zero h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n

Proof state:
n : Nat
k : Fin (n + 1)
⊢ ¬k < k + 1 ↔ ¬k < last n

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
k : Fin (n + 1)
⊢ k < k + 1 ↔ k < last n

Tactic:
rw [← Decidable.not_iff_not]

Result:
n : Nat
k : Fin (n + 1)
⊢ ¬k < k + 1 ↔ ¬k < last n
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem mul_dvd_mul_iff_right [CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) :
    a * c ∣ b * c ↔ a ∣ b :=
  exists_congr fun d => by rw [mul_right_comm, mul_left_inj' hc]

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
rw [mul_right_comm, mul_left_inj' hc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma mem_grothendieckTopology_iff_sectionsOfPresieve
    {U : X.AffineZariskiSite} {S : Sieve U} :
    S ∈ grothendieckTopology X U ↔ Ideal.span (sectionsOfPresieve S.1) = ⊤

Proof state:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔ Ideal.span (sectionsOfPresieve S.arrows) = ⊤

Tactic:
rw [← generate_presieveOfSections_mem_grothendieckTopology, presieveOfSections_sectionsOfPresieve,
  Sieve.generate_sieve]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_eq_zero_iff {x : mixedSpace K} :
    mixedEmbedding.norm x = 0 ↔ ∃ w, normAtPlace w x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm x = 0 ↔ ∃ w, (normAtPlace w) x = 0

Tactic:
simp_rw [mixedEmbedding.norm, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, prod_eq_zero_iff,
  mem_univ, true_and, pow_eq_zero_iff mult_ne_zero]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
lemma normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2

Proof state:
z : ℂ
⊢ normSq z = ‖z‖ ^ 2

Tactic:
simp [norm_def, sq, Real.mul_self_sqrt (normSq_nonneg _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_getD_of_contains [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.contains a = true → m.get? a = some (m.getD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ m.contains a = true → m.get? a = some (m.getD a fallback)

Tactic:
simp_to_raw using Raw₀.get?_eq_some_getD

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrange_eq_top {f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_mrange, coe_top]) Set.range_eq_univ

Proof state:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ ↑(mrange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_mrange, coe_top]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_self' (n : ℕ) : (n + 1 : ZMod (n + 1)) = 0

Proof state:
n : ℕ
⊢ ↑n + 1 = 0

Tactic:
rw [← Nat.cast_add_one, natCast_self (n + 1)]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem lift'_smul (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
    (r : R) (m) : r • LocalizedModule.lift' S g h m = LocalizedModule.lift' S g h (r • m) :=
  m.induction_on fun a b => by
    rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.map_smul]

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • lift' S g h (mk a b) = lift' S g h (r • mk a b)

Tactic:
rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
  ← map_smul, ← g.map_smul]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_univ_fin_two (f : Fin 2 → α) :
    (Finset.univ : Finset (Fin 2)).SupIndep f ↔ Disjoint (f 0) (f 1) :=
  have : (0 : Fin 2) ≠ 1

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Fin 2 → α
⊢ 0 ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem range_mem_rightTransversals {f : Quotient (QuotientGroup.rightRel H) → G}
    (hf : ∀ q, Quotient.mk'' (f q) = q) : Set.range f ∈ rightTransversals (H : Set G) :=
  mem_rightTransversals_iff_bijective.mpr
    ⟨by rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
        exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂),
      fun q => ⟨⟨f q, q, rfl⟩, hf q⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Injective ((range f).restrict Quotient.mk'')

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Tactic:
exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter p).isSome) :
    o.isSome

Proof state:
α : Type u_1
p : α → Bool
o : Option α
h : (Option.filter p o).isSome = true
⊢ o.isSome = true

Tactic:
cases o <;> simp at h ⊢

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_castSucc : snoc p x i.castSucc = p i

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ p (i.castSucc.castLT ⋯) = p i

Tactic:
convert cast_eq rfl (p i)

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ snoc p x i.castSucc = p i

Tactic:
simp only [snoc, coe_castSucc, is_lt, cast_eq, dite_true]

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ p (i.castSucc.castLT ⋯) = p i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem mem_keys_iff_contains_keys [BEq α] [LawfulBEq α] {m : Raw α β} {k : α} :
    k ∈ m.keys ↔ (List.keys (toListModel m.buckets)).contains k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
m : Raw α β
k : α
⊢ k ∈ m.keys ↔ (List.keys (toListModel m.buckets)).contains k = true

Tactic:
rw [← List.contains_iff_mem, contains_keys_eq_contains_keys]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem getD_eq_getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : β a) :
    getD m a fallback = getDₘ m a fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
fallback : β a
⊢ m.getD a fallback = m.getDₘ a fallback

Tactic:
simp [getD, getDₘ, get?ₘ, List.getValueCastD_eq_getValueCast?, bucket]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem degrees_neg (p : MvPolynomial σ R) : (-p).degrees = p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).degrees = p.degrees

Tactic:
rw [degrees, support_neg]

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s => toMultiset s) = p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s => toMultiset s) = p.degrees

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_zsmul_eq [AddGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℤ) :
    f (x - n • c) = (n.negOnePow : ℤ) • f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℤ
⊢ f (x - n • c) = ↑n.negOnePow • f x

Tactic:
simpa only [sub_eq_add_neg, neg_zsmul, Int.negOnePow_neg] using h.add_zsmul_eq (-n)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_mul_right {a : Nat} (a0 : a ≠ 0) : mkRat (n * a) (d * a) = mkRat n d

Proof state:
n : Int
d a : Nat
a0 : a ≠ 0
⊢ mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)

Tactic:
congr 1 <;> [apply Int.mul_comm; apply Nat.mul_comm]

Result:
no goals

Proof state:
n : Int
d a : Nat
a0 : a ≠ 0
⊢ mkRat (n * ↑a) (d * a) = mkRat n d

Tactic:
rw [← mkRat_mul_left (d := d) a0]

Result:
n : Int
d a : Nat
a0 : a ≠ 0
⊢ mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_finite_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X}
    (F_comp : IsCompact F) (F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) :
    coverMincard T F U n < ⊤

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ coverMincard T F U n < ⊤

Tactic:
rcases exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv U_uni n with ⟨s, s_cover⟩

Result:
case intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤

Proof state:
case intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem iterate_eq_of_map_eq_add_int {x : ℝ} {m : ℤ} (h : f x = x + m) (n : ℕ) :
    f^[n] x = x + n * m

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x = x + ↑m
n : ℕ
⊢ (⇑f)^[n] x = x + ↑n * ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_fuzzy_neg_iff {x : PGame} : 0 ‖ -x ↔ 0 ‖ x

Proof state:
x : PGame
⊢ 0 ‖ -x ↔ 0 ‖ x

Tactic:
rw [← neg_fuzzy_iff, neg_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma neg_natCast_eq_one (n : ℕ) : -(n : Fin (n + 1)) = 1

Proof state:
n : ℕ
⊢ -↑n = 1

Tactic:
simp only [natCast_eq_last, neg_last]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_erase_self [LawfulBEq α] (h : m.WF) {k : α} {fallback : β k} :
    (m.erase k).getD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
fallback : β k
⊢ (m.erase k).getD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.getD_erase_self

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem hensels_lemma :
    ∃ z : ℤ_[p],
      F.eval z = 0 ∧
        ‖z - a‖ < ‖F.derivative.eval a‖ ∧
          ‖F.derivative.eval z‖ = ‖F.derivative.eval a‖ ∧
            ∀ z', F.eval z' = 0 → ‖z' - a‖ < ‖F.derivative.eval a‖ → z' = z

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
ha : ¬Polynomial.eval a F = 0
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z

Tactic:
exact ⟨soln_gen hnorm, eval_soln hnorm,
  soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z

Tactic:
exact if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩
else by
  exact ⟨soln_gen hnorm, eval_soln hnorm,
    soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z

Tactic:
classical
exact if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩
else by
  exact ⟨soln_gen hnorm, eval_soln hnorm,
    soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    k ∈ m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ k ∈ m.insertIfNew k v

Tactic:
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_two_mul (n : ℕ) :
    bitIndices (2 * n) = (bitIndices n).map (· + 1)

Proof state:
n : ℕ
⊢ (2 * n).bitIndices = map (fun x => x + 1) n.bitIndices

Tactic:
rw [← bitIndices_bit_false, bit_false]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph'_pos {o : Ordinal} (ho : 0 < o) : 0 < aleph' o

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
⊢ 0 < aleph' o

Tactic:
rwa [← aleph'_zero, aleph'_lt]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) :
    ⨆ n : ℕ, f n = f ω

Proof state:
f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = f ω

Tactic:
rw [← iSup_natCast, hf.map_iSup]

Result:
no goals