harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_iff_forall_containsKey [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
    l.isEmpty ↔ ∀ a, containsKey a l = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
l : List ((a : α) × β a)
⊢ l.isEmpty = true ↔ ∀ (a : α), containsKey a l = false

Tactic:
simp only [isEmpty_iff_forall_isSome_getEntry?, containsKey_eq_isSome_getEntry?]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_eq_seq {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = (Prod.mk '' s).seq t

Tactic:
rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t

Proof state:
c : Prop
inst✝ : Decidable c
α : Sort u_1
t : α
⊢ (if c then t else t) = t

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem eq_zero_of_fst_eq_zero {z x} {y : M} (h : z * algebraMap R S y = algebraMap R S x)
    (hx : x = 0) : z = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = (algebraMap R S) x
hx : x = 0
⊢ z = 0

Tactic:
rw [hx, (algebraMap R S).map_zero] at h

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0

Tactic:
exact (IsUnit.mul_left_eq_zero (IsLocalization.map_units S y)).1 h

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A

Proof state:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ finrank F K * finrank K A = finrank F A

Tactic:
simp_rw [finrank]

Result:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)

Proof state:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)

Tactic:
rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
  lift_rank_mul_lift_rank, toNat_lift]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
theorem alternatization_apply_apply (v : ι → M) :
    alternatization f v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f (v ∘ σ)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
⊢ (alternatization f) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f (v ∘ ⇑σ)

Tactic:
simp [alternatization, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem map_subtype {p : α → Prop} {o : Option { x // p x }}
    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    o.map f = o.unattach.map g

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
o : Option { x // p x }
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map f o = Option.map g o.unattach

Tactic:
cases o <;> simp [hf]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_discrete_rng {α} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β]
    {f : α → β} : Continuous f ↔ ∀ b : β, IsOpen (f ⁻¹' {b}) :=
  ⟨fun h _ => (isOpen_discrete _).preimage h, fun h => ⟨fun s _ => by
    rw [← biUnion_of_singleton s, preimage_iUnion₂]
    exact isOpen_biUnion fun _ _ => h _⟩⟩

Proof state:
β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen (f ⁻¹' {b})
s : Set β
x✝ : IsOpen s
⊢ IsOpen (f ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Result:
β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen (f ⁻¹' {b})
s : Set β
x✝ : IsOpen s
⊢ IsOpen (⋃ i ∈ s, f ⁻¹' {i})

Proof state:
β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen (f ⁻¹' {b})
s : Set β
x✝ : IsOpen s
⊢ IsOpen (⋃ i ∈ s, f ⁻¹' {i})

Tactic:
exact isOpen_biUnion fun _ _ => h _

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
lemma isIso_of_toNatTrans_isIso (α : F ⟶ G) [IsIso (X := F.toFunctor) α.toNatTrans] : IsIso α :=
  have : IsIso ((forgetful 𝒳 𝒴).map α)

Proof state:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
inst✝ : IsIso α.toNatTrans
⊢ IsIso ((forgetful 𝒳 𝒴).map α)

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_map {l : Array α} (f : α → β) :
    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ (map f l).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      { toList := toList✝ }.attach

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_min {a b : ℝ≥0∞} (hr : a ≠ ∞) (hp : b ≠ ∞) :
    ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b) :=
  (le_total a b).elim (fun h => by simp only [h, ENNReal.toReal_mono hp h, min_eq_left])
    fun h => by simp only [h, ENNReal.toReal_mono hr h, min_eq_right]

Proof state:
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ (a ⊓ b).toReal = a.toReal ⊓ b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hp h, min_eq_left]

Result:
no goals

Proof state:
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ (a ⊓ b).toReal = a.toReal ⊓ b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hr h, min_eq_right]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma linearEquiv_symm_var (g : relations.G) :
    h.linearEquiv.symm (solution.var g) = relations.toQuotient (Finsupp.single g 1) :=
  h.linearEquiv.injective (by simp)

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
g : relations.G
⊢ h.linearEquiv (h.linearEquiv.symm (solution.var g)) = h.linearEquiv (relations.toQuotient (Finsupp.single g 1))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem exists_insert_toList_zoom_nil {t : RBNode α} (ht : Balanced t c n)
    (e : zoom (cmp v) t = (nil, p)) :
    ∃ L R, t.toList = L ++ R ∧ (t.insert cmp v).toList = L ++ v :: R :=
  ⟨p.listL, p.listR, by simp [← zoom_toList e, insert_toList_zoom_nil ht e]⟩

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
p : Path α
v : α
t : RBNode α
ht : t.Balanced c n
e : zoom (cmp v) t = (nil, p)
⊢ t.toList = p.listL ++ p.listR ∧ (insert cmp t v).toList = p.listL ++ v :: p.listR

Tactic:
simp [← zoom_toList e, insert_toList_zoom_nil ht e]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_I : arg I = π / 2

Proof state:
⊢ I.arg = π / 2

Tactic:
simp [arg, le_refl]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_map_map (f : E →+* L) :
    relfinrank (A.map f) (B.map f) = relfinrank A B

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : E →+* L
⊢ (map f A).relfinrank (map f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_map_map A B f))

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_diagonal_const (x : α) (v : m → α) :
    v ᵥ* (diagonal fun _ => x) = MulOpposite.op x • v

Proof state:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
⊢ (v ᵥ* diagonal fun x_1 => x) = MulOpposite.op x • v

Tactic:
ext

Result:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ (v ᵥ* diagonal fun x_1 => x) x✝ = (MulOpposite.op x • v) x✝

Proof state:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ (v ᵥ* diagonal fun x_1 => x) x✝ = (MulOpposite.op x • v) x✝

Tactic:
simp [vecMul_diagonal]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_mul_right [NormalizedGCDMonoid α] (a b c : α) :
    lcm (b * a) (c * a) = lcm b c * normalize a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
⊢ lcm (b * a) (c * a) = lcm b c * normalize a

Tactic:
simp only [mul_comm, lcm_mul_left]

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem trace_eq_sum_roots [FiniteDimensional K L] {x : L}
    (hF : (minpoly K x).Splits (algebraMap K F)) :
    algebraMap K F (Algebra.trace K L x) =
      finrank K⟮x⟯ L • ((minpoly K x).aroots F).sum

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
F : Type u_6
inst✝² : Field F
inst✝¹ : Algebra K F
inst✝ : FiniteDimensional K L
x : L
hF : Splits (algebraMap K F) (minpoly K x)
⊢ (algebraMap K F) ((Algebra.trace K L) x) = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum

Tactic:
rw [trace_eq_trace_adjoin K x, Algebra.smul_def, RingHom.map_mul, ← Algebra.smul_def,
  IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF, IsScalarTower.algebraMap_smul]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) :
    X.δ i.succ ≫ X.σ (Fin.castSucc j) = X.σ j ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_gt H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.δ i.succ ≫ X.σ j.castSucc = X.σ j ≫ X.δ i

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_Iio_same : Iic a \ Iio a = {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ Iic a \ Iio a = {a}

Tactic:
rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_mem_Iic)]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem Disjoint.symmDiff_eq_sup {a b : α} (h : Disjoint a b) : a ∆ b = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b

Tactic:
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.sub (h : HasIntegral I l f vol y) (h' : HasIntegral I l g vol y') :
    HasIntegral I l (f - g) vol (y - y')

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
h : HasIntegral I l f vol y
h' : HasIntegral I l g vol y'
⊢ HasIntegral I l (f - g) vol (y - y')

Tactic:
simpa only [sub_eq_add_neg] using h.add h'.neg

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_succ (o) {a} (h : fundamentalSequence o = Sum.inl (some a)) :
    fastGrowing o = fun i => (fastGrowing a)^[i] i

Proof state:
o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ o.fastGrowing = fun i => a.fastGrowing^[i] i

Tactic:
rw [fastGrowing_def h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_mul_of_tdiv_eq_left {a b c : Int}
    (H1 : b ∣ a) (H2 : a.tdiv b = c) : a = c * b

Proof state:
a b c : Int
H1 : b ∣ a
H2 : a.tdiv b = c
⊢ a = c * b

Tactic:
rw [Int.mul_comm, Int.eq_mul_of_tdiv_eq_right H1 H2]

Result:
no goals
-- Mathlib/Data/Complex/Determinant.lean
theorem det_conjAe : LinearMap.det conjAe.toLinearMap = -1

Proof state:
⊢ 1 * -1 - 0 * 0 = -1

Tactic:
simp

Result:
no goals

Proof state:
⊢ LinearMap.det conjAe.toLinearMap = -1

Tactic:
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]

Result:
⊢ 1 * -1 - 0 * 0 = -1
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem mem_iff_pullback_eq_top (f : Y ⟶ X) : S f ↔ S.pullback f = ⊤

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ pullback f S = ⊤

Tactic:
rw [← id_mem_iff_eq_top, pullback_apply, id_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.filter_toArray (p : α → Bool) (l : List α) :
    l.toArray.filter p = (l.filter p).toArray

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ filter p l.toArray = (List.filter p l).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma unitForward_naturality₁ {F G : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G)
    (hε : ε ≫ μ = η) (X : C) (p : YonedaCollection (restrictedYonedaObj η) X) :
    unitForward μ X (p.map₁ (restrictedYonedaObjMap₁ ε hε)) = ε.app _ (unitForward η X p)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ unitForward μ X (YonedaCollection.map₁ (restrictedYonedaObjMap₁ ε hε) p) = ε.app (op X) (unitForward η X p)

Tactic:
simp [unitForward]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal

Tactic:
rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div_eq_of_le_mod_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) (hc0 : 0 < c) :
    (a + b) / c = a / c + b / c + 1

Proof state:
a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + 1

Tactic:
rw [add_div hc0, if_pos hc]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_unop_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(opLinearEquiv R).symm) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ n

Tactic:
rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default

Tactic:
simp only [getKey!_alter, beq_self_eq_true, reduceIte]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem coe_sSup_of_directedOn {S : Set (Subring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
R : Type u
inst✝ : Ring R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_right (e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 _

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ e.inv.right ≫ e.hom.right = 𝟙 g.right

Tactic:
rw [← comp_right, e.inv_hom_id, id_right]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem inv_mul_of_eq {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * a = 1

Tactic:
rw [← h, u.inv_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_comm (hf : Integrable (fun x ↦ exp (f x)) μ) {g : α → ℝ}
    (hg : Integrable (fun x ↦ exp (g x)) μ) :
    (μ.tilted f).tilted g = (μ.tilted g).tilted f

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
hg : Integrable (fun x => rexp (g x)) μ
⊢ (μ.tilted f).tilted g = (μ.tilted g).tilted f

Tactic:
rw [tilted_tilted hf, add_comm, tilted_tilted hg]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one (n : ℤ) : adicAbv v n ≤ 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
n : ℤ
⊢ (adicAbv v) ↑n ≤ 1

Tactic:
simp [← AbsoluteValue.apply_natAbs_eq, adicAbv_natCast_le_one]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.subset_closure_diff_singleton (hC : M.IsCircuit C) (e : α) :
    C ⊆ M.closure (C \ {e})

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure (C \ {e})

Tactic:
rw [hC.closure_diff_singleton_eq]

Result:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure C

Tactic:
exact M.subset_closure _ hC.subset_ground

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
theorem invOf_ι_mul_ι_mul_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] :
    ⅟ (ι Q a) * ι Q b * ι Q a = ι Q ((⅟ (Q a) * QuadraticMap.polar Q a b) • a - b)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
a b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ ⅟((ι Q) a) * (ι Q) b * (ι Q) a = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub,
  smul_smul, smul_smul, invOf_mul_self, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem fst_lt_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l

Proof state:
α : Type u_1
x : Nat × α
l : List α
h : x ∈ l.enum
⊢ x.fst < l.length

Tactic:
simpa using fst_lt_add_of_mem_enumFrom h

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem ContMDiffWithinAt.contMDiffOn
    [IsManifold I n M] [IsManifold I' n M']
    (hm : m ≤ n) (h' : m = ∞ → n = ω)
    (h : ContMDiffWithinAt I I' n f s x) :
    ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h✝ : ContMDiffWithinAt I I' n f s x
_u : Set M
uo : IsOpen _u
xu : x ∈ _u
h : ContMDiffOn I I' m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Tactic:
exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContMDiffWithinAt I I' n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Tactic:
let ⟨_u, uo, xu, h⟩ := h.contMDiffOn' hm h'

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h✝ : ContMDiffWithinAt I I' n f s x
_u : Set M
uo : IsOpen _u
xu : x ∈ _u
h : ContMDiffOn I I' m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_eq_filter (s₁ s₂ : Finset α) : s₁ \ s₂ = filter (· ∉ s₂) s₁ :=
  ext fun _ => by simp [mem_sdiff, mem_filter]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ \ s₂ ↔ x✝ ∈ filter (fun x => x ∉ s₂) s₁

Tactic:
simp [mem_sdiff, mem_filter]

Result:
no goals