harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem div_smul {R} [Monoid R] [DistribMulAction R K[X]] [IsScalarTower R K[X] K[X]] (c : R)
    (p q : K[X]) :
    algebraMap _ (RatFunc K) (c • p) / algebraMap _ _ q =
      c • (algebraMap _ _ p / algebraMap _ _ q)

Proof state:
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ (algebraMap K[X] (RatFunc K)) (c • p) / (algebraMap K[X] (RatFunc K)) q =
    c • ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q)

Tactic:
rw [← mk_eq_div, mk_smul, mk_eq_div]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem abs_sum_of_nonneg {G : Type*} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι}
    (hf : ∀ i ∈ s, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Proof state:
ι : Type u_1
G : Type u_9
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Tactic:
rw [abs_of_nonneg (Finset.sum_nonneg hf)]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem withDensity_rnDeriv_le (μ ν : Measure α) : ν.withDensity (μ.rnDeriv ν) ≤ μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ

Tactic:
exact Measure.zero_le μ

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
exact Measure.le_add_left le_rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
rw [rnDeriv, dif_neg hl, withDensity_zero]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head?_attach (xs : List α) :
    xs.attach.head? = xs.head?.pbind (fun a h => some ⟨a, mem_of_mem_head? h⟩)

Proof state:
α : Type u_1
xs : List α
⊢ xs.attach.head? = xs.head?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_comp_subtype {s : Set ι} :
    AlgebraicIndependent R (x ∘ (↑) : s → A) ↔
      ∀ p ∈ MvPolynomial.supported R s, aeval x p = 0 → p = 0

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
this✝ : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)
this : ∀ (p : MvPolynomial (↑s) R), (rename Subtype.val) p = 0 ↔ p = 0
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Tactic:
simp [algebraicIndependent_iff, supported_eq_range_rename, *]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Tactic:
have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
this : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
this : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Tactic:
have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
  (injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
    (rename_injective _ Subtype.val_injective)

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
this✝ : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)
this : ∀ (p : MvPolynomial (↑s) R), (rename Subtype.val) p = 0 ↔ p = 0
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)

Tactic:
ext

Result:
case hf
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i✝ : ↑s
⊢ (aeval (x ∘ Subtype.val)) (X i✝) = ((aeval x).comp (rename Subtype.val)) (X i✝)

Proof state:
case hf
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i✝ : ↑s
⊢ (aeval (x ∘ Subtype.val)) (X i✝) = ((aeval x).comp (rename Subtype.val)) (X i✝)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback v : β} :
    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
fallback v : β
⊢ getD (m.insert k v) a fallback = if (k == a) = true then v else getD m a fallback

Tactic:
simp_to_model [insert] using List.getValueD_insertEntry

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_nonpos_iff : sign a ≤ 0 ↔ a ≤ 0

Proof state:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
simp [h, h.not_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Result:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ sign a ≤ 0 ↔ a ≤ 0

case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
simp [← h]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
simp [h, h.le]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem pred_iterate [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) :
    pred^[n] x = x - n

Proof state:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
⊢ pred^[0] x = x - ↑0

Tactic:
rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred^[n + 1] x = x - ↑(n + 1)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
⊢ pred^[n] x = x - ↑n

Tactic:
induction n with
| zero =>
  rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
| succ n IH =>
  rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp] lemma cast_nonneg : ∀ {n : ℤ}, (0 : R) ≤ n ↔ 0 ≤ n
  | (n : ℕ) => by simp
  | -[n+1] => by
    have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
    simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Tactic:
have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one

Result:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Tactic:
simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ -↑n ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑↑n ↔ 0 ≤ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain'_single [DecidableEq ι] [DecidableEq κ] [∀ i, Zero (β i)] (h : κ → ι)
    {h' : ι → κ} (hh' : Function.LeftInverse h' h) (k : κ) (x : β (h k)) :
    comapDomain' h hh' (single (h k) x) = single k x

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain' h hh' (single (h k) x)) i = (single k x) i

Tactic:
rw [comapDomain'_apply]

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
obtain rfl | hik := Decidable.eq_or_ne i k

Result:
case h.inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
x : β (h i)
⊢ (single (h i) x) (h i) = (single i x) i

case h.inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Proof state:
case h.inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
x : β (h i)
⊢ (single (h i) x) (h i) = (single i x) i

Tactic:
rw [single_eq_same, single_eq_same]

Result:
no goals

Proof state:
case h.inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
rw [single_eq_of_ne hik.symm, single_eq_of_ne (hh'.injective.ne hik.symm)]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
⊢ comapDomain' h hh' (single (h k) x) = single k x

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain' h hh' (single (h k) x)) i = (single k x) i
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_div_cancel' (a b c : G) : a / b * (c / a) = c / b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / b * (c / a) = c / b

Tactic:
rw [mul_comm]

Result:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a * (a / b) = c / b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a * (a / b) = c / b

Tactic:
apply div_mul_div_cancel

Result:
no goals
-- Mathlib/GroupTheory/Perm/ConjAct.lean
theorem cycleFactorsFinset_conj_eq
    (k : ConjAct (Perm α)) (g : Perm α) :
    cycleFactorsFinset (k • g) = k • cycleFactorsFinset g

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset

Tactic:
ext c

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
exact Finset.inv_smul_mem_iff

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
simp only [inv_smul_smul]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w &&& x).getLsbD i = (0#w).getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 0#w &&& x = 0#w

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w &&& x).getLsbD i = (0#w).getLsbD i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem any_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.any q (guard p a) = (p a && q a)

Proof state:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.any q (if p a then some a else none) = (decide (p a) && q a)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.any q (guard p a) = (decide (p a) && q a)

Tactic:
simp only [guard]

Result:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.any q (if p a then some a else none) = (decide (p a) && q a)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
lemma tendsto_measure_Icc_nhdsWithin_right' (b : ℝ) :
    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[>] (0 : ℝ)) (𝓝 (μ {b}))

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b + r ≤ b + s

Tactic:
linarith

Result:
no goals

Proof state:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)

Tactic:
intro r s _rpos hrs

Result:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ Icc (b - r) (b + r) ⊆ Icc (b - s) (b + s)

Proof state:
case hf
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∃ r > 0, μ (Icc (b - r) (b + r)) ≠ ⊤

Tactic:
exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩

Result:
no goals

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b - s ≤ b - r

Tactic:
linarith

Result:
no goals

Proof state:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ Icc (b - r) (b + r) ⊆ Icc (b - s) (b + s)

Tactic:
exact Icc_subset_Icc (by linarith) (by linarith)

Result:
no goals

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ (⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r))))

Tactic:
apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)

Result:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)

case hf
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∃ r > 0, μ (Icc (b - r) (b + r)) ≠ ⊤

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ {b}))

Tactic:
rw [Real.singleton_eq_inter_Icc]

Result:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ (⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r))))
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem one_smul (x : X[S⁻¹]) : (1 : R[S⁻¹]) • x = x

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ 1 • (r /ₒ s) = r /ₒ s

Proof state:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ 1 • (r /ₒ s) = r /ₒ s

Tactic:
simp [OreLocalization.one_def, oreDiv_smul_char 1 r 1 s 1 s (by simp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
lemma isProper_eq : @IsProper =
    (@IsSeparated ⊓ @UniversallyClosed : MorphismProperty Scheme) ⊓ @LocallyOfFiniteType

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
rw [isProper_iff, ← and_assoc]

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Proof state:
⊢ @IsProper = @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essInf_count_eq_ciInf (hf : BddBelow (Set.range f)) :
    essInf f .count = ⨅ a, f a := essInf_eq_ciInf (by simp) hf

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝² : ConditionallyCompleteLattice β
f : α → β
inst✝¹ : Nonempty α
inst✝ : MeasurableSingletonClass α
hf : BddBelow (range f)
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
@[to_additive (attr := simp, norm_cast)]
lemma coe_mul_coe [SetLike S M] [SubmonoidClass S M] (H : S) : H * H = (H : Set M)

Proof state:
M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
H : S
⊢ ↑H * ↑H = ↑H

Tactic:
aesop (add simp mem_mul)

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem star_mul_self [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (star x * x)

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (star x * x)

Tactic:
simp only [IsSelfAdjoint, star_mul, star_star]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma completedCosZeta_residue_zero (a : UnitAddCircle) :
    Tendsto (fun s ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
s : ℂ
⊢ ((fun s => s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun s => s / 2) s = s * completedCosZeta a s

Tactic:
simp [completedCosZeta, div_mul_eq_mul_div, mul_div_assoc]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0)
  (𝓝 (-1)) := (hurwitzEvenFEPair a).symm.Λ_residue_zero

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
⊢ Tendsto (fun s => s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
⊢ Tendsto (fun s => s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Tactic:
refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
s : ℂ
⊢ ((fun s => s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun s => s / 2) s = s * completedCosZeta a s
-- Mathlib/Data/Set/Prod.lean
theorem preimage_coe_coe_diagonal (s : Set α) :
    Prod.map (fun x : s => (x : α)) (fun x : s => (x : α)) ⁻¹' diagonal α = diagonal s

Proof state:
case h.mk.mk.mk
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (⟨x, hx⟩, ⟨y, hy⟩) ∈ (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' diagonal α ↔ (⟨x, hx⟩, ⟨y, hy⟩) ∈ diagonal ↑s

Tactic:
simp [Set.diagonal]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' diagonal α = diagonal ↑s

Tactic:
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

Result:
case h.mk.mk.mk
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (⟨x, hx⟩, ⟨y, hy⟩) ∈ (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' diagonal α ↔ (⟨x, hx⟩, ⟨y, hy⟩) ∈ diagonal ↑s