harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Derivation.lean
theorem mkDerivationₗ_X (f : σ → A) (i : σ) : mkDerivationₗ R f (X i) = f i :=
  (mkDerivationₗ_monomial f _ _).trans <| by simp [tsub_self]

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
f : σ → A
i : σ
⊢ (1 • (Finsupp.single i 1).sum fun i_1 k => (monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) = f i

Tactic:
simp [tsub_self]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Ici : (fun x => a + x) '' Ici b = Ici (a + b)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b : M
⊢ (fun x => a + x) '' Ici b = Ici (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ici]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem centroid_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex k P n}
    (h : Set.range s₁.points = Set.range s₂.points) :
    Finset.univ.centroid k s₁.points = Finset.univ.centroid k s₂.points

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h : s₁.points '' ↑univ = s₂.points '' ↑univ
⊢ centroid k univ s₁.points = centroid k univ s₂.points

Tactic:
exact
  Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
    (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
    (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ centroid k univ s₁.points = centroid k univ s₂.points

Tactic:
rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h : s₁.points '' ↑univ = s₂.points '' ↑univ
⊢ centroid k univ s₁.points = centroid k univ s₂.points
-- Mathlib/Order/LiminfLimsup.lean
/-- A bounded below function `u` is in particular eventually bounded below. -/
lemma _root_.BddBelow.isBoundedUnder_of_range (hu : BddBelow (Set.range u)) :
    f.IsBoundedUnder (· ≥ ·) u := BddBelow.isBoundedUnder (s := univ) f.univ_mem (by simpa)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
hu : BddBelow (range u)
⊢ BddBelow (u '' univ)

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
rw [lt_div_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_compl_comm (a b : α) : a ⇨ bᶜ = b ⇨ aᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
simp_rw [← himp_bot, himp_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    k ∈ m.alter k f ↔ (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

Tactic:
rw [mem_iff_contains, contains_alter_self h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
    (m.insertIfNew k v).getKey a h₁ =
      if h₂ : k == a ∧ m.contains k = false then k
      else m.getKey a (contains_of_contains_insertIfNew' _ h h₁ h₂)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
h₁ : (m.insertIfNew k v).contains a = true
⊢ (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯

Tactic:
simp_to_model [insertIfNew] using List.getKey_insertEntryIfNew

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_star_mul_self' {x : E} : ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖

Tactic:
rw [norm_star_mul_self, norm_star]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_hom_app_one : (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm'_smul_le_mul_eLpNorm' {p q r : ℝ} {f : α → E} (hf : AEStronglyMeasurable f μ)
    {φ : α → 𝕜} (hφ : AEStronglyMeasurable φ μ) (hp0_lt : 0 < p) (hpq : p < q)
    (hpqr : 1 / p = 1 / q + 1 / r) : eLpNorm' (φ • f) p μ ≤ eLpNorm' φ q μ * eLpNorm' f r μ

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : BoundedSMul 𝕜 E
p q r : ℝ
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
x✝ : α
⊢ ‖(fun x1 x2 => x1 • x2) (φ x✝) (f x✝)‖₊ ≤ 1 * ‖φ x✝‖₊ * ‖f x✝‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_sUnion {S : Set (Set X)} (hS : S.Countable) : dimH (⋃₀ S) = ⨆ s ∈ S, dimH s

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
S : Set (Set X)
hS : S.Countable
⊢ dimH (⋃₀ S) = ⨆ s ∈ S, dimH s

Tactic:
rw [sUnion_eq_biUnion, dimH_bUnion hS]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem map_eq_withDensity_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
    (μ : Measure E

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ μ
⊢ map X ℙ = withDensity μ (pdf X ℙ μ)

Tactic:
rw [pdf_def, withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If G preserves equalizers and finite products, it preserves finite limits. -/
lemma preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts [HasEqualizers C]
    [HasFiniteProducts C] (G : C ⥤ D) [PreservesLimitsOfShape WalkingParallelPair G]
    [PreservesFiniteProducts G] : PreservesFiniteLimits G where
  preservesFiniteLimits

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
⊢ ∀ (J : Type) [inst : SmallCategory J] [inst_1 : FinCategory J], PreservesLimitsOfShape J G

Tactic:
intros

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasFiniteProducts C
G : C ⥤ D
inst✝³ : PreservesLimitsOfShape WalkingParallelPair G
inst✝² : PreservesFiniteProducts G
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ G

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasFiniteProducts C
G : C ⥤ D
inst✝³ : PreservesLimitsOfShape WalkingParallelPair G
inst✝² : PreservesFiniteProducts G
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ G

Tactic:
apply preservesLimit_of_preservesEqualizers_and_product

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_mk (f : α → Vector β m) (a : Array α) (h : a.size = n) :
    (Vector.mk a h).flatMap f =
      Vector.mk (a.flatMap (fun a => (f a).toArray)) (by simp [h, Array.map_const']) := rfl

Proof state:
α : Type ?u.12936
β : Type ?u.12933
m n : Nat
f : α → Vector β m
a : Array α
h : a.size = n
⊢ (Array.flatMap (fun a => (f a).toArray) a).size = n * m

Tactic:
simp [h, Array.map_const']

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem toReal_inv (a : ℝ≥0∞) : a⁻¹.toReal = a.toReal⁻¹

Proof state:
a : ℝ≥0∞
⊢ a⁻¹.toReal = a.toReal⁻¹

Tactic:
simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime)
    (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Proof state:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
  Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
    |>.emultiplicity_eq_multiplicity,     ← padicValNat_def' ha.ne_one (Nat.pos_of_ne_zero hb),
  Nat.cast_le]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq' : cos x ^ 2 = 1 - sin x ^ 2

Proof state:
x : ℝ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Topology/Order/Hom/Esakia.lean
theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/WithTop.lean
theorem sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Proof state:
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
induction a <;> induction b <;>
  simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, top_sub_coe, false_and, Ne,
    not_true_eq_false, not_false_eq_true, and_false, and_self]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean
lemma range_le_equalizer_iff {G : Cᵒᵖ ⥤ Type w} (φ : G ⟶ A.toPresheaf) :
    range (φ ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ φ ≫ f = φ ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
G : Cᵒᵖ ⥤ Type w
φ : G ⟶ A.toPresheaf
⊢ range (φ ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ φ ≫ f = φ ≫ g

Tactic:
rw [NatTrans.ext_iff]

Result:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
G : Cᵒᵖ ⥤ Type w
φ : G ⟶ A.toPresheaf
⊢ range (φ ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
G : Cᵒᵖ ⥤ Type w
φ : G ⟶ A.toPresheaf
⊢ range (φ ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app

Tactic:
simp [le_def, Set.subset_def, funext_iff, CategoryTheory.types_ext_iff]

Result:
no goals
-- Mathlib/Data/Fintype/Defs.lean
theorem mem_univ_val : ∀ x, x ∈ (univ : Finset α).1

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ univ.val

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_dropLast : ∀ (xs : List α), xs.dropLast.length = xs.length - 1
  | [] => rfl
  | x::xs => by simp

Proof state:
α : Type u_1
x : α
xs : List α
⊢ (x :: xs).dropLast.length = (x :: xs).length - 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_add_one (n : ℤ) : T R (n + 1) = 2 * X * T R n - T R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 1) = 2 * X * T R n - T R (n - 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem const_inv {x : β} (hx : x ≠ 0) :
    const abv x⁻¹ = inv (const abv x) (by rwa [const_limZero]) :=
  rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ ¬(const abv x).LimZero

Tactic:
rwa [const_limZero]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
lemma IntermediateField.isSeparable_of_mem_isSeparable {L : IntermediateField F E}
    [Algebra.IsSeparable F L] {x : E} (h : x ∈ L) : IsSeparable F x

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

Tactic:
simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (K := L) ⟨x, h⟩

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem nat_eq_one_iff (m : ℕ) : padicNorm p m = 1 ↔ ¬p ∣ m

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ ¬p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem eventuallyConst_inv_set_ae :
    EventuallyConst (s⁻¹ : Set G) (ae μ) ↔ EventuallyConst s (ae μ)

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup₂_le_iff {f : ∀ i, κ i → α} : ⨆ (i) (j), f i j ≤ a ↔ ∀ i j, f i j ≤ a

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
simp_rw [iSup_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem succ_ne_zero (n : Nat) : succ n ≠ 0

Proof state:
n : Nat
⊢ n.succ ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem x_sub_y_dvd_pow_lem (y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ) :
    (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) =
      y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

Proof state:
y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ
⊢ (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

Tactic:
ring

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
  pullbackRightPullbackFstIso_inv_snd_snd, pullback.lift_snd, Category.comp_id,
  pullbackRightPullbackFstIso_hom_snd]

Result:
no goals
-- Mathlib/Data/Nat/Periodic.lean
theorem periodic_mod (a : ℕ) : Periodic (fun n => n % a) a

Proof state:
a : ℕ
⊢ Periodic (fun n => n % a) a

Tactic:
simp only [forall_const, eq_self_iff_true, add_mod_right, Periodic]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_add_erase (a : α) (f : α →₀ M) : single a (f a) + f.erase a = f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ single a (f a) + erase a f = f

Tactic:
rw [← update_eq_single_add_erase, update_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem shrink_eq_take (a : Array α) (n : Nat) : a.shrink n = a.take n

Proof state:
α : Type u_1
a : Array α
n : Nat
⊢ a.shrink n = a.take n

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingNorm_smul_le_hammingNorm [Zero α] [∀ i, SMulWithZero α (β i)] {k : α}
    {x : ∀ i, β i} : hammingNorm (k • x) ≤ hammingNorm x :=
  hammingNorm_comp_le_hammingNorm (fun i (c : β i) => k • c) fun i => by simp_rw [smul_zero]

Proof state:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0

Tactic:
simp_rw [smul_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.dist_0_eq_abs (x : ℝ) : dist x 0 = |x|

Proof state:
x : ℝ
⊢ dist x 0 = |x|

Tactic:
simp [Real.dist_eq]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem singleton_subset_singleton : ({a} : Set α) ⊆ {b} ↔ a = b

Proof state:
α : Type u
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem integral_truncation_eq_intervalIntegral (hf : AEStronglyMeasurable f μ) {A : ℝ}
    (hA : 0 ≤ A) : ∫ x, truncation f A x ∂μ = ∫ y in -A..A, y ∂Measure.map f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂Measure.map f μ

Tactic:
simpa using moment_truncation_eq_intervalIntegral hf hA one_ne_zero

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem toList'_cons (l : List α) (s : WSeq α) (a : α) :
    Computation.corec (fun ⟨l, s⟩ =>
      match Seq.destruct s with
      | none => Sum.inl l.reverse
      | some (none, s') => Sum.inr (l, s')
      | some (some a, s') => Sum.inr (a::l, s')) (l, cons a s) =
      (Computation.corec (fun ⟨l, s⟩ =>
        match Seq.destruct s with
        | none => Sum.inl l.reverse
        | some (none, s') => Sum.inr (l, s')
        | some (some a, s') => Sum.inr (a::l, s')) (a::l, s)).think :=
  destruct_eq_think <| by simp [toList, cons]

Proof state:
α : Type u
l : List α
s : WSeq α
a : α
⊢ (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, cons a s)).destruct =
    Sum.inr
      (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (a :: l, s))

Tactic:
simp [toList, cons]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isCycle_of_prime_order'' {σ : Perm α} (h1 : (Fintype.card α).Prime)
    (h2 : orderOf σ = Fintype.card α) : σ.IsCycle :=
  isCycle_of_prime_order' ((congr_arg Nat.Prime h2).mpr h1) <| by
    rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_right (orderOf_pos σ)]
    exact one_lt_two

Proof state:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ Fintype.card α < 2 * orderOf σ

Tactic:
rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_right (orderOf_pos σ)]

Result:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 < 2

Proof state:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 < 2

Tactic:
exact one_lt_two

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem shiftLeftNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
    x' <<< n = x <<< n

Proof state:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x' <<< n = x <<< n

Tactic:
simp[*]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_equiv (f : α ≃ β) (s : Set β) : #(f ⁻¹' s) = #s

Proof state:
α β : Type u
f : α ≃ β
s : Set β
⊢ #↑(⇑f ⁻¹' s) = #↑s

Tactic:
simpa using mk_preimage_equiv_lift f s

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem mem_closure_iff_comap_neBot :
    x ∈ closure s ↔ NeBot (comap ((↑) : s → X) (𝓝 x))

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure s ↔ (comap Subtype.val (𝓝 x)).NeBot

Tactic:
simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
  SetCoe.exists, exists_prop]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.compIso_inv_comp_image_ι [HasImage f] [IsIso g] :
    (image.compIso f g).inv ≫ image.ι f = image.ι (f ≫ g) ≫ inv g

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage (f ≫ g) ≫ (compIso f g).inv ≫ ι f = factorThruImage (f ≫ g) ≫ ι (f ≫ g) ≫ inv g

Tactic:
simp [image.compIso]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).inv ≫ ι f = ι (f ≫ g) ≫ inv g

Tactic:
ext

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage (f ≫ g) ≫ (compIso f g).inv ≫ ι f = factorThruImage (f ≫ g) ≫ ι (f ≫ g) ≫ inv g
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem rightAdjointUniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (x : D) :
    F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ F.map ((adj1.rightAdjointUniq adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
simp [rightAdjointUniq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_eq_iInf (s : Set α) : μ s = ⨅ (t) (_ : s ⊆ t) (_ : MeasurableSet t), μ t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t

Tactic:
rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem mul_conj (z : K) : z * conj z = ‖z‖ ^ 2

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z * (starRingEnd K) z = ↑‖z‖ ^ 2

Tactic:
apply ext <;> simp [← ofReal_pow, norm_sq_eq_def, mul_comm]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Set.image2 f`. -/
lemma image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (s : Set α) :
    image2 f s {b} = s

Proof state:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ image2 f s {b} = s

Tactic:
rw [image2_singleton_right, funext h, image_id']

Result:
no goals