harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem condExp_prod_ae_eq_integral_condDistrib [NormedSpace ℝ F] [CompleteSpace F]
    (hX : Measurable X) (hY : AEMeasurable Y μ) (hf : StronglyMeasurable f)
    (hf_int : Integrable (fun a => f (X a, Y a)) μ) :
    μ[fun a => f (X a, Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) :=
  haveI hf_int' : Integrable f (μ.map fun a => (X a, Y a))

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : StronglyMeasurable f
hf_int : Integrable (fun a => f (X a, Y a)) μ
⊢ Integrable f (Measure.map (fun a => (X a, Y a)) μ)

Tactic:
rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prod_mk hY)]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem product_nil : ∀ l : List α, l ×ˢ (@nil β) = []
  | [] => rfl
  | _ :: l => by simp [product_cons, product_nil l]

Proof state:
α : Type u_1
β : Type u_2
head✝ : α
l : List α
⊢ (head✝ :: l) ×ˢ [] = []

Tactic:
simp [product_cons, product_nil l]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k

Proof state:
n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n.choose k

Tactic:
rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
  Nat.sub_sub_self hk, Nat.mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_factorial {n b : ℕ} [hp : Fact p.Prime] (hnb : log p n < b) :
    padicValNat p (n !) = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Proof state:
p n b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p n < b
⊢ padicValNat p n ! = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Tactic:
exact_mod_cast ((padicValNat_eq_emultiplicity (p := p) <| factorial_pos _) ▸
    Prime.emultiplicity_factorial hp.out hnb)

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem direction_altitude {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) :
    (s.altitude i).direction =
      (vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [altitude_def,
  direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
  direction_mk', direction_affineSpan, direction_affineSpan]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[simp]
lemma τ₁_ofEpiOfIsIsoOfMono_f' (φ : S₁ ⟶ S₂) (h : LeftHomologyData S₁)
    [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'

Tactic:
rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
  ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem invOf_mul_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ ⅟a * (a * b) = b

Tactic:
rw [← mul_assoc, invOf_mul_self, one_mul]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add : cos (x + y) = cos x * cos y - sin x * sin y

Proof state:
x y : ℂ
⊢ cos (x + y) = cos x * cos y - sin x * sin y

Tactic:
rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
  mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitLower_def [DecidableEq ι] {i x} (h : x ∈ Ioo (I.lower i) (I.upper i))
    (h' : ∀ j, I.lower j < update I.upper i x j :=
      (forall_update_iff I.upper fun j y => I.lower j < y).2
        ⟨h.1, fun _ _ => I.lower_lt_upper _⟩) :
    I.splitLower i x = (⟨I.lower, update I.upper i x, h'⟩ : Box ι)

Proof state:
ι : Type u_1
I : Box ι
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (I.lower i) (I.upper i)
h' : optParam (∀ (j : ι), I.lower j < update I.upper i x j) ⋯
⊢ I.splitLower i x = ↑{ lower := I.lower, upper := update I.upper i x, lower_lt_upper := h' }

Tactic:
simp (config := { unfoldPartialApp := true }) only [splitLower, mk'_eq_coe, min_eq_left h.2.le,
  update, and_self]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_diff_singleton_eq_closure (h : e ∈ M.closure (X \ {e})) :
    M.closure (X \ {e}) = M.closure X :=
  closure_diff_eq_self (by simpa)

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e : α
h : e ∈ M.closure (X \ {e})
⊢ {e} ⊆ M.closure (X \ {e})

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/Ideal/IsPrincipal.lean
theorem associatesEquivIsPrincipal_map_zero :
    (associatesEquivIsPrincipal R 0 : Ideal R) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) 0) = 0

Tactic:
rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
The completed L-function of a function `ZMod 1 → ℂ` is a scalar multiple of the completed Riemann
zeta function.
-/
lemma completedLFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) :
    completedLFunction Φ s = Φ 1 * completedRiemannZeta s

Proof state:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ completedLFunction Φ s = Φ 1 * completedRiemannZeta s

Tactic:
rw [completedLFunction_def_even (show Φ.Even from fun _ ↦ congr_arg Φ (Subsingleton.elim ..)),
  Nat.cast_one, one_cpow, one_mul, ← singleton_eq_univ 0, sum_singleton, map_zero,
  completedHurwitzZetaEven_zero, Subsingleton.elim 0 1]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma commSq : CommSq (p.map φ) (eqToHom (domain_eq p f φ)) (eqToHom (codomain_eq p f φ)) f where
  w

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f

Tactic:
simp only [fac p f φ, eqToHom_trans_assoc, eqToHom_refl, id_comp]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma kernImage_preimage_union {s : Set α} {t : Set β} :
    kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

Tactic:
rw [union_comm, kernImage_union_preimage, union_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c)

Proof state:
a b c : Prop
⊢ a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)

Tactic:
rw [@or_comm (a ∧ b), or_and_left, @or_comm c, @or_comm c]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem all_mem_nhds (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
    (∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s :=
  ((nhds_basis_opens x).forall_iff hP).trans <| by simp only [@and_comm (x ∈ _), and_imp]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
P : Set X → Prop
hP : ∀ (s t : Set X), s ⊆ t → P s → P t
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen i → P i) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s

Tactic:
simp only [@and_comm (x ∈ _), and_imp]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem union_ae_eq_right_iff_ae_subset : (s ∪ t : Set α) =ᵐ[μ] t ↔ s ≤ᵐ[μ] t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t

Tactic:
rw [union_comm, union_ae_eq_left_iff_ae_subset]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_comm (z w : ℍ) : dist z w = dist w z

Proof state:
z w : ℍ
⊢ dist z w = dist w z

Tactic:
simp only [dist_eq, dist_comm (z : ℂ), mul_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpTo_zero_iff :
    HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ x, (p x 0).curry0 = f x

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
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ (x : E), (p x 0).curry0 = f x

Tactic:
simp [hasFTaylorSeriesUpToOn_univ_iff.symm, continuous_iff_continuousOn_univ,
  hasFTaylorSeriesUpToOn_zero_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma ι_comp_colimitLeftOpIsoUnopLimit_hom (F : J ⥤ Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) :
    colimit.ι F.leftOp j ≫ (colimitLeftOpIsoUnopLimit F).hom = (limit.π F j.unop).unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ colimit.ι F.leftOp j ≫ (colimitLeftOpIsoUnopLimit F).hom = (limit.π F (unop j)).unop

Tactic:
simp [colimitLeftOpIsoUnopLimit]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_eq_iff : ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ z

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z

Tactic:
rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
  and_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_conj (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') :
    LinearEquiv.det ((e.symm.trans f).trans e) = LinearEquiv.det f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
⊢ LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f

Tactic:
rw [← Units.eq_iff, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
  eq_replicate_iff.2
    ⟨by rw [length_reverse, length_replicate],
     fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (replicate n a).reverse.length = n

Tactic:
rw [length_reverse, length_replicate]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_one_div_of_mul_eq_one_left (h : b * a = 1) : b = 1 / a

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_left h, one_div]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_one : (1 : Perm α).support = ∅

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ support 1 = ∅

Tactic:
rw [support_eq_empty_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_zero' (μ : Measure α) : μ.tilted 0 = (μ Set.univ)⁻¹ • μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ μ.tilted 0 = (μ Set.univ)⁻¹ • μ

Tactic:
change μ.tilted (fun _ ↦ 0) = (μ Set.univ)⁻¹ • μ

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (μ.tilted fun x => 0) = (μ Set.univ)⁻¹ • μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (μ.tilted fun x => 0) = (μ Set.univ)⁻¹ • μ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next : ∀ {it}, Valid it → it.hasNext → Valid it.next
  | _, h, hn => by
    let ⟨l, r, h⟩ := h.validFor
    obtain ⟨c, r, rfl⟩ := List.exists_cons_of_ne_nil (h.hasNext.1 hn)
    exact h.next.valid

Proof state:
case intro.intro
x✝ : Iterator
h✝ : x✝.Valid
hn : x✝.hasNext = true
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) x✝
⊢ x✝.next.Valid

Tactic:
exact h.next.valid

Result:
no goals

Proof state:
x✝ : Iterator
h : x✝.Valid
hn : x✝.hasNext = true
⊢ x✝.next.Valid

Tactic:
let ⟨l, r, h⟩ := h.validFor

Result:
x✝ : Iterator
h✝ : x✝.Valid
hn : x✝.hasNext = true
l r : List Char
h : ValidFor l r x✝
⊢ x✝.next.Valid

Proof state:
x✝ : Iterator
h✝ : x✝.Valid
hn : x✝.hasNext = true
l r : List Char
h : ValidFor l r x✝
⊢ x✝.next.Valid

Tactic:
obtain ⟨c, r, rfl⟩ := List.exists_cons_of_ne_nil (h.hasNext.1 hn)

Result:
case intro.intro
x✝ : Iterator
h✝ : x✝.Valid
hn : x✝.hasNext = true
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) x✝
⊢ x✝.next.Valid
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem card_le_card_mul_self {s : Finset α} : s.card ≤ (s * s).card

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_left, *]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_eq_zero_iff_deg_eq_bot : leadingCoeff p = 0 ↔ degree p = ⊥

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff = 0 ↔ p.degree = ⊥

Tactic:
rw [leadingCoeff_eq_zero, degree_eq_bot]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.map (H : IsCoprime x y) {S : Type v} [CommSemiring S] (f : R →+* S) :
    IsCoprime (f x) (f y) :=
  let ⟨a, b, h⟩ := H
  ⟨f a, f b, by rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]⟩

Proof state:
R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f a * f x + f b * f y = 1

Tactic:
rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem Option.dmap_congr {o o' : Option α} {f : (a : α) → (o = some a) → β} (h : o = o') :
    Option.dmap o f = Option.dmap o' (fun a h' => f a (h ▸ h'))

Proof state:
case refl
α : Type u
β : Type v
o : Option α
f : (a : α) → o = some a → β
⊢ Std.DHashMap.Internal.List.Option.dmap o f = Std.DHashMap.Internal.List.Option.dmap o fun a h' => f a ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
o o' : Option α
f : (a : α) → o = some a → β
h : o = o'
⊢ Std.DHashMap.Internal.List.Option.dmap o f = Std.DHashMap.Internal.List.Option.dmap o' fun a h' => f a ⋯

Tactic:
cases h

Result:
case refl
α : Type u
β : Type v
o : Option α
f : (a : α) → o = some a → β
⊢ Std.DHashMap.Internal.List.Option.dmap o f = Std.DHashMap.Internal.List.Option.dmap o fun a h' => f a ⋯
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuous_sInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} :
    UniformContinuous[u₁, sInf u₂] f ↔ ∀ u ∈ u₂, UniformContinuous[u₁, u] f

Proof state:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f

Tactic:
delta UniformContinuous

Result:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ u ∈ u₂, Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ u ∈ u₂, Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
  Set.ext fun _ => by simpa using isFixedPt_id _

Proof state:
α : Type u
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ

Tactic:
simpa using isFixedPt_id _

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem volume_apply' (I : Box ι) :
    ((volume : Measure (ι → ℝ)) I).toReal = ∏ i, (I.upper i - I.lower i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ (volume ↑I).toReal = ∏ i : ι, (I.upper i - I.lower i)

Tactic:
rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_eq_tsum (h : IsFundamentalDomain G s μ) (t : Set α) :
    μ t = ∑' g : G, μ (g • t ∩ s)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
⊢ μ t = ∑' (g : G), μ (g • t ∩ s)

Tactic:
simpa only [setLIntegral_one] using h.setLIntegral_eq_tsum' (fun _ => 1) t

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma coborder_eq_univ_iff :
    coborder s = univ ↔ IsClosed s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = univ ↔ IsClosed s

Tactic:
simp [coborder, diff_eq_empty, closure_subset_iff_isClosed]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_sub {i : Nat} {x y : BitVec w} (h : i < w) :
    (x - y)[i] = (x[i] ^^ ((~~~y + 1#w)[i] ^^ carry i x (~~~y + 1#w) false))

Proof state:
w i : Nat
x y : BitVec w
h : i < w
⊢ (x - y)[i] = (x[i] ^^ ((~~~y + 1#w)[i] ^^ carry i x (~~~y + 1#w) false))

Tactic:
simp [← getLsbD_eq_getElem, getLsbD_sub, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_right_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - c < b

Proof state:
a b c : Int
h✝ : a < b + c
h : a + -c < b + c + -c
⊢ a - c < b

Tactic:
rwa [Int.add_neg_cancel_right] at h

Result:
no goals

Proof state:
a b c : Int
h : a < b + c
⊢ a - c < b

Tactic:
have h := Int.add_lt_add_right h (-c)

Result:
a b c : Int
h✝ : a < b + c
h : a + -c < b + c + -c
⊢ a - c < b
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) :
    (modify f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
⊢ (modify f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m

Tactic:
simp [getElem?_modify]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianPDFReal_add {μ : ℝ} {v : ℝ≥0} (x y : ℝ) :
    gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

Proof state:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

Tactic:
rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem singleton_iff_unique_mem (s : Finset α) : (∃ a, s = {a}) ↔ ∃! a, a ∈ s

Proof state:
α : Type u_1
s : Finset α
⊢ (∃ a, s = {a}) ↔ ∃! a, a ∈ s

Tactic:
simp only [eq_singleton_iff_unique_mem, ExistsUnique]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem closure_isSquare : closure {x : T | IsSquare x} = sumSq T

Proof state:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
⊢ closure {x | IsSquare x} = sumSq T

Tactic:
simp [sumSq, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
lemma floorDiv_zero (b : β) : b ⌊/⌋ (0 : α) = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
b : β
⊢ b ⌊/⌋ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
    (C a * X ^ n : T[X]).aroots S = n • ({0} : Multiset S)

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).aroots S = n • {0}

Tactic:
rw [aroots_C_mul _ ha, aroots_X_pow]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.dvdNotUnit_iff_lt {I J : Ideal A} : DvdNotUnit I J ↔ J < I :=
  ⟨fun ⟨hI, H, hunit, hmul⟩ =>
    lt_of_le_of_ne (Ideal.dvd_iff_le.mp ⟨H, hmul⟩)
      (mt
        (fun h =>
          have : H = 1 := mul_left_cancel₀ hI (by rw [← hmul, h, mul_one])
          show IsUnit H from this.symm ▸ isUnit_one)
        hunit),
    fun h =>
    dvdNotUnit_of_dvd_of_not_dvd (Ideal.dvd_iff_le.mpr (le_of_lt h))
      (mt Ideal.dvd_iff_le.mp (not_le_of_lt h))⟩

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
x✝ : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
⊢ I * H = I * 1

Tactic:
rw [← hmul, h, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    k ∈ m.insert 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.insert k v

Tactic:
simp [mem_iff_contains, contains_insert_self h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_nonneg_ae (hs : MeasurableSet s) (hf : ∀ᵐ x ∂μ, x ∈ s → 0 ≤ f x) :
    0 ≤ ∫ x in s, f x ∂μ :=
  setIntegral_nonneg_of_ae_restrict <| by rwa [EventuallyLE, ae_restrict_iff' hs]

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
⊢ 0 ≤ᶠ[ae (μ.restrict s)] f

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_left_inj' (a b c : BitVec w) : (a + c == c + b) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a + c == c + b) = (a == b)

Tactic:
rw [BitVec.add_comm c b, add_left_inj]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem Filter.EventuallyEq.hasDerivAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x)
    (h₁ : f₀' = f₁') : HasDerivAtFilter f₀ f₀' x L ↔ HasDerivAtFilter f₁ f₁' x L :=
  h₀.hasFDerivAtFilter_iff hx (by simp [h₁])

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₀ f₁ : 𝕜 → F
f₀' f₁' : F
x : 𝕜
L : Filter 𝕜
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ ∀ (x : 𝕜), (smulRight 1 f₀') x = (smulRight 1 f₁') x

Tactic:
simp [h₁]

Result:
no goals
-- Mathlib/Order/Category/BoolAlg.lean
lemma comp_apply {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp, nolint simpNF] lemma natCast_eq_zero {n : ℕ} : (n : ℤ) = 0 ↔ n = 0

Proof state:
n : ℕ
⊢ ↑n = 0 ↔ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
lemma arrowMap_functor_to_top (i : J) (hi : i < j) :
    letI := hasColimitsOfShape_of_isSuccLimit C j hj
    arrowMap (functor hj iter) i j hi.le (by simp) =
      Arrow.mk (colimit.ι (inductiveSystem iter) ⟨i, hi⟩) :=
  arrowMap_ofCocone_to_top _ _ _

Proof state:
C : Type u_1
inst✝⁵ : Category.{?u.32911, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
this : HasColimitsOfShape (↑(Set.Iio j)) C := hasColimitsOfShape_of_isSuccLimit C j hj
⊢ j ≤ j

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_one_one_comp_comm (m n : ℕ) :
    (dickson 1 (1 : R) m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m)

Proof state:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ (dickson 1 1 m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m)

Tactic:
rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]

Result:
no goals