harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Jensen.lean
theorem ConvexOn.map_centerMass_le (hf : ConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i)
    (h₁ : 0 < ∑ i ∈ t, w i) (hmem : ∀ i ∈ t, p i ∈ s) :
    f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Tactic:
convert (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2 <;>
  simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Tactic:
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 } := fun i hi =>
  ⟨hmem i hi, le_rfl⟩

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
-- Mathlib/Algebra/Polynomial/Roots.lean
lemma mem_roots_iff_aeval_eq_zero {x : R} (w : p ≠ 0) : x ∈ roots p ↔ aeval x p = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
x : R
w : p ≠ 0
⊢ x ∈ p.roots ↔ (aeval x) p = 0

Tactic:
rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w,
  Algebra.id.map_eq_id, map_id]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_toFinset {m1 m2 : Multiset α} :
    _root_.Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Tactic:
simp [disjoint_left, Finset.disjoint_left]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.smul_of_top_left {f : α → β} {φ : α → 𝕜} (hφ : Integrable φ μ)
    (hf : MemLp f ∞ μ) : Integrable (φ • f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : MemLp φ 1 μ
hf : MemLp f ⊤ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
exact MemLp.smul hf hφ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Integrable φ μ
hf : MemLp f ⊤ μ
⊢ Integrable (φ • f) μ

Tactic:
rw [← memLp_one_iff_integrable] at hφ ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : MemLp φ 1 μ
hf : MemLp f ⊤ μ
⊢ MemLp (φ • f) 1 μ
-- Mathlib/Computability/Primrec.lean
theorem cons {n m f g} (hf : @Primrec' n f) (hg : @Vec n m g) :
    Vec fun v => f v ::ᵥ g v := fun i => Fin.cases (by simp [*]) (fun i => by simp [hg i]) i

Proof state:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Primrec' fun v => ((fun v => f v ::ᵥ g v) v).get i.succ

Tactic:
simp [hg i]

Result:
no goals

Proof state:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin m.succ
⊢ Primrec' fun v => ((fun v => f v ::ᵥ g v) v).get 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Option/Defs.lean
lemma elim'_eq_elim {α β : Type*} (b : β) (f : α → β) (a : Option α) :
    Option.elim' b f a = Option.elim a b f

Proof state:
α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = a.elim b f

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/Quiver/SingleObj.lean
theorem toPrefunctor_symm_comp (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ) :
    toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

Tactic:
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem iterate_pos_le_iff_map_le (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Tactic:
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem norm_unit_smul (u : (𝓞 K)ˣ) (x : mixedSpace K) :
    mixedEmbedding.norm (u • x) = mixedEmbedding.norm x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm (u • x) = mixedEmbedding.norm x

Tactic:
rw [unitSMul_smul, map_mul, norm_unit, one_mul]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_sUnion (S : Set (Set X)) (hc : Set.Countable S)
    (hcomp : ∀ s : S, IsSigmaCompact s (X := X)) : IsSigmaCompact (⋃₀ S)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
apply sUnion_eq_iUnion.symm ▸ isSigmaCompact_iUnion _ hcomp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_Ψ₂Sq_ne_zero (h : (4 : R) ≠ 0) : W.Ψ₂Sq.coeff 3 ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.coeff 3 ≠ 0

Tactic:
rwa [coeff_Ψ₂Sq]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
lemma valuation_p : valuation (p : ℚ_[p]) = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p).valuation = 1

Tactic:
rw [valuation_natCast, padicValNat_self, cast_one]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem bot_coprod (l : Filter β) : (⊥ : Filter α).coprod l = comap Prod.snd l

Proof state:
α : Type u_1
β : Type u_2
l : Filter β
⊢ ⊥.coprod l = comap Prod.snd l

Tactic:
simp [Filter.coprod]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem node3R_size {l x m y r} : size (@node3R α l x m y r) = size l + size m + size r + 2

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
        | nil => 0
        | node sz l x r => sz) +
        (((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
          1) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
rw [← add_assoc, ← add_assoc]

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).size = l.size + m.size + r.size + 2

Tactic:
dsimp [node3R, node', size]

Result:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
        | nil => 0
        | node sz l x r => sz) +
        (((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
          1) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem not_mem_support_iff (x : X) (a : FreeAbelianGroup X) : x ∉ a.support ↔ coeff x a = 0

Proof state:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x = 0 ↔ (coeff x) a = 0

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∉ a.support ↔ (coeff x) a = 0

Tactic:
rw [support, Finsupp.not_mem_support_iff]

Result:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x = 0 ↔ (coeff x) a = 0
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_symm_id (X : D) : (adj.homEquiv _ X).symm (𝟙 _) = adj.counit.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : D
⊢ (adj.homEquiv (G.obj X) X).symm (𝟙 (G.obj X)) = adj.counit.app X

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_smul_id {S : Type*} [SMul S R] [ContinuousConstSMul S R]
    [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)]
    (s : S) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => s • x) a = s • a

Tactic:
rw [cfc_smul .., cfc_id' ..]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, we have that `2 ≤ S'.multiplicity`. -/
lemma Solution'.two_le_multiplicity : 2 ≤ S'.multiplicity

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 2 ≤ S'.multiplicity

Tactic:
simpa [Solution'.multiplicity] using
  S'.multiplicity_lambda_c_finite.le_multiplicity_of_pow_dvd (lambda_sq_dvd_c S')

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem dist_iterate_next_le (f₁ f₂ : FunSpace v) (n : ℕ) :
    dist (next^[n] f₁) (next^[n] f₂) ≤ (v.L * v.tDist) ^ n / n ! * dist f₁ f₂

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
⊢ dist (next^[n] f₁) (next^[n] f₂) ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂

Tactic:
refine dist_le_of_forall fun t => (dist_iterate_next_apply_le _ _ _ _).trans ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : |↑t - ↑v.t₀| ≤ v.tDist
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂

Tactic:
gcongr

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂

Tactic:
have : |(t - v.t₀ : ℝ)| ≤ v.tDist := v.dist_t₀_le t

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : |↑t - ↑v.t₀| ≤ v.tDist
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_zsmul_sub_toIocMod (a b : α) : toIocDiv hp a b • p + toIocMod hp a b = b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p + toIocMod hp a b = b

Tactic:
rw [add_comm, toIocMod_add_toIocDiv_zsmul]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem hom_inv_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
    f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ≅ Y
Z : C
⊢ f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z)

Tactic:
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem update_le_update_iff' : update x i a ≤ update x i b ↔ a ≤ b

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update x i b ↔ a ≤ b

Tactic:
simp [update_le_update_iff]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsRat a (.ofNat n) (nat_lit 1) → IsNat a n
  | _, _, ⟨inv, rfl⟩ => have := @invertibleOne α _; ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑(Int.ofNat a✝) * ⅟↑1 = ↑a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_abs_le_abs_sub (a b : α) : |a| - |b| ≤ |a - b| :=
  sub_le_iff_le_add.2 <|
    calc
      |a| = |a - b + b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a| = |a - b + b|

Tactic:
rw [sub_add_cancel]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem TFAE_mem_nhdsLE {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[≤] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b]`
      s ∈ 𝓝[Icc a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b]`
      s ∈ 𝓝[Ioc a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b]`
      ∃ l ∈ Ico a b, Ioc l b ⊆ s,-- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)`
      ∃ l ∈ Iio b, Ioc l b ⊆ s]

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[≤] b, s ∈ 𝓝[Icc a b] b, s ∈ 𝓝[Ioc a b] b, ∃ l ∈ Ico a b, Ioc l b ⊆ s, ∃ l ∈ Iio b, Ioc l b ⊆ s].TFAE

Tactic:
simpa only [exists_prop, OrderDual.exists, dual_Ici, dual_Ioc, dual_Icc, dual_Ico] using
  TFAE_mem_nhdsGE h.dual (ofDual ⁻¹' s)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem measurableSet_preimage_iff_inter_range {f : X → Z} [CountablySeparated (range f)]
    (hf : Measurable f) (hr : MeasurableSet (range f)) {s : Set Z} :
    MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Proof state:
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
  ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]

Result:
no goals
-- Mathlib/Algebra/Symmetrized.lean
theorem unsym_mul_self [Semiring α] [Invertible (2 : α)] (a : αˢʸᵐ) :
    unsym (a * a) = unsym a * unsym a

Proof state:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ unsym (a * a) = unsym a * unsym a

Tactic:
rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw α β).get? a = none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
a : α
c : Nat
⊢ (empty c).get? a = none

Tactic:
simp_to_raw using Raw₀.get?_empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True

Proof state:
a b : Prop
h : b = True
⊢ (a → b) = True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem eq_iff_abs_toReal_eq_of_sign_eq {θ ψ : Angle} (h : θ.sign = ψ.sign) :
    θ = ψ ↔ |θ.toReal| = |ψ.toReal|

Proof state:
θ ψ : Angle
h : θ.sign = ψ.sign
⊢ θ = ψ ↔ |θ.toReal| = |ψ.toReal|

Tactic:
simpa [h] using @eq_iff_sign_eq_and_abs_toReal_eq θ ψ

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
@[simp] lemma dedup_nsmul [DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) :
    (n • s).dedup = s.dedup

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
by_cases h : a ∈ s <;> simp [h, hn]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_add (f g : ℕ → ℂ) (s : ℂ) : term (f + g) s = term f s + term g s

Proof state:
f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s = term f s + term g s

Tactic:
ext ⟨- | n⟩ <;>
simp [add_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b

Proof state:
n : Nat
a b : Fin n
⊢ a.castSucc = b.castSucc ↔ a = b

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_preimage : negAt s ⁻¹' A = negAt s '' A

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
⊢ ⇑(negAt s) ⁻¹' A = ⇑(negAt s) '' A

Tactic:
rw [ContinuousLinearEquiv.image_eq_preimage, negAt_symm]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem orbitRel_conjAct : ⇑(orbitRel (ConjAct G) G) = IsConj :=
  funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]

Proof state:
G : Type u_3
inst✝ : Group G
g h : G
⊢ (orbitRel (ConjAct G) G) g h = IsConj g h

Tactic:
rw [orbitRel_apply, mem_orbit_conjAct]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_div_primeFactors_mul (n : ℕ) :
    φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Proof state:
n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p

Tactic:
exact prod_pos (fun p => pos_of_mem_primeFactors)

Result:
no goals

Proof state:
n : ℕ
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
  Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]

Result:
n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
-- Mathlib/Logic/Basic.lean
theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R)

Proof state:
P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by_cases p : P <;> simp [p]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg

Proof state:
n : Num
⊢ -n.toZNum = n.toZNumNeg

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2)

Proof state:
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ (do
          let g ← f
          g <$> x).run
      s =
    do
    let fs ← f.run s
    (fun p => (fs.fst p.fst, p.snd)) <$> x.run fs.snd

Tactic:
simp

Result:
no goals

Proof state:
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ (f <*> x).run s = do
    let fs ← f.run s
    (fun p => (fs.fst p.fst, p.snd)) <$> x.run fs.snd

Tactic:
show (f >>= fun g => g <$> x).run s = _

Result:
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ (do
          let g ← f
          g <$> x).run
      s =
    do
    let fs ← f.run s
    (fun p => (fs.fst p.fst, p.snd)) <$> x.run fs.snd
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_eq_zero {x} : arccos x = 0 ↔ 1 ≤ x

Proof state:
x : ℝ
⊢ arccos x = 0 ↔ 1 ≤ x

Tactic:
simp [arccos, sub_eq_zero]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.nhdsSet_prod_eq {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) :
    𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Tactic:
simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
  nhds_prod_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem fundamentalInterior_smul [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) :
    fundamentalInterior G (g • s) = g • fundamentalInterior G s

Proof state:
G : Type u_1
H : Type u_2
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s

Tactic:
simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe :
    TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p :=
  forall₂_congr fun u _ => by simp

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ᶠ (n : ι) in p, ∀ (x : ↑s), ((f ∘ Subtype.val) x, (fun i x => F i ↑x) n x) ∈ u

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
    getKey? (unitOfList l) k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
contains_eq_false : l.contains k = false
⊢ (unitOfList l).getKey? k = none

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
@[simp] lemma liminf_top_eq_iInf (u : β → α) : liminf u ⊤ = ⨅ i, u i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ liminf u ⊤ = ⨅ i, u i

Tactic:
rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]

Result:
no goals