harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_filter (q) [DecidablePred q] (s : Multiset α) :
    filter p (filter q s) = filter (fun a => p a ∧ q a) s :=
  Quot.inductionOn s fun l => by simp

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk (⇑(isSetoid α)) l)) = filter (fun a => p a ∧ q a) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
@[nolint unusedArguments]
lemma mul_zero_eq {α} {R : α → α → Prop} [Semiring α] {a b : α} (_ : R a 0) (h : b = 0) :
    a * b = 0

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
x✝ : R a 0
h : b = 0
⊢ a * b = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
/-- The operator norm of the first projection `E × F → E` is at most 1. (It is 0 if `E` is zero, so
the inequality cannot be improved without further assumptions.) -/
lemma norm_fst_le : ‖fst 𝕜 E F‖ ≤ 1 :=
  opNorm_le_bound _ zero_le_one (fun ⟨e, f⟩ ↦ by simpa only [one_mul] using le_max_left ‖e‖ ‖f‖)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x✝ : E × F
e : E
f : F
⊢ ‖(fst 𝕜 E F) (e, f)‖ ≤ 1 * ‖(e, f)‖

Tactic:
simpa only [one_mul] using le_max_left ‖e‖ ‖f‖

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem iInf_IicSnd_gt (t : ℚ) {s : Set α} (hs : MeasurableSet s) [IsFiniteMeasure ρ] :
    ⨅ r : { r' : ℚ // t < r' }, ρ.IicSnd r s = ρ.IicSnd t s

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
t : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ⨅ r, (ρ.IicSnd ↑↑r) s = (ρ.IicSnd ↑t) s

Tactic:
simp_rw [ρ.IicSnd_apply _ hs, Measure.iInf_rat_gt_prod_Iic hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a

Tactic:
exact ⟨trivial, fun _ h => h.2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ filter (fun x => x == a) l = replicate (count a l) a

Tactic:
simp only [count, countP_eq_length_filter, eq_replicate_iff, mem_filter, beq_iff_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_const_preimage (U : Set α) (s : Set M) (a : M) :
    (U.mulIndicator fun _ => a) ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α))

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ (U.mulIndicator fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

Tactic:
rw [mulIndicator_const_preimage_eq_union]

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ (U.mulIndicator fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

Tactic:
classical
  rw [mulIndicator_const_preimage_eq_union]
  split_ifs <;> simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_inf' {f g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g)
    (h : InjOn m t) : map m (f ⊓ g) = map m f ⊓ map m g

Proof state:
case intro
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g

Tactic:
lift g to Filter t using htg

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : α → β
t : Set α
h : InjOn m t
f g : Filter ↑t
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : α → β
t : Set α
h : InjOn m t
f g : Filter ↑t
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)

Tactic:
replace h : Injective (m ∘ ((↑) : t → α)) := h.injective

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : α → β
t : Set α
f g : Filter ↑t
h : Injective (m ∘ Subtype.val)
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
lift f to Filter t using htf

Result:
case intro
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : α → β
t : Set α
f g : Filter ↑t
h : Injective (m ∘ Subtype.val)
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)

Tactic:
simp only [map_map, ← map_inf Subtype.coe_injective, map_inf h]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_bot_of_localization_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized' (Rₚ P) P.primeCompl (f P) = ⊥) :
    N = ⊥ :=
  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP ↦ by simpa using h P

Proof state:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized' (Rₚ P) P.primeCompl (f P) N = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ localized' (Rₚ P) P.primeCompl (f P) N = localized' (Rₚ P) P.primeCompl (f P) ⊥

Tactic:
simpa using h P

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem EMetric.isUniformEmbedding_iff' [EMetricSpace β] {f : γ → β} :
    IsUniformEmbedding f ↔
      (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
        ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

Proof state:
β : Type v
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : EMetricSpace β
f : γ → β
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem option_casesOn {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Computable o)
    (hf : Computable f) (hg : Computable₂ g) :
    @Computable _ σ _ _ fun a => Option.casesOn (o a) (f a) (g a) :=
  option_some_iff.1 <|
    (nat_casesOn (encode_iff.2 ho) (option_some_iff.2 hf) (map_decode_iff.2 hg)).of_eq fun a => by
      cases o a <;> simp [encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n => Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))

Tactic:
cases o a <;> simp [encodek]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem mapM_mk_empty [Monad m] (f : α → m β)  :
    (mk #[] rfl).mapM f = pure #v[]

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ mapM.go f { toArray := #[], size_toArray := ⋯ } 0 ⋯ { toArray := #[], size_toArray := ⋯ } =
    pure { toArray := #[], size_toArray := ⋯ }

Tactic:
unfold mapM.go

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ (if h' : 0 < #[].size then do
      let __do_lift ← f { toArray := #[], size_toArray := ⋯ }[0]
      mapM.go f { toArray := #[], size_toArray := ⋯ } (0 + 1) ⋯ ({ toArray := #[], size_toArray := ⋯ }.push __do_lift)
    else pure (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ })) =
    pure { toArray := #[], size_toArray := ⋯ }

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ (if h' : 0 < #[].size then do
      let __do_lift ← f { toArray := #[], size_toArray := ⋯ }[0]
      mapM.go f { toArray := #[], size_toArray := ⋯ } (0 + 1) ⋯ ({ toArray := #[], size_toArray := ⋯ }.push __do_lift)
    else pure (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ })) =
    pure { toArray := #[], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ mapM f { toArray := #[], size_toArray := ⋯ } = pure { toArray := #[], size_toArray := ⋯ }

Tactic:
unfold mapM

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ mapM.go f { toArray := #[], size_toArray := ⋯ } 0 ⋯ { toArray := #[], size_toArray := ⋯ } =
    pure { toArray := #[], size_toArray := ⋯ }
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_add_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) :
    m.leadingCoeff (f + g) = m.leadingCoeff f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + g) = m.leadingCoeff f

Tactic:
simp only [leadingCoeff, m.degree_add_of_lt h, coeff_add, coeff_eq_zero_of_lt h, add_zero]

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ ≤ ‖c n‖

Tactic:
exact (mul_le_of_le_one_right (norm_nonneg _)
  (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖ofScalars E c n‖ ≤ ‖c n‖

Tactic:
simp only [ofScalars_norm_eq_mul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ ≤ ‖c n‖
-- Mathlib/Order/Filter/Basic.lean
theorem biInf_sets_eq {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s)
    (ne : s.Nonempty) : (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets :=
  ext fun t => by simp [mem_biInf_of_directed h ne]

Proof state:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ t ∈ (⨅ i ∈ s, f i).sets ↔ t ∈ ⋃ i ∈ s, (f i).sets

Tactic:
simp [mem_biInf_of_directed h ne]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepFun.isProbabilityMeasure (h : iIndepFun m f μ) : IsProbabilityMeasure μ :=
  ⟨by simpa using h.meas_biInter (S := ∅) (s := fun _ ↦ univ)⟩

Proof state:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : iIndepFun m f μ
⊢ μ univ = 1

Tactic:
simpa using h.meas_biInter (S := ∅) (s := fun _ ↦ univ)

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_dvd {n : ℕ} : exponent G ∣ n ↔ ∀ g : G, orderOf g ∣ n

Proof state:
G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n

Tactic:
simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_eq_length_of_false {p : α → Bool} {xs : List α} (h : ∀ x ∈ xs, p x = false) :
    xs.findIdx p = xs.length

Proof state:
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ xs → p x = false
⊢ ∀ (x : α), x ∈ xs → p x = false

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs = xs.length

Tactic:
rw [findIdx_eq_length]

Result:
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ xs → p x = false
⊢ ∀ (x : α), x ∈ xs → p x = false
-- Mathlib/Data/Num/Lemmas.lean
theorem le_to_nat {m n : PosNum} : (m : ℕ) ≤ n ↔ m ≤ n

Proof state:
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr lt_to_nat

Result:
no goals

Proof state:
m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n
-- Mathlib/Data/List/InsertIdx.lean
theorem get_insertIdx_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length)
    (hn' : n < (insertIdx n x l).length :=
      (by rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff])) :
    (insertIdx n x l).get ⟨n, hn'⟩ = x

Proof state:
α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < (insertIdx n x l).length

Tactic:
rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff]

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n : ℕ
hn : n ≤ l.length
hn' : optParam (n < (insertIdx n x l).length) ⋯
⊢ (insertIdx n x l).get ⟨n, hn'⟩ = x

Tactic:
simp [hn, hn']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_neg_add_lt_right {a b c : Int} (h : -c + a < b) : a < b + c

Proof state:
a b c : Int
h : a + -c < b
⊢ a < b + c

Tactic:
exact Int.lt_add_of_sub_right_lt h

Result:
no goals

Proof state:
a b c : Int
h : -c + a < b
⊢ a < b + c

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a + -c < b
⊢ a < b + c
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem continuousAt_of_locally_lipschitz {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ)
    (h : ∀ y, dist y x < r → dist (f y) (f x) ≤ K * dist y x) : ContinuousAt f x

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Tendsto (fun a => K * dist a x) (𝓝 x) (𝓝 0)

Tactic:
refine (continuous_const.mul (continuous_id.dist continuous_const)).tendsto' _ _ ?_

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ K * dist (id x) x = 0

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ K * dist (id x) x = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ ContinuousAt f x

Tactic:
refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg)
  (mem_of_superset (ball_mem_nhds _ hr) h) ?_)

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Tendsto (fun a => K * dist a x) (𝓝 x) (𝓝 0)
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem mem_carrier_iff (q : Spec.T A⁰_ f) (a : A) :
    a ∈ carrier f_deg q ↔ ∀ i, (HomogeneousLocalization.mk ⟨m * i, ⟨proj 𝒜 i a ^ m, by
      rw [← smul_eq_mul]; mem_tac⟩,
      ⟨f ^ i, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.1 :=
  Iff.rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m * i)

Tactic:
rw [← smul_eq_mul]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformity_eq_comap_nhds_one_swapped :
    𝓤 α = comap (fun x : α × α => x.1 / x.2) (𝓝 (1 : α))

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.2 / x.1) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.1 / x.2) (𝓝 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.1 / x.2) (𝓝 1)

Tactic:
rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.2 / x.1) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.1 / x.2) (𝓝 1)
-- Mathlib/AlgebraicGeometry/Scheme.lean
/-- An alternative ext lemma for scheme morphisms. -/
protected lemma ext' {f g : X ⟶ Y} (h : f.toLRSHom = g.toLRSHom) : f = g

Proof state:
case mk.mk
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h : { toHom_1 := toHom_1✝¹ }.toLRSHom = { toHom_1 := toHom_1✝ }.toLRSHom
⊢ { toHom_1 := toHom_1✝¹ } = { toHom_1 := toHom_1✝ }

Tactic:
congr 1

Result:
no goals

Proof state:
case mk
X Y : Scheme
g : X ⟶ Y
toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h : { toHom_1 := toHom_1✝ }.toLRSHom = toLRSHom g
⊢ { toHom_1 := toHom_1✝ } = g

Tactic:
cases g

Result:
case mk.mk
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h : { toHom_1 := toHom_1✝¹ }.toLRSHom = { toHom_1 := toHom_1✝ }.toLRSHom
⊢ { toHom_1 := toHom_1✝¹ } = { toHom_1 := toHom_1✝ }

Proof state:
X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
⊢ f = g

Tactic:
cases f

Result:
case mk
X Y : Scheme
g : X ⟶ Y
toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h : { toHom_1 := toHom_1✝ }.toLRSHom = toLRSHom g
⊢ { toHom_1 := toHom_1✝ } = g
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAtFilter_sub_const_iff (c : F) :
    HasFDerivAtFilter (f · - c) f' x L ↔ HasFDerivAtFilter f f' x L

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
f' : E →L[𝕜] F
x : E
L : Filter E
c : F
⊢ HasFDerivAtFilter (fun x => f x - c) f' x L ↔ HasFDerivAtFilter f f' x L

Tactic:
simp only [sub_eq_add_neg, hasFDerivAtFilter_add_const_iff]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_fixed {x} (h : f x = x) (n : ℕ) : f^[n] x = x :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ_apply, h, ihn]

Proof state:
α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[n.succ] x = x

Tactic:
rw [iterate_succ_apply, h, ihn]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma setLIntegral_compProd [SFinite μ] [IsSFiniteKernel κ]
    {f : α × β → ℝ≥0∞} (hf : Measurable f)
    {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) :
    ∫⁻ x in s ×ˢ t, f x ∂(μ ⊗ₘ κ) = ∫⁻ a in s, ∫⁻ b in t, f (a, b) ∂(κ a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem powHalf_leftMoves (n) : (powHalf n).LeftMoves = PUnit

Proof state:
n : ℕ
⊢ (powHalf n).LeftMoves = PUnit.{u_1 + 1}

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
lemma lie_lie_smul_f (t : IsSl2Triple h e f) : ⁅h, f⁆ = -((2 : R) • f)

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h e f : L
t : IsSl2Triple h e f
⊢ ⁅h, f⁆ = -(2 • f)

Tactic:
simp [t.lie_h_f_nsmul, two_smul]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Field.lean
lemma cast_inv_le_one : ∀ n : ℕ, (n⁻¹ : α) ≤ 1
  | 0 => by simp
  | n + 1 => inv_le_one_of_one_le₀ <| by simp [Nat.cast_nonneg]

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp [Nat.cast_nonneg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
⊢ (↑0)⁻¹ ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem toSubtype_of_subtype_assoc
    {α β : TypeVec n} (p : α ⟹ «repeat» n Prop) (f : β ⟹ Subtype_ p) :
    @toSubtype n _ p ⊚ ofSubtype _ ⊚ f = f

Proof state:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ toSubtype p ⊚ ofSubtype p ⊚ f = f

Tactic:
rw [← comp_assoc, toSubtype_of_subtype]

Result:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.isUnit [Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a → IsUnit b :=
  let ⟨u, hu⟩ := h
  fun ⟨v, hv⟩ => ⟨v * u, by simp [hv, hu.symm]⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
a b : M
h : a ~ᵤ b
u : Mˣ
hu : a * ↑u = b
x✝ : IsUnit a
v : Mˣ
hv : ↑v = a
⊢ ↑(v * u) = b

Tactic:
simp [hv, hu.symm]

Result:
no goals