harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[simp] lemma natAbs_even : Even n.natAbs ↔ Even n

Proof state:
n : ℤ
⊢ Even n.natAbs ↔ Even n

Tactic:
simp [even_iff_two_dvd, dvd_natAbs, natCast_dvd.symm]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIcc : Fintype.card (Set.Icc a b) = b + 1 - a

Proof state:
a b : ℕ
⊢ Fintype.card ↑(Set.Icc a b) = b + 1 - a

Tactic:
rw [Fintype.card_ofFinset, card_Icc]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem nilradical_eq_sInf (R : Type*) [CommSemiring R] :
    nilradical R = sInf { J : Ideal R | J.IsPrime } :=
  (Ideal.radical_eq_sInf ⊥).trans <| by simp_rw [and_iff_right bot_le]

Proof state:
R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
simp_rw [and_iff_right bot_le]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma Φ_ne_zero [Nontrivial R] (n : ℤ) : W.Φ n ≠ 0

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : n = 0
⊢ W.Φ n ≠ 0

Tactic:
simpa only [hn, Φ_zero] using one_ne_zero

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
⊢ W.Φ n ≠ 0

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : n = 0
⊢ W.Φ n ≠ 0

case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ W.Φ n ≠ 0

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ W.Φ n ≠ 0

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_Φ_pos hn

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitOpIsoOpColimit_hom_comp_ι (F : J ⥤ C) [HasColimit F] (j : J) :
    (limitOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.op (op j)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ (limitOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.op (op j)

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem Nat.norm_cast_le : ∀ n : ℕ, ‖(n : α)‖ ≤ n * ‖(1 : α)‖
  | 0 => by simp
  | n + 1 => by
    rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
    exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖

Tactic:
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑(n + 1)‖ ≤ ↑(n + 1) * ‖1‖

Tactic:
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]

Result:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
⊢ ‖↑0‖ ≤ ↑0 * ‖1‖

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_one_div_int_pow {p : ℕ} :
    (Summable fun n : ℤ ↦ 1 / (n : ℝ) ^ p) ↔ 1 < p

Proof state:
p : ℕ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p

Tactic:
refine ⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
  fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
    (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩

Result:
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / ↑(-↑n) ^ p

Proof state:
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / ↑(-↑n) ^ p

Tactic:
rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem snd_expSeries_of_smul_comm
    (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) (n : ℕ) :
    snd (expSeries 𝕜 (tsze R M) (n + 1) fun _ => x) = (expSeries 𝕜 R n fun _ => x.fst) • x.snd

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ ((expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 => x).snd = ((expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd

Tactic:
simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
  ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
  Nat.cast_mul, mul_inv_rev,
  inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem isUniformEmbedding_iff [PseudoMetricSpace β] {f : α → β} :
    IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I)

Proof state:
x : ℂ
⊢ cexp x = cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)

Tactic:
rw [← exp_add_mul_I, re_add_im]

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_sum_single (s : Finset ι) (n : ℕ) :
    Finsupp.toMultiset (∑ i ∈ s, single i n) = n • s.val

Proof state:
ι : Type u_3
s : Finset ι
n : ℕ
⊢ toMultiset (∑ i ∈ s, single i n) = n • s.val

Tactic:
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_prod (n : ℕ) :
    lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)

Proof state:
case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
⊢ lowerCentralSeries (G₁ × G₂) (n + 1) = (lowerCentralSeries G₁ (n + 1)).prod (lowerCentralSeries G₂ (n + 1))

Tactic:
calc
  lowerCentralSeries (G₁ × G₂) n.succ = ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ := rfl
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ := by rw [ih]
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), (⊤ : Subgroup G₁).prod ⊤⁆ := by
    simp
  _ = ⁅lowerCentralSeries G₁ n, (⊤ : Subgroup G₁)⁆.prod ⁅lowerCentralSeries G₂ n, ⊤⁆ :=
    (commutator_prod_prod _ _ _ _)
  _ = (lowerCentralSeries G₁ n.succ).prod (lowerCentralSeries G₂ n.succ) := rfl

Result:
no goals

Proof state:
case zero
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
⊢ lowerCentralSeries (G₁ × G₂) 0 = (lowerCentralSeries G₁ 0).prod (lowerCentralSeries G₂ 0)

Tactic:
simp

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
⊢ ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ =
    ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤.prod ⊤⁆

Tactic:
simp

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
⊢ ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆

Tactic:
rw [ih]

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
⊢ lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)

Tactic:
induction' n with n ih

Result:
case zero
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
⊢ lowerCentralSeries (G₁ × G₂) 0 = (lowerCentralSeries G₁ 0).prod (lowerCentralSeries G₂ 0)

case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
⊢ lowerCentralSeries (G₁ × G₂) (n + 1) = (lowerCentralSeries G₁ (n + 1)).prod (lowerCentralSeries G₂ (n + 1))
-- Mathlib/Topology/Order.lean
theorem le_nhdsAdjoint_iff {α : Type*} (a : α) (f : Filter α) (t : TopologicalSpace α) :
    t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, IsOpen[t] {b}

Proof state:
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}

Tactic:
simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_congr_nnnorm_ae {f g : α → F} (hfg : ∀ᵐ x ∂μ, ‖f x‖₊ = ‖g x‖₊) :
    eLpNorm' f q μ = eLpNorm' g q μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
x : α
hx : ‖f x‖₊ = ‖g x‖₊
⊢ (fun x => ‖f x‖ₑ ^ q) x = (fun x => ‖g x‖ₑ ^ q) x

Tactic:
simp [enorm, hx]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
this : (fun x => ‖f x‖ₑ ^ q) =ᶠ[ae μ] fun x => ‖g x‖ₑ ^ q
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, lintegral_congr_ae this]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiff_iff :
    ContMDiff I I' n f ↔
      Continuous f ∧
        ∀ (x : M) (y : M'),
          ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
            ((extChartAt I x).target ∩
              (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

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'
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiff I I' n f ↔
    Continuous f ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

Tactic:
simp [← contMDiffOn_univ, contMDiffOn_iff, continuous_iff_continuousOn_univ]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem cons_equiv_eq_equiv_cons (α : Type*) (n : ℕ) (a : α) (s : Sym α n) :
    (a::symEquivSym' s) = symEquivSym' (a ::ₛ s)

Proof state:
α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ (a :: symEquivSym' s) = symEquivSym' (a ::ₛ s)

Tactic:
rcases s with ⟨⟨l⟩, _⟩

Result:
case mk.mk
α : Type u_3
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = n
⊢ (a :: symEquivSym' ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩) =
    symEquivSym' (a ::ₛ ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩)

Proof state:
case mk.mk
α : Type u_3
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = n
⊢ (a :: symEquivSym' ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩) =
    symEquivSym' (a ::ₛ ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    [Std.Irrefl (· < · : β → β → Prop)]
    [Std.Asymm (· < · : β → β → Prop)]
    [Std.Antisymm (¬ · < · : β → β → Prop)]
    {l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
    map f l₁ ≤ map f l₂

Proof state:
α : Type u_1
β : Type u_2
n : Nat
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : Vector α n
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ ≤ l₂
⊢ map f l₁ ≤ map f l₂

Tactic:
simpa using Array.map_le w h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_indicator (hs : MeasurableSet s) :
    ∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, 0 ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
simp

Result:
no goals

Proof state:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [integral_undef hfi, integral_undef]

Result:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ¬Integrable (s.indicator f) μ

Proof state:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
swap

Result:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Proof state:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ¬Integrable (s.indicator f) μ

Tactic:
rwa [integrable_indicator_iff hs]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by_cases hfi : IntegrableOn f s μ

Result:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem exists_ne_one_of_nontrivial (H : Subgroup G) [Nontrivial H] :
    ∃ x ∈ H, x ≠ 1

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Nontrivial ↥H
⊢ ∃ x ∈ H, x ≠ 1

Tactic:
rwa [← Subgroup.nontrivial_iff_exists_ne_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem indicator_le_thickenedIndicator {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) :
    (E.indicator fun _ => (1 : ℝ≥0)) ≤ thickenedIndicator δ_pos E

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a

Tactic:
by_cases h : a ∈ E

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a

Tactic:
simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a

Tactic:
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ (E.indicator fun x => 1) ≤ ⇑(thickenedIndicator δ_pos E)

Tactic:
intro a

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ E.indicator (fun x => 1) a ≤ (thickenedIndicator δ_pos E) a
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type*) [CommRing R] (p k : ℕ)
    [hn : Fact (Nat.Prime p)] :
    cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1

Tactic:
rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/Shift.lean
@[simp]
lemma shift_zero [P.IsClosedUnderIsomorphisms] : P.shift (0 : A) = P

Proof state:
case h.a
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ P.shift 0 X ↔ P X

Tactic:
exact P.prop_iff_of_iso ((shiftFunctorZero C A).app X)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.shift 0 = P

Tactic:
ext X

Result:
case h.a
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ P.shift 0 X ↔ P X
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_ordinalToPGame (o : Ordinal) : o.toPGame.birthday = o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ (lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding

Tactic:
congr with x

Result:
case h.e_f.h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
x : o.toType
⊢ (↑(o.enumIsoToType.symm x)).toPGame.birthday = (typein fun x1 x2 => x1 < x2).toRelEmbedding x

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ ((lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) ⊔ lsub fun i => i.elim.birthday) = o

Tactic:
simp only [lsub_empty, max_zero_right]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ (lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) = o

Proof state:
o : Ordinal.{u_1}
⊢ o.toPGame.birthday = o

Tactic:
induction' o using Ordinal.induction with o IH

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ o.toPGame.birthday = o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ o.toPGame.birthday = o

Tactic:
rw [toPGame, PGame.birthday]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ ((lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) ⊔ lsub fun i => i.elim.birthday) = o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ (lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) = o

Tactic:
conv_rhs => rw [← lsub_typein o]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
⊢ (lsub fun i => (↑(o.enumIsoToType.symm i)).toPGame.birthday) = lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding

Proof state:
case h.e_f.h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.birthday = k
x : o.toType
⊢ (↑(o.enumIsoToType.symm x)).toPGame.birthday = (typein fun x1 x2 => x1 < x2).toRelEmbedding x

Tactic:
exact IH _ (typein_lt_self x)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem coe_det_isEmpty [IsEmpty n] : (det : Matrix n n R → R) = Function.const _ 1

Proof state:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
⊢ det = const (Matrix n n R) 1

Tactic:
ext

Result:
case h
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
x✝ : Matrix n n R
⊢ x✝.det = const (Matrix n n R) 1 x✝

Proof state:
case h
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
x✝ : Matrix n n R
⊢ x✝.det = const (Matrix n n R) 1 x✝

Tactic:
exact det_isEmpty

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem nonempty_mk_iff {x : PSet} : (mk x).Nonempty ↔ x.Nonempty

Proof state:
case intro.h
x a✝ : PSet.{u_1}
h : ⟦a✝⟧ ∈ (mk x).toSet
⊢ x.Nonempty

Tactic:
exact ⟨_, h⟩

Result:
no goals

Proof state:
x : PSet.{u_1}
⊢ (mk x).Nonempty → x.Nonempty

Tactic:
rintro ⟨a, h⟩

Result:
case intro
x : PSet.{u_1}
a : ZFSet.{u_1}
h : a ∈ (mk x).toSet
⊢ x.Nonempty

Proof state:
case intro
x : PSet.{u_1}
a : ZFSet.{u_1}
h : a ∈ (mk x).toSet
⊢ x.Nonempty

Tactic:
induction a using Quotient.inductionOn

Result:
case intro.h
x a✝ : PSet.{u_1}
h : ⟦a✝⟧ ∈ (mk x).toSet
⊢ x.Nonempty

Proof state:
x : PSet.{u_1}
⊢ (mk x).Nonempty ↔ x.Nonempty

Tactic:
refine ⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩

Result:
x : PSet.{u_1}
⊢ (mk x).Nonempty → x.Nonempty
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ico_mul_Ioc_subset' [LocallyFiniteOrder α] (a b c d : α) :
    Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Ico_mul_Ioc_subset' _ _ _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b * Ioc c d) ⊆ ↑(Ioo (a * c) (b * d))

Tactic:
simpa using Set.Ico_mul_Ioc_subset' _ _ _ _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
theorem limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π {C : Type*} [Category C] {D : Type*}
    [Category D] {E : Type*} [Category E] {J : Type*} [Category J]
    [HasLimitsOfShape J D] (F : D ⥤ E) [PreservesLimitsOfShape J F] (G : J ⥤ C ⥤ D) (j : J) :
    (limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
      limit.π (G ⋙ (whiskeringRight _ _ _).obj F) j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{u_7, u_3} E
J : Type u_4
inst✝² : Category.{u_8, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
    limit.π (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals