harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Jensen.lean
/-- A form of the **equality case of Jensen's equality**.

For a strictly concave function `f` and positive weights `w`, if
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)`, then the points `p` are all equal.

See also `StrictConcaveOn.map_sum_eq_iff`. -/
lemma StrictConcaveOn.eq_of_map_sum_eq (hf : StrictConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s)
    (h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)) :
    ∀ ⦃j⦄, j ∈ t → ∀ ⦃k⦄, k ∈ t → p j = p k

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 : StrictConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
exact h_eq.not_lt <| hf.lt_map_sum h₀ h₁ hmem this

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 : StrictConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!

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 : StrictConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_conj : tan (conj x) = conj (tan x)

Proof state:
x : ℂ
⊢ tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
rw [tan, sin_conj, cos_conj, ← map_div₀, tan]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
    (hn : n < (pmap f l h).length) :
    get (pmap f l h) ⟨n, hn⟩ =
      f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn)))

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
hn : n < (pmap f l h).length
⊢ (pmap f l h).get ⟨n, hn⟩ = f (l.get ⟨n, ⋯⟩) ⋯

Tactic:
simp only [get_eq_getElem]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
hn : n < (pmap f l h).length
⊢ (pmap f l h)[n] = f l[n] ⋯

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
hn : n < (pmap f l h).length
⊢ (pmap f l h)[n] = f l[n] ⋯

Tactic:
simp [getElem_pmap]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_symm_inf (s₁ s₂) :
    letI e := isIdempotentElemEquivClopens (R := R).symm
    e (s₁ ⊓ s₂) = ⟨_, (e s₁).2.mul (e s₂).2⟩ :=
  isIdempotentElemEquivClopens.symm_apply_eq.mpr <| by
    simp_rw [isIdempotentElemEquivClopens_mul, Equiv.apply_symm_apply]

Proof state:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ s₁ ⊓ s₂ =
    isIdempotentElemEquivClopens ⟨↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂), ⋯⟩

Tactic:
simp_rw [isIdempotentElemEquivClopens_mul, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_boole_mul' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
    𝔼 j, ite (j = i) (Fintype.card ι : M) 0 * f j = f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ 𝔼 j : ι, (if j = i then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
simp_rw [@eq_comm _ _ i, expect_boole_mul]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_sum {f : β ⊕ γ → α} : ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) :=
  eq_of_forall_ge_iff fun c => by simp only [sup_le_iff, iSup_le_iff, Sum.forall]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β ⊕ γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) ≤ c

Tactic:
simp only [sup_le_iff, iSup_le_iff, Sum.forall]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem cons_product : (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t

Proof state:
α : Type u_1
β : Type v
a : α
s : Multiset α
t : Multiset β
⊢ (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_sdiff_offDiag : s ×ˢ s \ s.offDiag = s.diag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s ×ˢ s \ s.offDiag = s.diag

Tactic:
rw [← diag_union_offDiag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _)]

Result:
no goals
-- Mathlib/Data/Real/Pointwise.lean
theorem Real.iSup_mul_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (⨆ i, f i) * r = ⨆ i, f i * r

Proof state:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨆ i, f i * r

Tactic:
simp only [Real.mul_iSup_of_nonneg ha, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
    (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j

Proof state:
s n i : Nat
p : Nat → Bool
⊢ find? p (List.range' s n).toArray = some i ↔
    p i = true ∧ i ∈ (List.range' s n).toArray ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
simp only [List.find?_toArray, mem_toArray]

Result:
s n i : Nat
p : Nat → Bool
⊢ List.find? p (List.range' s n) = some i ↔
    p i = true ∧ i ∈ List.range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Proof state:
s n i : Nat
p : Nat → Bool
⊢ find? p (range' s n) = some i ↔ p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
rw [← List.toArray_range']

Result:
s n i : Nat
p : Nat → Bool
⊢ find? p (List.range' s n).toArray = some i ↔
    p i = true ∧ i ∈ (List.range' s n).toArray ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Proof state:
s n i : Nat
p : Nat → Bool
⊢ List.find? p (List.range' s n) = some i ↔
    p i = true ∧ i ∈ List.range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
simp [List.find?_range'_eq_some]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_curry (f : α × β → M) :
    (mulSupport f.curry) = (mulSupport f).image Prod.fst

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : One M
f : α × β → M
⊢ mulSupport (curry f) = Prod.fst '' mulSupport f

Tactic:
simp [mulSupport, funext_iff, image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j)

Proof state:
w i j : Nat
⊢ twoPow w i * twoPow w j = twoPow w (i + j)

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w i j : Nat
⊢ (twoPow w i * twoPow w j).toNat = (twoPow w (i + j)).toNat

Proof state:
case a
w i j : Nat
⊢ 2 ^ i % 2 ^ w * (2 ^ j % 2 ^ w) % 2 ^ w = 2 ^ (i + j) % 2 ^ w

Tactic:
rw [← Nat.mul_mod, Nat.pow_add]

Result:
no goals

Proof state:
case a
w i j : Nat
⊢ (twoPow w i * twoPow w j).toNat = (twoPow w (i + j)).toNat

Tactic:
simp only [toNat_mul, toNat_twoPow]

Result:
case a
w i j : Nat
⊢ 2 ^ i % 2 ^ w * (2 ^ j % 2 ^ w) % 2 ^ w = 2 ^ (i + j) % 2 ^ w
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem forall_smul_mem_iff {R M S : Type*} [Monoid R] [MulAction R M] [SetLike S M]
    [SMulMemClass S R M] {N : S} {x : M} : (∀ a : R, a • x ∈ N) ↔ x ∈ N :=
  ⟨fun h => by simpa using h 1, fun h a => SMulMemClass.smul_mem a h⟩

Proof state:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : SetLike S M
inst✝ : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N

Tactic:
simpa using h 1

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Lemmas.lean
theorem Heap.deleteMin_fst : ((s : Heap α).deleteMin le).map (·.1) = s.head? le :=
  match s with
  | .nil => rfl
  | .cons r a c s => by simp only [deleteMin, findMin_val, Option.map, head?]

Proof state:
α : Type u_1
s✝ : Heap α
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ Option.map (fun x => x.fst) (deleteMin le (cons r a c s)) = head? le (cons r a c s)

Tactic:
simp only [deleteMin, findMin_val, Option.map, head?]

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_apply_one (hk : 0 < k) : hasseDeriv k (1 : R[X]) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 0 < k
⊢ (hasseDeriv k) 1 = 0

Tactic:
rw [← C_1, hasseDeriv_C k _ hk]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem sub_add {X Y : C} (a b c : X ⟶ Y) : a - b + c = a - (b - c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - b + c = a - (b - c)

Tactic:
rw [add_def, neg_def, sub_sub_sub, sub_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma div_mul_cancel_of_imp (h : b = 0 → a = 0) : a / b * b = a

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;>  simp [*]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.sup {N₁ N₂ : L.Substructure M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG :=
  let ⟨t₁, ht₁⟩ := fg_def.1 hN₁
  let ⟨t₂, ht₂⟩ := fg_def.1 hN₂
  fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [closure_union, ht₁.2, ht₂.2]⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ (closure L).toFun t₂ = N₂
⊢ (closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isBigO_cpow_rpow (hl : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|) :
    (fun x => f x ^ g x) =O[l] fun x => ‖f x‖ ^ (g x).re :=
  calc
    (fun x => f x ^ g x) =O[l]
        (show α → ℝ from fun x => ‖f x‖ ^ (g x).re / Real.exp (arg (f x) * im (g x))) :=
      isBigO_of_le _ fun _ => (norm_cpow_le _ _).trans (le_abs_self _)
    _ =Θ[l] (show α → ℝ from fun x => ‖f x‖ ^ (g x).re / (1 : ℝ)) :=
      ((isTheta_refl _ _).div (isTheta_exp_arg_mul_im hl))
    _ =ᶠ[l] (show α → ℝ from fun x => ‖f x‖ ^ (g x).re)

Proof state:
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|
⊢ (let_fun this := fun x => ‖f x‖ ^ (g x).re / 1;
    this) =ᶠ[l]
    let_fun this := fun x => ‖f x‖ ^ (g x).re;
    this

Tactic:
simp only [ofReal_one, div_one, EventuallyEq.rfl]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem toNNReal_div (a b : ℝ≥0∞) : (a / b).toNNReal = a.toNNReal / b.toNNReal

Proof state:
a b : ℝ≥0∞
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal

Tactic:
rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_lt [LinearOrderedSemiring α] {m n : Num} : (m : α) < n ↔ m < n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : Num
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]

Result:
no goals
-- Mathlib/.lake/packages/aesop/Aesop/Util/Basic.lean
theorem size_modify (a : Array α) (i : Nat) (f : α → α) :
    (a.modify i f).size = a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ (a.modify i f).size = a.size

Tactic:
simp only [Array.modify, Id.run, Array.modifyM]

Result:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size
      (if h : i < a.size then do
        let v ← f a[i]
        pure (a.set i v ⋯)
      else pure a) =
    a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size
      (if h : i < a.size then do
        let v ← f a[i]
        pure (a.set i v ⋯)
      else pure a) =
    a.size

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_bihimp_cancel_left : a ⇔ (a ⇔ b) = b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ (a ⇔ b) = b

Tactic:
simp [← bihimp_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma zero_nnrpow {x : ℝ≥0} : (0 : A) ^ x = 0

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
x : ℝ≥0
⊢ 0 ^ x = 0

Tactic:
simp [nnrpow_def]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem length_ndinsert_of_mem {a : α} {s : Multiset α} (h : a ∈ s) :
    card (ndinsert a s) = card s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (ndinsert a s).card = s.card

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sigma_apply_prime_pow {k p i : ℕ} (hp : p.Prime) :
    σ k (p ^ i) = ∑ j ∈ .range (i + 1), p ^ (j * k)

Proof state:
k p i : ℕ
hp : Nat.Prime p
⊢ (σ k) (p ^ i) = ∑ j ∈ range (i + 1), p ^ (j * k)

Tactic:
simp [sigma_apply, divisors_prime_pow hp, Nat.pow_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_filter_mul_prod_filter_not (p) [DecidablePred p] :
    (s.filter p).prod * (s.filter (fun a ↦ ¬ p a)).prod = s.prod

Proof state:
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter p s).prod * (filter (fun a => ¬p a) s).prod = s.prod

Tactic:
rw [← prod_add, filter_add_not]

Result:
no goals
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_iff {x y z : Tropical R} : x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Proof state:
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop]

Result:
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ untrop x ⊓ untrop y = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Proof state:
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ untrop x ⊓ untrop y = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
simp [min_eq_iff]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
lemma Absorbs.sub {s₁ s₂ t₁ t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
    Absorbs M (s₁ - s₂) (t₁ - t₂)

Proof state:
M : Type u_1
E : Type u_2
inst✝³ : Monoid M
inst✝² : AddGroup E
inst✝¹ : DistribMulAction M E
inst✝ : Bornology M
s₁ s₂ t₁ t₂ : Set E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
⊢ Absorbs M (s₁ - s₂) (t₁ - t₂)

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_neg

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioo_pred_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (pred a) b = Ico a b :=
  coe_injective <| by simpa using Set.Ioo_pred_left_eq_Ioc_of_not_isMin ha _

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

Tactic:
simpa using Set.Ioo_pred_left_eq_Ioc_of_not_isMin ha _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Basic.lean
theorem nil_merge (ys : List α) : merge [] ys le = ys

Proof state:
α : Type u_1
le : α → α → Bool
ys : List α
⊢ [].merge ys le = ys

Tactic:
simp [merge]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoc_eq_union : Ι a b = Ioc a b ∪ Ioc b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
cases le_total a b <;> simp [uIoc, *]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem Filter.Eventually.union_nhdsSet {p : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ x in 𝓝ˢ s, p x) ∧ ∀ᶠ x in 𝓝ˢ t, p x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x

Tactic:
rw [nhdsSet_union, eventually_sup]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_eq_nat {φ : R⟦X⟧} {n : ℕ} :
    order φ = n ↔ coeff R n φ ≠ 0 ∧ ∀ i, i < n → coeff R i φ = 0

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ order 0 = ↑n ↔ (coeff R n) 0 ≠ 0 ∧ ∀ i < n, (coeff R i) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff R n) φ ≠ 0 ∧ ∀ i < n, (coeff R i) φ = 0

Tactic:
simp [order, dif_neg hφ, Nat.find_eq_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = ↑n ↔ (coeff R n) φ ≠ 0 ∧ ∀ i < n, (coeff R i) φ = 0

Tactic:
rcases eq_or_ne φ 0 with (rfl | hφ)

Result:
case inl
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ order 0 = ↑n ↔ (coeff R n) 0 ≠ 0 ∧ ∀ i < n, (coeff R i) 0 = 0

case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff R n) φ ≠ 0 ∧ ∀ i < n, (coeff R i) φ = 0
-- Mathlib/Data/Matroid/Closure.lean
lemma Spanning.closure_eq_of_superset (hS : M.Spanning S) (hST : S ⊆ T) : M.closure T = M.E

Proof state:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.Spanning (T ∩ M.E)

Tactic:
exact hS.superset (subset_inter hST hS.subset_ground)

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.closure T = M.E

Tactic:
rw [← closure_inter_ground, ← spanning_iff_closure_eq]

Result:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.Spanning (T ∩ M.E)
-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma deriv_cgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) :
    deriv (cgf X μ) 0 = μ[X] / (μ Set.univ).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) 0 = (∫ (x : Ω), X x ∂μ) / (μ Set.univ).toReal

Tactic:
simp [deriv_cgf h]

Result:
no goals
-- Mathlib/Topology/Ultrafilter.lean
theorem isOpen_iff_ultrafilter :
    IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l

Tactic:
simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_mul {R} [CommSemiring R] (r : R) (p q : R[X]) :
    taylor r (p * q) = taylor r p * taylor r q

Proof state:
R : Type u_2
inst✝ : CommSemiring R
r : R
p q : R[X]
⊢ (taylor r) (p * q) = (taylor r) p * (taylor r) q

Tactic:
simp only [taylor_apply, mul_comp]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma isoClosure_eq_self (P : MorphismProperty C) [P.RespectsIso] :
    P.isoClosure = P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.isoClosure = P

Tactic:
rwa [isoClosure_eq_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem lt_iff : μ < ν ↔ μ ≤ ν ∧ ∃ s, MeasurableSet s ∧ μ s < ν s :=
  lt_iff_le_not_le.trans <|
    and_congr Iff.rfl <| by simp only [le_iff, not_forall, not_le, exists_prop]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ¬ν ≤ μ ↔ ∃ s, MeasurableSet s ∧ μ s < ν s

Tactic:
simp only [le_iff, not_forall, not_le, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
    get? (m.insert k v) k = some v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β
⊢ get? (m.insert k v) k = some v

Tactic:
simp_to_raw using Raw₀.Const.get?_insert_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.ushiftRight_self (n : BitVec w) : n >>> n = 0#w

Proof state:
w : Nat
n : BitVec w
⊢ n >>> n = 0#w

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_two_sub (x : ℝ) : cos (π / 2 - x) = sin x

Proof state:
x : ℝ
⊢ cos (π / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma rewrites_reverse : r.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u v :=
  ⟨fun h ↦ by simpa using h.reverse, .reverse⟩

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
h : r.reverse.Rewrites u.reverse v.reverse
⊢ r.Rewrites u v

Tactic:
simpa using h.reverse

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

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

Tactic:
simp [Functor.map, StateT.map, run, ←bind_pure_comp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem deriv_log (x : ℝ) : deriv log x = x⁻¹ :=
  if hx : x = 0 then by
    rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
  else (hasDerivAt_log hx).deriv

Proof state:
x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem preimageOfMemIntegerSet_mixedEmbedding {x : (𝓞 K)}
    (hx : mixedEmbedding K (x : 𝓞 K) ∈ integerSet K) :
    preimageOfMemIntegerSet (⟨mixedEmbedding K (x : 𝓞 K), hx⟩) = x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ ↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = x

Tactic:
simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
  mixedEmbedding_preimageOfMemIntegerSet]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_eq_support_sub : f.neLocus g = (f - g).support

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus g = (f - g).support

Tactic:
rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem «forall» {p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b) :=
  ⟨fun h _ _ => h _,
   fun h q => by
    have := h q.num q.den
    rwa [Int.cast_natCast, num_div_den q] at this⟩

Proof state:
p : ℚ → Prop
h : ∀ (a b : ℤ), p (↑a / ↑b)
q : ℚ
this : p (↑q.num / ↑↑q.den)
⊢ p q

Tactic:
rwa [Int.cast_natCast, num_div_den q] at this

Result:
no goals

Proof state:
p : ℚ → Prop
h : ∀ (a b : ℤ), p (↑a / ↑b)
q : ℚ
⊢ p q

Tactic:
have := h q.num q.den

Result:
p : ℚ → Prop
h : ∀ (a b : ℤ), p (↑a / ↑b)
q : ℚ
this : p (↑q.num / ↑↑q.den)
⊢ p q