harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem coe_multilinearMap_mk (f : (ι → M) → N) (h₁ h₂ h₃) :
    ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) =
      ⟨f, @h₁, @h₂⟩

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : (ι → M) → N
h₁ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (update m i (c • x)) = c • f (update m i x)
h₃ :
  ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯ }.toFun v = 0
⊢ ↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ } =
    { toFun := f, map_update_add' := h₁, map_update_smul' := h₂ }

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integrable_compProd_iff ⦃f : β × γ → E⦄ (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
    Integrable f ((κ ⊗ₖ η) a) ↔
      (∀ᵐ x ∂κ a, Integrable (fun y => f (x, y)) (η (a, x))) ∧
        Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ Integrable f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, Integrable (fun y => f (x, y)) (η (a, x))) ∧
      Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
simp only [Integrable, hasFiniteIntegral_compProd_iff' hf, hf.norm.integral_kernel_compProd,
  hf, hf.compProd_mk_left, eventually_and, true_and]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
theorem coe_range : AlgebraicIndependent R ((↑) : range x → A)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
simpa using hx.comp _ (rangeSplitting_injective x)

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_top_right : H.relindex ⊤ = H.index

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relindex ⊤ = H.index

Tactic:
rw [← relindex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_comp_exp_atTop {f : ℝ → α} :
    Tendsto (fun x => f (exp x)) atTop l ↔ Tendsto f atTop l

Proof state:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (rexp x)) atTop l ↔ Tendsto f atTop l

Tactic:
simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]

Result:
no goals
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem d_eq_unop_d (n : ℕ) :
    objD X n =
      (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X))
          n).unop

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • (((cosimplicialSimplicialEquiv C).functor.obj (op X)).δ x).unop

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop

Tactic:
simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • (((cosimplicialSimplicialEquiv C).functor.obj (op X)).δ x).unop
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem coe_linearMapAt_of_mem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
⊢ ⇑(Trivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2

Tactic:
simp_rw [coe_linearMapAt, if_pos hb]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_zero (a n' : ℤ) (hn' : n + a = n') :
    (0 : Cochain (K⟦a⟧) L n').leftUnshift n hn' = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ leftUnshift 0 n hn' = 0

Tactic:
change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn').symm 0 = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn').symm 0 = 0

Tactic:
apply _root_.map_zero

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) :
    (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id _ _

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id A (A ⊗[R] CliffordAlgebra Q)

Tactic:
ext v

Result:
case hb.a.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (((AlgHom.restrictScalars R ((toBaseChange A Q).comp (ofBaseChange A Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v =
    (((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] CliffordAlgebra Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v

Proof state:
case hb.a.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (((AlgHom.restrictScalars R ((toBaseChange A Q).comp (ofBaseChange A Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v =
    (((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] CliffordAlgebra Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_mk_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
    homMk' (mk f) (g' ≫ g) = eqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f)) g' ≫ homMk' (mk f) g :=
  homMk'_comp _ _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ (mk f).hom) = mk (S.map g' ≫ (mk (S.map g ≫ f)).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem right_eq_midpoint_iff {x y : P} : y = midpoint R x y ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ y = midpoint R x y ↔ x = y

Tactic:
rw [eq_comm, midpoint_eq_right_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_coe_center (z w : ℍ) (r : ℝ) : dist (z : ℂ) (w.center r) =
    √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Proof state:
z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Tactic:
rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem swap_eq_eq {o : Ordering} : o.swap = .eq ↔ o = .eq

Proof state:
o : Ordering
⊢ o.swap = eq ↔ o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/Exterior.lean
@[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ :=
  ⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s = ∅ → exterior s = ∅

Tactic:
rintro rfl

Result:
X : Type u_2
inst✝ : TopologicalSpace X
⊢ exterior ∅ = ∅

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
⊢ exterior ∅ = ∅

Tactic:
exact exterior_empty

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem sum_zero_index {S : Type*} [AddCommMonoid S] (f : ℕ → R → S) : (0 : R[X]).sum f = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
simp [sum]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_filter_ne_zero : {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z :=
  Finset.centerMass_subset z (filter_subset _ _) fun i hit hit' => by
    simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
i : ι
hit : i ∈ t
hit' : i ∉ filter (fun i => w i ≠ 0) t
⊢ w i = 0

Tactic:
simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem id [PerfectRing R p] : PerfectionMap p (RingHom.id R) :=
  { injective := fun _ _ hxy => hxy 0
    surjective := fun f hf =>
      ⟨f 0, fun n =>
        show ((frobeniusEquiv R p).symm)^[n] (f 0) = f n from
          Nat.recOn n rfl fun n ih => injective_pow_p R p <| by
            rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]⟩ }

Proof state:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ (⇑(frobeniusEquiv R p).symm)^[n.succ] (f 0) ^ p = f n.succ ^ p

Tactic:
rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma prop_map_succ (i : J) (hi : i < j) :
    Φ.prop (iter.F.map (homOfLE (Order.le_succ i) :
      ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ Φ.prop (iter.F.map (homOfLE ⋯))

Tactic:
rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_equiv_symm (e : α ≃ β) (f : Filter β) : map e.symm f = comap e f :=
  map_injective e.injective <| by
    rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map (⇑e) (map (⇑e.symm) f) = map (⇑e) (comap (⇑e) f)

Tactic:
rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem range_extend_subset (f : α → β) (g : α → γ) (g' : β → γ) :
    range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' (range f)ᶜ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
classical
rintro _ ⟨y, rfl⟩
rw [extend_def]
split_ifs with h
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' (range f)ᶜ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
rw [extend_def]

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' (range f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
rintro _ ⟨y, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
-- Mathlib/MeasureTheory/Group/Action.lean
theorem smulInvariantMeasure_map [SMul M α] [SMul M β]
    [MeasurableSMul M β]
    (μ : Measure α) [SMulInvariantMeasure M α μ] (f : α → β)
    (hsmul : ∀ (m : M) a, f (m • a) = m • f a) (hf : Measurable f) :
    SMulInvariantMeasure M β (map f μ) where
  measure_preimage_smul m S hS := calc
    map f μ ((m • ·) ⁻¹' S)
    _ = μ (f ⁻¹' ((m • ·) ⁻¹' S)) := map_apply hf <| hS.preimage (measurable_const_smul _)
    _ = μ ((m • f ·) ⁻¹' S)

Proof state:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x => f (m • x)) ⁻¹' S) = μ ((fun x => m • x) ⁻¹' (f ⁻¹' S))

Tactic:
rw [← preimage_preimage]

Result:
no goals

Proof state:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x => m • x) ⁻¹' (f ⁻¹' S)) = μ (f ⁻¹' S)

Tactic:
rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]

Result:
no goals

Proof state:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x => m • f x) ⁻¹' S) = μ ((fun x => f (m • x)) ⁻¹' S)

Tactic:
simp_rw [hsmul]

Result:
no goals

Proof state:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ (f ⁻¹' ((fun x => m • x) ⁻¹' S)) = μ ((fun x => m • f x) ⁻¹' S)

Tactic:
rw [preimage_preimage]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_apply_eq_zero_iff : p.toOuterMeasure s = 0 ↔ Disjoint p.support s

Proof state:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s

Tactic:
exact funext_iff.symm.trans Set.indicator_eq_zero'

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure s = 0 ↔ Disjoint p.support s

Tactic:
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]

Result:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t

Proof state:
𝕂 : Type u_1
𝔸 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t

Tactic:
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem neg_add {R} [Ring R] {a₁ a₂ b₁ b₂ : R}
    (_ : -a₁ = b₁) (_ : -a₂ = b₂) : -(a₁ + a₂) = b₁ + b₂

Proof state:
R : Type u_2
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
-- Mathlib/Data/Sign.lean
theorem self_eq_neg_iff (a : SignType) : a = -a ↔ a = 0

Proof state:
a : SignType
⊢ a = -a ↔ a = 0

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1)

Proof state:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
simpa only [← Int.ofNat_succ, zpow_natCast] using integral_zpow (Or.inl n.cast_nonneg)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_mod_eq_add_mod_left (c : ℕ) (H : a % d = b % d) : (c + a) % d = (c + b) % d

Proof state:
a b d c : ℕ
H : a % d = b % d
⊢ (c + a) % d = (c + b) % d

Tactic:
rw [Nat.add_comm, add_mod_eq_add_mod_right _ H, Nat.add_comm]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem disjoint_nhds_atBot (a : α) : Disjoint (𝓝 a) atBot

Proof state:
α : Type u
inst✝³ : Preorder α
inst✝² : NoBotOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_smul_of_tower [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M]
    [Module S N] [IsScalarTower S R N] (a : S)
    (x : M) : Q (a • x) = (a * a) • Q x

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x : M
⊢ Q (a • x) = (a * a) • Q x

Tactic:
rw [← IsScalarTower.algebraMap_smul R a x, map_smul, ← RingHom.map_mul, algebraMap_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem zero_rpow_def (y : ℝ) : (0 : ℝ≥0∞) ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

Proof state:
case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

Tactic:
simp [H, ne_of_gt, zero_rpow_of_pos, lt_irrefl]

Result:
no goals

Proof state:
case inr.inl

⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤

Tactic:
simp [lt_irrefl]

Result:
no goals

Proof state:
y : ℝ
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

Tactic:
rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)

Result:
case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

case inr.inl

⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤

case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

Proof state:
case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

Tactic:
simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_left (x y : V) (r : ℝ) :
    (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

Tactic:
rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem exists_coeff_ne_zero_iff_ne_zero : (∃ n : ℕ, coeff R n φ ≠ 0) ↔ φ ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (¬∃ n, (coeff R n) φ ≠ 0) ↔ ¬φ ≠ 0

Tactic:
push_neg

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ (n : ℕ), (coeff R n) φ = 0) ↔ φ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∃ n, (coeff R n) φ ≠ 0) ↔ φ ≠ 0

Tactic:
refine not_iff_not.mp ?_

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (¬∃ n, (coeff R n) φ ≠ 0) ↔ ¬φ ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ (n : ℕ), (coeff R n) φ = 0) ↔ φ = 0

Tactic:
simp [(coeff R _).map_zero]

Result:
no goals
-- Mathlib/Logic/Embedding/Set.lean
theorem Function.Embedding.sumSet_range {s t : Set α} (h : Disjoint s t) :
    range (Function.Embedding.sumSet h) = s ∪ t

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ range ⇑(sumSet h) = s ∪ t

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_symm_single : b.repr.symm (Finsupp.single i c) = c • b i :=
  calc
    b.repr.symm (Finsupp.single i c) = b.repr.symm (c • Finsupp.single i (1 : R))

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

Tactic:
rw [Finsupp.smul_single', mul_one]

Result:
no goals

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

Tactic:
rw [LinearEquiv.map_smul, repr_symm_single_one]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma ext_iff_isCircuit {M₁ M₂ : Matroid α} :
    M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ C, M₁.IsCircuit C ↔ M₂.IsCircuit C :=
  ⟨fun h ↦ by simp [h], fun h ↦ ext_isCircuit h.1 fun C hC ↦ h.2 (C := C)⟩

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- A number that divides an `n`-smooth number is itself `n`-smooth. -/
lemma mem_smoothNumbers_of_dvd {n m k : ℕ} (h : m ∈ smoothNumbers n) (h' : k ∣ m) :
    k ∈ smoothNumbers n

Proof state:
n m k : ℕ
h' : k ∣ m
h : m ∈ factoredNumbers (Finset.range n)
⊢ k ∈ factoredNumbers (Finset.range n)

Tactic:
exact mem_factoredNumbers_of_dvd h h'

Result:
no goals

Proof state:
n m k : ℕ
h : m ∈ n.smoothNumbers
h' : k ∣ m
⊢ k ∈ n.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers] at h ⊢

Result:
n m k : ℕ
h' : k ∣ m
h : m ∈ factoredNumbers (Finset.range n)
⊢ k ∈ factoredNumbers (Finset.range n)