harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_zero : Integrable (fun _ => (0 : β)) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
⊢ Integrable (fun x => 0) μ

Tactic:
simp [Integrable, aestronglyMeasurable_const]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) :
    ContDiffAt 𝕜 n (fun x => -f x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => -f x) univ x

Tactic:
exact hf.neg

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (fun x => -f x) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => -f x) univ x
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_neg (n : ℤ) : normEDS b c d (-n) = -normEDS b c d n

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n

Tactic:
simp only [normEDS, preNormEDS_neg, neg_mul, even_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_one (x : ℂ) : x ^ (1 : ℂ) = x :=
  if hx : x = 0 then by simp [hx, cpow_def]
  else by rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]

Proof state:
x : ℂ
hx : ¬x = 0
⊢ x ^ 1 = x

Tactic:
rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]

Result:
no goals

Proof state:
x : ℂ
hx : x = 0
⊢ x ^ 1 = x

Tactic:
simp [hx, cpow_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma norm_mul_le_max (x y : S) :
    ‖x * y‖ ≤ max ‖x‖ ‖y‖

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
⊢ ‖x * y‖ ≤ ‖x‖ ⊔ ‖y‖

Tactic:
simpa only [le_max_iff, dist_eq_norm_div, div_inv_eq_mul, div_one, one_mul] using
  dist_triangle_max x 1 y⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a

Proof state:
w : Nat
a : BitVec w
⊢ a &&& -1#w = a

Tactic:
ext

Result:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (a &&& -1#w).getLsbD i✝ = a.getLsbD i✝

Proof state:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (a &&& -1#w).getLsbD i✝ = a.getLsbD i✝

Tactic:
simp [BitVec.negOne_eq_allOnes]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Bounds.lean
lemma harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

Proof state:
n : ℕ
⊢ harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

Tactic:
rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1)]

Result:
n : ℕ
⊢ ∑ x ∈ Finset.Ico (0 + 1) (n + 1), (↑x)⁻¹ = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

Proof state:
n : ℕ
⊢ ∑ x ∈ Finset.Ico (0 + 1) (n + 1), (↑x)⁻¹ = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

Tactic:
simp only [Nat.add_one, Nat.Ico_succ_right]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem compl_sInf : (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Proof state:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
⊢ (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Tactic:
simp only [sInf_eq_iInf, compl_iInf]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@[simp]
lemma autMap_id {A : C} [IsGalois A] : autMap (𝟙 A) = id :=
  funext fun σ ↦ autMap_unique (𝟙 A) σ _ (by simp)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A : C
inst✝ : IsGalois A
σ : Aut A
⊢ 𝟙 A ≫ (id σ).hom = σ.hom ≫ 𝟙 A

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_lt_mul_of_neg_right [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (h : b < a) (hc : c < 0) : a * c < b * c

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
⊢ a * c < b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * c < b * c

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * c < b * c

Tactic:
refine (add_lt_add_iff_right (b * d + a * d)).1 ?_

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) < b * c + (b * d + a * d)

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) < b * c + (b * d + a * d)

Tactic:
calc
  _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
  _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
  _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
@[ext]
lemma FunctorsInverting.ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D}
    (h : F₁.obj = F₂.obj) : F₁ = F₂

Proof state:
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
obj✝¹ : C ⥤ D
property✝¹ : W.IsInvertedBy obj✝¹
obj✝ : C ⥤ D
property✝ : W.IsInvertedBy obj✝
h : { obj := obj✝¹, property := property✝¹ }.obj = { obj := obj✝, property := property✝ }.obj
⊢ { obj := obj✝¹, property := property✝¹ } = { obj := obj✝, property := property✝ }

Tactic:
subst h

Result:
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
obj✝ : C ⥤ D
property✝¹ : W.IsInvertedBy obj✝
property✝ : W.IsInvertedBy { obj := obj✝, property := property✝¹ }.obj
⊢ { obj := obj✝, property := property✝¹ } =
    { obj := { obj := obj✝, property := property✝¹ }.obj, property := property✝ }

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₂ : W.FunctorsInverting D
obj✝ : C ⥤ D
property✝ : W.IsInvertedBy obj✝
h : { obj := obj✝, property := property✝ }.obj = F₂.obj
⊢ { obj := obj✝, property := property✝ } = F₂

Tactic:
cases F₂

Result:
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
obj✝¹ : C ⥤ D
property✝¹ : W.IsInvertedBy obj✝¹
obj✝ : C ⥤ D
property✝ : W.IsInvertedBy obj✝
h : { obj := obj✝¹, property := property✝¹ }.obj = { obj := obj✝, property := property✝ }.obj
⊢ { obj := obj✝¹, property := property✝¹ } = { obj := obj✝, property := property✝ }

Proof state:
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
obj✝ : C ⥤ D
property✝¹ : W.IsInvertedBy obj✝
property✝ : W.IsInvertedBy { obj := obj✝, property := property✝¹ }.obj
⊢ { obj := obj✝, property := property✝¹ } =
    { obj := { obj := obj✝, property := property✝¹ }.obj, property := property✝ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : W.FunctorsInverting D
h : F₁.obj = F₂.obj
⊢ F₁ = F₂

Tactic:
cases F₁

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₂ : W.FunctorsInverting D
obj✝ : C ⥤ D
property✝ : W.IsInvertedBy obj✝
h : { obj := obj✝, property := property✝ }.obj = F₂.obj
⊢ { obj := obj✝, property := property✝ } = F₂
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) :
    d ∣ n ↔ ∀ p k : ℕ, Prime p → p ^ k ∣ d → p ^ k ∣ n

Proof state:
case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p

Tactic:
intro h p pp

Result:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ d.factorization p ≤ n.factorization p

Proof state:
case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Result:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Proof state:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩

Result:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n

Proof state:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n

Tactic:
rw [← factorization_prime_le_iff_dvd hd hn]

Result:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p

Proof state:
n d : ℕ
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Proof state:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ ∃ x x_1, ∃ (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n

Tactic:
exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_le⟩

Result:
no goals

Proof state:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ d.factorization p ≤ n.factorization p

Tactic:
simp_rw [← pp.pow_dvd_iff_le_factorization hn]

Result:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ p ^ d.factorization p ∣ n

Proof state:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ p ^ d.factorization p ∣ n

Tactic:
exact h p _ pp (ordProj_dvd _ _)

Result:
no goals

Proof state:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

Tactic:
simp only [zero_dvd_iff, hn, false_iff, not_forall]

Result:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ ∃ x x_1, ∃ (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_mul_intCast (hx : 0 ≤ x) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul hx, rpow_intCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem mem_submodule_iff {P : Submodule R M} (b : Basis ι R P) {x : M} :
    x ∈ P ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : M)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ LinearMap.range (linearCombination R (⇑P.subtype ∘ ⇑b)) ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)

Tactic:
simp [@eq_comm _ x, Function.comp, Finsupp.linearCombination_apply]

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
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ P ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)

Tactic:
conv_lhs =>
  rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
      ← Finsupp.range_linearCombination]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ LinearMap.range (linearCombination R (⇑P.subtype ∘ ⇑b)) ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toOuterMeasure_pure_apply : (pure a).toOuterMeasure s = if a ∈ s then 1 else 0

Proof state:
case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
b : α
⊢ s.indicator (⇑(pure a)) b = 0

Tactic:
exact ite_eq_right_iff.2 fun hb =>
  ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Set α
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = if a ∈ s then 1 else 0

Tactic:
split_ifs with ha

Result:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0

Proof state:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

Tactic:
refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)

Result:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
b : α
⊢ s.indicator (⇑(pure a)) b = if b = a then 1 else 0

Proof state:
case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0

Tactic:
refine (tsum_congr fun b => ?_).trans tsum_zero

Result:
case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
b : α
⊢ s.indicator (⇑(pure a)) b = 0

Proof state:
α : Type u_1
a : α
s : Set α
⊢ (pure a).toOuterMeasure s = if a ∈ s then 1 else 0

Tactic:
refine (toOuterMeasure_apply (pure a) s).trans ?_

Result:
α : Type u_1
a : α
s : Set α
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = if a ∈ s then 1 else 0

Proof state:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
b : α
⊢ s.indicator (⇑(pure a)) b = if b = a then 1 else 0

Tactic:
exact ite_eq_left_iff.2 fun hb =>
  symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem exists_measurableSet_of_ne [MeasurableSpace α] [SeparatesPoints α] {x y : α}
    (h : x ≠ y) : ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y

Tactic:
exact separatesPoints_def h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : x ≠ y
⊢ ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setIntegral_condKernel_univ_left {t : Set Ω} (ht : MeasurableSet t)
    (hf : IntegrableOn f (Set.univ ×ˢ t) ρ) :
    ∫ b, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in Set.univ ×ˢ t, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Tactic:
rw [← setIntegral_condKernel MeasurableSet.univ ht hf]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem comap_id (f : Ultrafilter α) (h₀ : Injective (id : α → α) := injective_id)
    (h₁ : range id ∈ f := (by rw [range_id]; exact univ_mem)) :
    f.comap h₀ h₁ = f :=
  coe_injective comap_id

Proof state:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ range id ∈ f

Tactic:
rw [range_id]

Result:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ univ ∈ f

Proof state:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ univ ∈ f

Tactic:
exact univ_mem

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem le_comap_pow_of_le_comap (p : Submodule R M) {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ) :
    p ≤ p.comap (f ^ k)

Proof state:
case succ
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : p ≤ comap (f ^ k) p
⊢ p ≤ comap (f ^ (k + 1)) p

Tactic:
simp [LinearMap.iterate_succ, comap_comp, h.trans (comap_mono ih)]

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
⊢ p ≤ comap (f ^ 0) p

Tactic:
simp [LinearMap.one_eq_id]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
⊢ p ≤ comap (f ^ k) p

Tactic:
induction k with
| zero => simp [LinearMap.one_eq_id]
| succ k ih => simp [LinearMap.iterate_succ, comap_comp, h.trans (comap_mono ih)]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_lt_of_sq_lt_sq (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : |a| < b

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_lt_sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ a - a = 0#w

Tactic:
rw [BitVec.sub_self]

Result:
no goals

Proof state:
w : Nat
a : BitVec w
⊢ a + -a = 0#w

Tactic:
rw [← BitVec.sub_toAdd]

Result:
w : Nat
a : BitVec w
⊢ a - a = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ ~~~a + 1#w + a = 0#w

Tactic:
rw [← BitVec.neg_eq_not_add]

Result:
w : Nat
a : BitVec w
⊢ -a + a = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ -a + a = 0#w

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
a : BitVec w
⊢ a + -a = 0#w
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
    derivWithin f s x = 0

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x) 1 = 0

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h]

Result:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 1 = 0

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 1 = 0

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
unfold derivWithin

Result:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x) 1 = 0
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem coe_sInf (S : Set (Con M)) :
    ⇑(sInf S) = sInf ((⇑) '' S)

Proof state:
case h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Result:
case h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Proof state:
case h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ ⇑(sInf S) = sInf (DFunLike.coe '' S)

Tactic:
ext

Result:
case h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
lemma exists_le_of_tendsto_atTop (h : Tendsto u atTop atTop) (a : α) (b : β) :
    ∃ a' ≥ a, b ≤ u a'

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a' ≥ a, b ≤ u a'

Tactic:
have : Nonempty α := ⟨a⟩

Result:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a' ≥ a, b ≤ u a'

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a' ≥ a, b ≤ u a'

Tactic:
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
  (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)

Result:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a' ≥ a, b ≤ u a'

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a' ≥ a, b ≤ u a'

Tactic:
exact this.exists

Result:
no goals