harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsTrivialBlock.smul_iff {B : Set α} (g : M) :
    IsTrivialBlock (g • B) ↔ IsTrivialBlock B

Proof state:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

Tactic:
intro H

Result:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

Proof state:
case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

Tactic:
intro H

Result:
case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)

Proof state:
case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)

Tactic:
exact IsTrivialBlock.smul H g

Result:
no goals

Proof state:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

Tactic:
convert IsTrivialBlock.smul H g⁻¹

Result:
case h.e'_2
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ B = g⁻¹ • g • B

Proof state:
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) ↔ IsTrivialBlock B

Tactic:
constructor

Result:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

Proof state:
case h.e'_2
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ B = g⁻¹ • g • B

Tactic:
simp only [inv_smul_smul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_mul_limit_aux {a b c : Ordinal} (ba : b + a = a) (l : IsLimit c)
    (IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b) : (a + b) * c = a * c :=
  le_antisymm
    ((mul_le_of_limit l).2 fun c' h => by
      apply (mul_le_mul_left' (le_succ c') _).trans
      rw [IH _ h]
      apply (add_le_add_left _ _).trans
      · rw [← mul_succ]
        exact mul_le_mul_left' (succ_le_of_lt <| l.succ_lt h) _
      · rw [← ba]
        exact le_add_right _ _)
    (mul_le_mul_right' (le_add_right _ _) _)

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ b ≤ b + a

Tactic:
exact le_add_right _ _

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ c' + b ≤ a * c

Tactic:
apply (add_le_add_left _ _).trans

Result:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ c' + ?m.123444 ≤ a * c

a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ Ordinal.{u_4}

a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ b ≤ ?m.123444

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * succ c' ≤ a * c

Tactic:
rw [IH _ h]

Result:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ c' + b ≤ a * c

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ (succ c') ≤ a * c

Tactic:
exact mul_le_mul_left' (succ_le_of_lt <| l.succ_lt h) _

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ b ≤ a

Tactic:
rw [← ba]

Result:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ b ≤ b + a

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ c' + ?m.123444 ≤ a * c

Tactic:
rw [← mul_succ]

Result:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ (succ c') ≤ a * c

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * c' ≤ a * c

Tactic:
apply (mul_le_mul_left' (le_succ c') _).trans

Result:
a b c : Ordinal.{u_4}
ba : b + a = a
l : c.IsLimit
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * succ c' ≤ a * c
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem exists_lt_apply_of_lt_opNNNorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ≥0}
    (hr : r < ‖f‖₊) : ∃ x : E, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Proof state:
case intro
𝕜 : Type u_11
𝕜₂ : Type u_12
E : Type u_13
F : Type u_14
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖f y‖₊
hy' : ‖y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
have hfy : ‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'

Result:
case intro
𝕜 : Type u_11
𝕜₂ : Type u_12
E : Type u_13
F : Type u_14
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖f y‖₊
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
-- Mathlib/Data/Finsupp/Order.lean
theorem single_tsub : single i (a - b) = single i a - single i b

Proof state:
case h.inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
⊢ single i (a - b) = single i a - single i b

Tactic:
ext j

Result:
case h
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
⊢ (single i (a - b)) j = (single i a - single i b) j

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
obtain rfl | h := eq_or_ne i j

Result:
case h.inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
⊢ (single i (a - b)) i = (single i a - single i b) i

case h.inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ (single i (a - b)) j = (single i a - single i b) j

Proof state:
case h.inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
⊢ (single i (a - b)) i = (single i a - single i b) i

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem contains_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} :
    m.val.contains a = m.contains a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ m.val.contains a = m.contains a

Tactic:
simp [Raw.contains, m.2]

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem inducedMap_inducedMap (a : α) : inducedMap β γ (inducedMap α β a) = inducedMap α γ a :=
  eq_of_forall_rat_lt_iff_lt fun q => by
    rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a

Tactic:
rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrable_comap (hs : MeasurableSet s) :
    LocallyIntegrable (fun x : s ↦ f x) (μ.comap Subtype.val) ↔ LocallyIntegrableOn f s μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (fun x => f ↑x) (comap Subtype.val μ) ↔
    ∀ (x : { a // a ∈ s }), IntegrableAtFilter f (Filter.map Subtype.val (𝓝 x)) μ

Tactic:
exact forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (fun x => f ↑x) (comap Subtype.val μ) ↔ LocallyIntegrableOn f s μ

Tactic:
simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]

Result:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (fun x => f ↑x) (comap Subtype.val μ) ↔
    ∀ (x : { a // a ∈ s }), IntegrableAtFilter f (Filter.map Subtype.val (𝓝 x)) μ
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_inv_of_invertible [Invertible A] : A⁻¹⁻¹ = A

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
⊢ A⁻¹⁻¹ = A

Tactic:
simp only [← invOf_eq_nonsing_inv, invOf_invOf]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.stieltjesFunctionAux_eq (a : α) (r : ℚ) :
    IsMeasurableRatCDF.stieltjesFunctionAux f a r = f a r

Proof state:
case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ∀ (x : { q' // ↑r < ↑q' }),
    f a ↑({ toFun := fun t => ⟨↑t, ⋯⟩, invFun := fun t => ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x) = f a ↑x

Tactic:
intro t

Result:
case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' // ↑r < ↑q' }
⊢ f a ↑({ toFun := fun t => ⟨↑t, ⋯⟩, invFun := fun t => ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } t) = f a ↑t

Proof state:
case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' // ↑r < ↑q' }
⊢ f a ↑({ toFun := fun t => ⟨↑t, ⋯⟩, invFun := fun t => ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } t) = f a ↑t

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.coe_mk]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : ↑(Ioi r)
⊢ (fun t => ⟨↑t, ⋯⟩) ((fun t => ⟨↑t, ⋯⟩) t) = t

Tactic:
simp only [Subtype.coe_eta]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ⨅ q, f a ↑q = ⨅ r_1, f a ↑r_1

Tactic:
refine Equiv.iInf_congr ?_ ?_

Result:
case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ { q' // ↑r < ↑q' } ≃ ↑(Ioi r)

case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ∀ (x : { q' // ↑r < ↑q' }), f a ↑(?refine_1 x) = f a ↑x

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' // ↑r < ↑q' }
⊢ (fun t => ⟨↑t, ⋯⟩) ((fun t => ⟨↑t, ⋯⟩) t) = t

Tactic:
simp only [Subtype.coe_eta]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ { q' // ↑r < ↑q' } ≃ ↑(Ioi r)

Tactic:
exact
  { toFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
    invFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
    left_inv := fun t ↦ by simp only [Subtype.coe_eta]
    right_inv := fun t ↦ by simp only [Subtype.coe_eta] }

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ stieltjesFunctionAux f a ↑r = f a r

Tactic:
rw [← hf.iInf_rat_gt_eq a r, IsMeasurableRatCDF.stieltjesFunctionAux]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ⨅ q, f a ↑q = ⨅ r_1, f a ↑r_1
-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
lemma continuous_iff_of_isColimit {X : Type w} [TopologicalSpace X] (f : c.pt → X) :
    Continuous f ↔ ∀ (j : J), Continuous (f ∘ c.ι.app j)

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Type w
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)))

Tactic:
simp only [continuous_def, isOpen_iff_of_isColimit _ hc]

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Type w
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ (∀ (s : Set X), IsOpen s → ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' (f ⁻¹' s))) ↔
    ∀ (j : J) (s : Set X), IsOpen s → IsOpen (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' s)

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Type w
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ (∀ (s : Set X), IsOpen s → ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' (f ⁻¹' s))) ↔
    ∀ (j : J) (s : Set X), IsOpen s → IsOpen (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' s)

Tactic:
tauto

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_singleton (ω : Ω) (t : Set Ω) [Decidable (ω ∈ t)] :
    uniformOn {ω} t = if ω ∈ t then 1 else 0

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0

Tactic:
split_ifs

Result:
case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ Measure.count ({ω} ∩ t) = 1

case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∉ t
⊢ Measure.count ({ω} ∩ t) = 0

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ (uniformOn {ω}) t = if ω ∈ t then 1 else 0

Tactic:
rw [uniformOn, cond_apply (measurableSet_singleton ω), Measure.count_singleton, inv_one,
  one_mul]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0

Proof state:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∉ t
⊢ Measure.count ({ω} ∩ t) = 0

Tactic:
simpa

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ {ω} ∩ t = {ω}

Tactic:
simpa

Result:
no goals

Proof state:
case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ Measure.count ({ω} ∩ t) = 1

Tactic:
rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblX_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : W'.dblX P = W'.dblU P ^ 2

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblX P = W'.dblU P ^ 2

Tactic:
rw [dblX, Y_eq_negY_of_Y_eq hQz hx hy hy']

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (W'.negY P - W'.negY P) - W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
      2 * P x * (W'.negY P - W'.negY P) ^ 2 =
    W'.dblU P ^ 2

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (W'.negY P - W'.negY P) - W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
      2 * P x * (W'.negY P - W'.negY P) ^ 2 =
    W'.dblU P ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem drop_take_succ_eq_cons_getElem (L : List α) (i : Nat) (h : i < L.length) :
    (L.take (i + 1)).drop i = [L[i]]

Proof state:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
i : ℕ
h : i + 1 < (head :: tail).length
⊢ drop (i + 1) (take (i + 1 + 1) (head :: tail)) = [(head :: tail)[i + 1]]

Tactic:
simpa using ih _ (by simpa using h)

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
h : 0 < (head :: tail).length
⊢ drop 0 (take (0 + 1) (head :: tail)) = [(head :: tail)[0]]

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
i : ℕ
h : i < [].length
⊢ drop i (take (i + 1) []) = [[][i]]

Tactic:
exact (Nat.not_succ_le_zero i h).elim

Result:
no goals

Proof state:
α : Type u_1
L : List α
i : ℕ
h : i < L.length
⊢ drop i (take (i + 1) L) = [L[i]]

Tactic:
induction' L with head tail ih generalizing i

Result:
case nil
α : Type u_1
i : ℕ
h : i < [].length
⊢ drop i (take (i + 1) []) = [[][i]]

case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
i : ℕ
h : i < (head :: tail).length
⊢ drop i (take (i + 1) (head :: tail)) = [(head :: tail)[i]]

Proof state:
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
i : ℕ
h : i + 1 < (head :: tail).length
⊢ i < tail.length

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
i : ℕ
h : i < (head :: tail).length
⊢ drop i (take (i + 1) (head :: tail)) = [(head :: tail)[i]]

Tactic:
rcases i with _ | i

Result:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
h : 0 < (head :: tail).length
⊢ drop 0 (take (0 + 1) (head :: tail)) = [(head :: tail)[0]]

case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (i : ℕ) (h : i < tail.length), drop i (take (i + 1) tail) = [tail[i]]
i : ℕ
h : i + 1 < (head :: tail).length
⊢ drop (i + 1) (take (i + 1 + 1) (head :: tail)) = [(head :: tail)[i + 1]]
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_eq_cons_Ico (h : a ≤ b) : Icc a b = (Ico a b).cons b right_not_mem_Ico

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ico_insert_right h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
rw [cons_eq_insert, Ico_insert_right h]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
theorem isSeparator [Nonempty D] : IsSeparator (generator F)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator F)

Tactic:
apply isSeparator_sigma_of_isSeparator _ Classical.ofNonempty

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)

Tactic:
apply isSeparator_sigma_of_isSeparator _ 0

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)

Tactic:
exact isSeparator_projectiveSeparator

Result:
no goals