harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma singularPart_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ]
    [IsFiniteKernel η] (a : α) :
    singularPart κ η a = 0 ↔ singularPart κ η a (mutuallySingularSetSlice κ η a) = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
  singularPart_compl_mutuallySingularSetSlice, add_zero]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
rw [← Measure.measure_univ_eq_zero]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eq_some_getValueCast [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l) : getValueCast? a l = some (getValueCast a l h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ getValueCast? a l = some (getValueCast a l h)

Tactic:
simp [getValueCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem ofIsCompl_left_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
    ofIsCompl h φ ψ (u : E) = φ u

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
u : ↥p
⊢ (ofIsCompl h φ ψ) ↑u = φ u

Tactic:
simp [ofIsCompl]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iInter_Iic_eq_empty_iff : ⋂ i, Iic (f i) = ∅ ↔ ¬ BddBelow (range f)

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
⊢ ⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f)

Tactic:
simp [not_bddBelow_iff, Set.eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma Function.Injective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
    [SMulCommClass M N β] {f : α → β} (hf : Injective f) (h₁ : ∀ (c : M) x, f (c • x) = c • f x)
    (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N α where
  smul_comm c₁ c₂ x := hf <| by simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

Proof state:
M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)

Tactic:
simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_midpoint_left (p₁ p₂ p₃ : P) : ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
by_cases h : p₁ = p₂

Result:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_left

Result:
no goals

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem iteratedFDeriv_tsum_apply (hf : ∀ i, ContDiff 𝕜 N (f i))
    (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
    (h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ}
    (hk : (k : ℕ∞) ≤ N) (x : E) :
    iteratedFDeriv 𝕜 k (fun y => ∑' n, f n y) x = ∑' n, iteratedFDeriv 𝕜 k (f n) x

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk : ↑k ≤ N
x : E
⊢ iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Tactic:
rw [iteratedFDeriv_tsum hf hv h'f hk]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem zero_eq_mul_self : 0 = a * a ↔ a = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ 0 = a * a ↔ a = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_neg (x : ℝ) : arccos (-x) = π - arccos x

Proof state:
x : ℝ
⊢ arccos (-x) = π - arccos x

Tactic:
rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem Metric.finite_isBounded_inter_isClosed [ProperSpace α] {K s : Set α} [DiscreteTopology s]
    (hK : IsBounded K) (hs : IsClosed s) : Set.Finite (K ∩ s)

Proof state:
case refine_1
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
K s : Set α
inst✝ : DiscreteTopology ↑s
hK : Bornology.IsBounded K
hs : IsClosed s
⊢ IsCompact (closure K ∩ s)

Tactic:
exact hK.isCompact_closure.inter_right hs

Result:
no goals

Proof state:
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
K s : Set α
inst✝ : DiscreteTopology ↑s
hK : Bornology.IsBounded K
hs : IsClosed s
⊢ (K ∩ s).Finite

Tactic:
refine Set.Finite.subset (IsCompact.finite ?_ ?_) (Set.inter_subset_inter_left s subset_closure)

Result:
case refine_1
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
K s : Set α
inst✝ : DiscreteTopology ↑s
hK : Bornology.IsBounded K
hs : IsClosed s
⊢ IsCompact (closure K ∩ s)

case refine_2
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
K s : Set α
inst✝ : DiscreteTopology ↑s
hK : Bornology.IsBounded K
hs : IsClosed s
⊢ DiscreteTopology ↑(closure K ∩ s)

Proof state:
case refine_2
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
K s : Set α
inst✝ : DiscreteTopology ↑s
hK : Bornology.IsBounded K
hs : IsClosed s
⊢ DiscreteTopology ↑(closure K ∩ s)

Tactic:
exact DiscreteTopology.of_subset inferInstance Set.inter_subset_right

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_roots_sub_C' {p : R[X]} {a x : R} : x ∈ (p - C a).roots ↔ p ≠ C a ∧ p.eval x = a

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ x ∈ (p - C a).roots ↔ p ≠ C a ∧ eval x p = a

Tactic:
rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioo_pred_left_of_not_isMin (ha : ¬IsMin a) : Ioo (pred a) b = Ico a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioo (pred a) b = Ico a b

Tactic:
rw [← Ioi_inter_Iio, Ioi_pred_of_not_isMin ha, Ici_inter_Iio]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem compl_mem_ae_iff {s : Set α} : sᶜ ∈ ae μ ↔ μ s = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : Set α
⊢ sᶜ ∈ ae μ ↔ μ s = 0

Tactic:
simp only [mem_ae_iff, compl_compl]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem Monotone.ne_of_lt_of_lt_nat {f : ℕ → α} (hf : Monotone f) (n : ℕ) {x : α} (h1 : f n < x)
    (h2 : x < f (n + 1)) (a : ℕ) : f a ≠ x

Proof state:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
exact (hf.reflect_lt h1).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h2)

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl

Result:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDerivWithin_comp_add_left (n : ℕ) (a : E) (x : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s x =
      iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a x : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Tactic:
simp [iteratedFDerivWithin_comp_add_left']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).isEmpty = m.isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).isEmpty = m.isEmpty

Tactic:
simp_to_raw using Raw₀.isEmpty_modify

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_inv_snd (X Y Z : C) :
    (α_ X Y Z).inv ≫ prod.snd = prod.snd ≫ prod.snd

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ prod.snd = prod.snd ≫ prod.snd

Tactic:
simp [associator_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem abs_sub_map_le_div [Group α] [LinearOrderedAddCommGroup β] [GroupSeminormClass F α β]
    (f : F) (x y : α) : |f x - f y| ≤ f (x / y)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']

Result:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (x / y) ∧ f y ≤ f x + f (x / y)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (x / y) ∧ f y ≤ f x + f (x / y)

Tactic:
exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem subset_positive_null_set (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hw : MeasurableSet w) (hsu : 0 ≤[u] s) (hw₁ : s w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w) :
    s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ↑s v = 0

Tactic:
have : s v + s (w \ v) = 0 := by
  rw [← hw₁, ← of_union Set.disjoint_sdiff_right hv (hw.diff hv), Set.union_diff_self,
    Set.union_eq_self_of_subset_left hwt]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
⊢ ↑s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ↑s v + ↑s (w \ v) = 0

Tactic:
rw [← hw₁, ← of_union Set.disjoint_sdiff_right hv (hw.diff hv), Set.union_diff_self,
  Set.union_eq_self_of_subset_left hwt]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
h₁ : 0 ≤ ↑s v
h₂ : 0 ≤ ↑s (w \ v)
⊢ ↑s v = 0

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
⊢ ↑s v = 0

Tactic:
have h₁ := nonneg_of_zero_le_restrict _ (restrict_le_restrict_subset _ _ hu hsu (hwt.trans hw₂))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
h₁ : 0 ≤ ↑s v
⊢ ↑s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
h₁ : 0 ≤ ↑s v
⊢ ↑s v = 0

Tactic:
have h₂ : 0 ≤ s (w \ v) :=
  nonneg_of_zero_le_restrict _
    (restrict_le_restrict_subset _ _ hu hsu (diff_subset.trans hw₂))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s v + ↑s (w \ v) = 0
h₁ : 0 ≤ ↑s v
h₂ : 0 ≤ ↑s (w \ v)
⊢ ↑s v = 0
-- Mathlib/GroupTheory/Perm/Support.lean
theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
    #{x | σ x = x} < Fintype.card α - 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #(filter (fun x => σ x = x) univ) < Fintype.card α - 1

Tactic:
rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < #(filter (fun x => ¬σ x = x) univ)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < #(filter (fun x => ¬σ x = x) univ)

Tactic:
exact one_lt_card_support_of_ne_one h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem roots_map {f : K[X]} (hf : f.Splits <| RingHom.id K) : (f.map i).roots = f.roots.map i :=
  (roots_map_of_injective_of_card_eq_natDegree i.injective <| by
      convert (natDegree_eq_card_roots hf).symm
      rw [map_id]).symm

Proof state:
case h.e'_2.h.e'_2.h.e'_4
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits (RingHom.id K) f
⊢ f = map (RingHom.id K) f

Tactic:
rw [map_id]

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits (RingHom.id K) f
⊢ f.roots.card = f.natDegree

Tactic:
convert (natDegree_eq_card_roots hf).symm

Result:
case h.e'_2.h.e'_2.h.e'_4
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits (RingHom.id K) f
⊢ f = map (RingHom.id K) f
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_add_single (a : α) (f : α →₀ M) : f.erase a + single a (f a) = f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ erase a f + single a (f a) = f

Tactic:
rw [← update_eq_erase_add_single, update_self]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem zero_nmul (a) : 0 ⨳ a = 0

Proof state:
a : Ordinal.{u_1}
⊢ 0 ⨳ a = 0

Tactic:
rw [nmul_comm, nmul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_append (p : α → Bool) (l₁ l₂ : Array α) :
    (l₁ ++ l₂).findIdx p =
      if l₁.findIdx p < l₁.size then l₁.findIdx p else l₂.findIdx p + l₁.size

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ findIdx p ({ toList := l₁ } ++ { toList := l₂ }) =
    if findIdx p { toList := l₁ } < { toList := l₁ }.size then findIdx p { toList := l₁ }
    else findIdx p { toList := l₂ } + { toList := l₁ }.size

Tactic:
simp [List.findIdx_append]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
⊢ findIdx p (l₁ ++ l₂) = if findIdx p l₁ < l₁.size then findIdx p l₁ else findIdx p l₂ + l₁.size

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ findIdx p ({ toList := l₁ } ++ l₂) =
    if findIdx p { toList := l₁ } < { toList := l₁ }.size then findIdx p { toList := l₁ }
    else findIdx p l₂ + { toList := l₁ }.size

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ findIdx p ({ toList := l₁ } ++ l₂) =
    if findIdx p { toList := l₁ } < { toList := l₁ }.size then findIdx p { toList := l₁ }
    else findIdx p l₂ + { toList := l₁ }.size

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ findIdx p ({ toList := l₁ } ++ { toList := l₂ }) =
    if findIdx p { toList := l₁ } < { toList := l₁ }.size then findIdx p { toList := l₁ }
    else findIdx p { toList := l₂ } + { toList := l₁ }.size
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
protected lemma map_neg (P : Fin 3 → R) : (W'.map f).toJacobian.neg (f ∘ P) = f ∘ W'.neg P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ ![(⇑f ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ ![(⇑f ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]
-- Mathlib/Algebra/Algebra/Tower.lean
theorem restrictScalars_span (hsur : Function.Surjective (algebraMap R A)) (X : Set M) :
    restrictScalars R (span A X) = span R X

Proof state:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
⊢ restrictScalars R (span A X) = span R X

Tactic:
refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm

Result:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m : M
hm : m ∈ restrictScalars R (span A X)
⊢ m ∈ span R X

Proof state:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
a : A
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
⊢ a • m ∈ span R X

Tactic:
obtain ⟨r, rfl⟩ := hsur a

Result:
case intro
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ (algebraMap R A) r • m ∈ span R X

Proof state:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m : M
hm : m ∈ restrictScalars R (span A X)
⊢ m ∈ span R X

Tactic:
refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm

Result:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
a : A
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
⊢ a • m ∈ span R X

Proof state:
case intro
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ (algebraMap R A) r • m ∈ span R X

Tactic:
simpa [algebraMap_smul] using smul_mem _ r hm

Result:
no goals