harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma setLIntegral_indicator₀ (f : α → ℝ≥0∞) {s t : Set α}
    (hs : NullMeasurableSet s (μ.restrict t)) :
    ∫⁻ a in t, s.indicator f a ∂μ = ∫⁻ a in s ∩ t, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]

Result:
no goals
-- Mathlib/Data/List/SplitBy.lean
theorem ne_nil_of_mem_splitBy (r : α → α → Bool) {l : List α} (h : m ∈ l.splitBy r) : m ≠ []

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
⊢ m ≠ []

Tactic:
rintro rfl

Result:
α : Type u_1
r : α → α → Bool
l : List α
h : [] ∈ splitBy r l
⊢ False

Proof state:
α : Type u_1
r : α → α → Bool
l : List α
h : [] ∈ splitBy r l
⊢ False

Tactic:
exact nil_not_mem_splitBy r l h

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
lemma injOn_iInf_maxGenEigenspace :
    InjOn (fun χ : ι → R ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
      {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}

Tactic:
simpa [hχ₁₂] using disjoint_iInf_maxGenEigenspace f hχ₂

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₂ : χ₂ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
⊢ InjOn (fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)) {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}

Tactic:
rintro χ₁ _ χ₂
  hχ₂ (hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i))

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₂ : χ₂ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
⊢ χ₁ = χ₂
-- Mathlib/Logic/Nontrivial/Defs.lean
theorem subsingleton_iff : Subsingleton α ↔ ∀ x y : α, x = y :=
  ⟨by
    intro h
    exact Subsingleton.elim, fun h ↦ ⟨h⟩⟩

Proof state:
α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y

Tactic:
exact Subsingleton.elim

Result:
no goals

Proof state:
α : Type u_1
⊢ Subsingleton α → ∀ (x y : α), x = y

Tactic:
intro h

Result:
α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

Tactic:
simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean
theorem FiniteField.trace_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
    trace (M ^ Fintype.card K) = trace M ^ Fintype.card K

Proof state:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
simp [Matrix.trace]

Result:
no goals

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
cases isEmpty_or_nonempty n

Result:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Proof state:
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
  FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive] lemma mul_pow_mul (a b : M) (n : ℕ) :
    (a * b) ^ n * a = a * (b * a) ^ n

Proof state:
case zero
M : Type u_2
inst✝ : Monoid M
a b : M
⊢ (a * b) ^ 0 * a = a * (b * a) ^ 0

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
a b : M
n : ℕ
⊢ (a * b) ^ n * a = a * (b * a) ^ n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [pow_succ', ← ih, Nat.mul_add, mul_assoc]

Result:
no goals

Proof state:
case succ
M : Type u_2
inst✝ : Monoid M
a b : M
n : ℕ
ih : (a * b) ^ n * a = a * (b * a) ^ n
⊢ (a * b) ^ (n + 1) * a = a * (b * a) ^ (n + 1)

Tactic:
simp [pow_succ', ← ih, Nat.mul_add, mul_assoc]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_insert_le (a : α) (s : Set α) : (insert a s).ncard ≤ s.ncard + 1

Proof state:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
to_encard_tac

Result:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1

Proof state:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1

Tactic:
apply encard_insert_le

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Set α
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
obtain hs | hs := s.finite_or_infinite

Result:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).ncard ≤ s.ncard + 1

case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1

Proof state:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
rw [(hs.mono (subset_insert a s)).ncard]

Result:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Proof state:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1

Tactic:
rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]

Result:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1
-- Mathlib/Data/ENat/Lattice.lean
lemma sub_iSup [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
case inl.intro
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, (iInf_eq_bot _).2, bot_eq_zero]

Result:
case inl.intro
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ ∀ b > ⊥, ∃ i, a - f i < b

Proof state:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
  ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
  add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
  iSup_le fun i ↦ ?_

Result:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ i, a - f i

Proof state:
case inl.intro
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ ∀ b > ⊥, ∃ i, a - f i < b

Tactic:
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩

Result:
no goals

Proof state:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
simp_rw [not_exists, not_lt] at h

Result:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
x : ℕ∞
hx : x > ⊥
⊢ a - f i < x

Tactic:
simpa [hi.le, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Result:
case inl.intro
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ i, a - f i

Tactic:
rw [← ENat.sub_sub_cancel ha (h _)]

Result:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i
-- Mathlib/Topology/PartialHomeomorph.lean
theorem isOpenEmbedding_restrict : IsOpenEmbedding (e.source.restrict e)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
V : Set ↑e.source
hV : IsOpen V
⊢ IsOpen (↑e '' (Subtype.val '' V))

Tactic:
exact e.isOpen_image_of_subset_source (e.open_source.isOpenMap_subtype_val V hV)
  fun _ ⟨x, _, h⟩ ↦ h ▸ x.2

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsOpenEmbedding (e.source.restrict ↑e)

Tactic:
refine .of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous
  continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
V : Set ↑e.source
hV : IsOpen V
⊢ IsOpen (e.source.restrict ↑e '' V)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
V : Set ↑e.source
hV : IsOpen V
⊢ IsOpen (e.source.restrict ↑e '' V)

Tactic:
rw [Set.restrict_eq, Set.image_comp]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
V : Set ↑e.source
hV : IsOpen V
⊢ IsOpen (↑e '' (Subtype.val '' V))
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Topology.IsInducing.isLindelof_preimage {f : X → Y} (hf : IsInducing f)
    (hf' : IsClosed (range f)) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)

Tactic:
rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (f ⁻¹' K)

Tactic:
replace hK := hK.inter_right hf'

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem zero_eq_nndist {x y : γ} : 0 = nndist x y ↔ x = y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 = nndist x y ↔ x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, zero_eq_dist]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_eq_fderiv (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableAt 𝕜 f x) :
    fderivWithin 𝕜 f s x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ fderivWithin 𝕜 f s x = fderiv 𝕜 f x

Tactic:
rw [← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ fderivWithin 𝕜 f s x = fderivWithin 𝕜 f univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ fderivWithin 𝕜 f s x = fderivWithin 𝕜 f univ x

Tactic:
exact fderivWithin_subset (subset_univ _) hs h.differentiableWithinAt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
  any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega))

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
⊢ (n + 1).any f = ((n.any fun i h => f i ⋯) || f n ⋯)

Tactic:
simp [any]

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
i : Nat
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem smul_im (a : ℤ) (b : ℤ√d) : (↑a * b).im = a * b.im

Proof state:
d a : ℤ
b : ℤ√d
⊢ (↑a * b).im = a * b.im

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma toNNReal_mul_add_neg_mul_add_mul_neg_eq (f g : C(X, ℝ)₀) :
    ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
    ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)

Proof state:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ ↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
    ↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)

Tactic:
simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
  using (f : C(X, ℝ)).toNNReal_mul_add_neg_mul_add_mul_neg_eq g

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Tactic:
apply toContinuousMap_injective

Result:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ ↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
    ↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)
-- Mathlib/Data/Nat/Factorial/Cast.lean
theorem cast_descFactorial_two : (a.descFactorial 2 : S) = a * (a - 1)

Proof state:
S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ ↑(a.descFactorial 2) = ↑a * (↑a - 1)

Tactic:
rw [cast_descFactorial]

Result:
S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (ascPochhammer S 2) = ↑a * (↑a - 1)

Proof state:
case succ
S : Type u_1
inst✝ : Ring S
n✝ : ℕ
⊢ Polynomial.eval (↑(n✝ + 1 - (2 - 1))) (ascPochhammer S 2) = ↑(n✝ + 1) * (↑(n✝ + 1) - 1)

Tactic:
rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel_right, ascPochhammer_succ_right,
  ascPochhammer_one, Polynomial.X_mul, Polynomial.eval_mul_X, Polynomial.eval_add,
  Polynomial.eval_X, cast_one, Polynomial.eval_one]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (ascPochhammer S 2) = ↑a * (↑a - 1)

Tactic:
cases a

Result:
case zero
S : Type u_1
inst✝ : Ring S
⊢ Polynomial.eval (↑(0 - (2 - 1))) (ascPochhammer S 2) = ↑0 * (↑0 - 1)

case succ
S : Type u_1
inst✝ : Ring S
n✝ : ℕ
⊢ Polynomial.eval (↑(n✝ + 1 - (2 - 1))) (ascPochhammer S 2) = ↑(n✝ + 1) * (↑(n✝ + 1) - 1)

Proof state:
case zero
S : Type u_1
inst✝ : Ring S
⊢ Polynomial.eval (↑(0 - (2 - 1))) (ascPochhammer S 2) = ↑0 * (↑0 - 1)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem hasseDeriv_comp (k l : ℕ) (f : LaurentSeries V) :
    hasseDeriv R k (hasseDeriv R l f) = (k + l).choose k • hasseDeriv R (k + l) f

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
⊢ (hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k • (hasseDeriv R (k + l)) f

Tactic:
ext n

Result:
case coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Proof state:
case coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Tactic:
simp [hasseDeriv_comp_coeff k l f n]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem measurableSet_plusPart (hm : MeasurableSet A) :
    MeasurableSet (plusPart A)

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (A ∩ ⋂ w, {x | 0 < x.1 w})

Tactic:
refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)

Result:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : { w // w.IsReal }
⊢ MeasurableSet {x | 0 < x.1 x✝}

Proof state:
case h.e'_3.h
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : mixedSpace K
⊢ x✝ ∈ plusPart A ↔ x✝ ∈ A ∩ ⋂ w, {x | 0 < x.1 w}

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ plusPart A = A ∩ ⋂ w, {x | 0 < x.1 w}

Tactic:
ext

Result:
case h.e'_3.h
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : mixedSpace K
⊢ x✝ ∈ plusPart A ↔ x✝ ∈ A ∩ ⋂ w, {x | 0 < x.1 w}

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (plusPart A)

Tactic:
convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))

Result:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ plusPart A = A ∩ ⋂ w, {x | 0 < x.1 w}

K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (A ∩ ⋂ w, {x | 0 < x.1 w})

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : { w // w.IsReal }
⊢ MeasurableSet {x | 0 < x.1 x✝}

Tactic:
exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)

Result:
no goals
-- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
theorem surjective_units_map_of_local_ringHom [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Function.Surjective f) (h : IsLocalHom f) :
    Function.Surjective (Units.map <| f.toMonoidHom)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Tactic:
use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ (Units.map ↑f) ⋯.unit = a

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ (Units.map ↑f) ⋯.unit = a

Tactic:
ext

Result:
case h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ↑((Units.map ↑f) ⋯.unit) = ↑a

Proof state:
case h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ↑((Units.map ↑f) ⋯.unit) = ↑a

Tactic:
exact hb

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit (f b)

Tactic:
rw [hb]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit ↑a

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
⊢ Function.Surjective ⇑(Units.map ↑f)

Tactic:
intro a

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Tactic:
obtain ⟨b, hb⟩ := hf (a : S)

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit ↑a

Tactic:
exact Units.isUnit _

Result:
no goals