harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_lt_coe_iff {n : ℕ} : krullDim α < n ↔ ∀ l : LTSeries α, l.length < n

Proof state:
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑n ↔ ∀ (l : LTSeries α), l.length < n

Tactic:
rcases n with - | n

Result:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0

case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Proof state:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0

Tactic:
rw [ENat.coe_zero, ← bot_eq_zero, WithBot.lt_coe_bot]

Result:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length = ⊥ ↔ ∀ (l : LTSeries α), l.length < 0

Proof state:
case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Tactic:
simp [WithBot.lt_add_one_iff, WithBot.coe_natCast, Nat.lt_succ]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length = ⊥ ↔ ∀ (l : LTSeries α), l.length < 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ krullDim α < ↑n ↔ ∀ (l : LTSeries α), l.length < n

Tactic:
rw [krullDim, ← WithBot.coe_natCast]

Result:
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑n ↔ ∀ (l : LTSeries α), l.length < n
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toOuterMeasure_uniformOfFinset_apply :
    (uniformOfFinset s hs).toOuterMeasure t = (s.filter (· ∈ t)).card / s.card :=
  calc
    (uniformOfFinset s hs).toOuterMeasure t = ∑' x, if x ∈ t then uniformOfFinset s hs x else 0 :=
      toOuterMeasure_apply (uniformOfFinset s hs) t
    _ = ∑' x, if x ∈ s ∧ x ∈ t then (s.card : ℝ≥0∞)⁻¹ else 0 :=
      (tsum_congr fun x => by simp_rw [uniformOfFinset_apply, ← ite_and, and_comm])
    _ = ∑ x ∈ s.filter (· ∈ t), if x ∈ s ∧ x ∈ t then (s.card : ℝ≥0∞)⁻¹ else 0 :=
      (tsum_eq_sum fun _ hx => if_neg fun h => hx (Finset.mem_filter.2 h))
    _ = ∑ _x ∈ s.filter (· ∈ t), (s.card : ℝ≥0∞)⁻¹ :=
      (Finset.sum_congr rfl fun x hx => by
        let this : x ∈ s ∧ x ∈ t

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ (if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0) = (↑s.card)⁻¹

Tactic:
let this : x ∈ s ∧ x ∈ t := by simpa using hx

Result:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
this : x ∈ s ∧ x ∈ t := Eq.mp Mathlib.Data.Finset.Filter._auxLemma.2 hx
⊢ (if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0) = (↑s.card)⁻¹

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
this : x ∈ s ∧ x ∈ t := Eq.mp Mathlib.Data.Finset.Filter._auxLemma.2 hx
⊢ (if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0) = (↑s.card)⁻¹

Tactic:
simp only [this, and_self_iff, if_true]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
⊢ (if x ∈ t then (uniformOfFinset s hs) x else 0) = if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0

Tactic:
simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ x ∈ s ∧ x ∈ t

Tactic:
simpa using hx

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
⊢ ∑ _x ∈ Finset.filter (fun x => x ∈ t) s, (↑s.card)⁻¹ = ↑(Finset.filter (fun x => x ∈ t) s).card / ↑s.card

Tactic:
simp only [div_eq_mul_inv, Finset.sum_const, nsmul_eq_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {h} (hl : DistinctKeys l) :
    getValue a (eraseKey k l) h = getValue a l (containsKey_of_containsKey_eraseKey hl h)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
h : containsKey a (eraseKey k l) = true
hl : DistinctKeys l
⊢ getValue a (eraseKey k l) h = getValue a l ⋯

Tactic:
rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getValue a (eraseKey k l) h✝ = getValue a l ⋯

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getValue? a l) = some (getValue a l ⋯)

Tactic:
simp [← getValue?_eq_some_getValue]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getValue a (eraseKey k l) h✝ = getValue a l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getValue? a l) = some (getValue a l ⋯)
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_append (ω ω' : List B) : π (ω ++ ω') = π ω * π ω'

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω ω' : List B
⊢ cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'

Tactic:
simp [wordProd]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma neg_mem {x} (hx : x ∈ I) : -x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
hx : x ∈ I
⊢ -x ∈ I

Tactic:
simpa using I.ringCon.neg hx

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem continuous_extend_one [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : U → β}
    (cont : Continuous f) (supp : HasCompactMulSupport f) :
    Continuous (Subtype.val.extend f 1) :=
  continuous_of_mulTSupport fun x h ↦ by
    rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
      ← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]
    exact cont.continuousAt

Proof state:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen U
f : ↑U → β
cont : Continuous f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt f ⟨x, ⋯⟩

Tactic:
exact cont.continuousAt

Result:
no goals

Proof state:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen U
f : ↑U → β
cont : Continuous f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt (extend Subtype.val f 1) x

Tactic:
rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
  (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
  ← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]

Result:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen U
f : ↑U → β
cont : Continuous f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt f ⟨x, ⋯⟩

Proof state:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen U
f : ↑U → β
cont : Continuous f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ x = ↑⟨x, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_prod_const {s : ι → Set α} {t : Set β} : (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ i, s i) ×ˢ t ↔ x✝ ∈ ⋃ i, s i ×ˢ t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
⊢ (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ i, s i) ×ˢ t ↔ x✝ ∈ ⋃ i, s i ×ˢ t
-- Mathlib/Computability/Primrec.lean
theorem to_prim {n f} (pf : @Nat.Primrec' n f) : Primrec f

Proof state:
case zero
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec fun x => 0

Tactic:
exact .const 0

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
⊢ Primrec f

Tactic:
induction pf with
| zero => exact .const 0
| succ => exact _root_.Primrec.succ.comp .vector_head
| get i => exact Primrec.vector_get.comp .id (.const i)
| comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
| @prec n f g _ _ hf hg =>
  exact
    .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
      (hg.comp <|
        Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
        Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
          (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂

Result:
no goals

Proof state:
case comp
n : ℕ
f : List.Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → List.Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
hf : Primrec f✝
hg : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a => f✝ (ofFn fun i => g✝ i a)

Tactic:
exact hf.comp (.vector_ofFn fun i => hg i)

Result:
no goals

Proof state:
case prec
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head

Tactic:
exact
  .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
    (hg.comp <|
      Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
      Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
        (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂

Result:
no goals

Proof state:
case get
n : ℕ
f : List.Vector ℕ n → ℕ
n✝ : ℕ
i : Fin n✝
⊢ Primrec fun v => v.get i

Tactic:
exact Primrec.vector_get.comp .id (.const i)

Result:
no goals

Proof state:
case succ
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec fun v => v.head.succ

Tactic:
exact _root_.Primrec.succ.comp .vector_head

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type*) [Preorder α] [Nonempty α]
    [IsDirected α (· ≤ ·)] [(atTop : Filter α).IsCountablyGenerated] :
    ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop

Proof state:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
refine ⟨xs, ?_, ?_⟩

Result:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Monotone xs

case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Tendsto xs atTop atTop

Proof state:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
choose c hleft hright using exists_ge_ge (α := α)

Result:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@[aesop safe apply]
lemma differentiableAt_smoothingFn {x : ℝ} (hx : 1 < x) : DifferentiableAt ℝ ε x

Proof state:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x

Tactic:
have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)

Result:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ ε x

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (fun z => (log z)⁻¹) x

Tactic:
exact DifferentiableAt.inv (differentiableAt_log (by positivity)) this

Result:
no goals

Proof state:
x : ℝ
hx : 1 < x
⊢ 0 < x

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ ε x

Tactic:
show DifferentiableAt ℝ (fun z => 1 / log z) x

Result:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (fun z => 1 / log z) x

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (fun z => 1 / log z) x

Tactic:
simp_rw [one_div]

Result:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (fun z => (log z)⁻¹) x
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_eq_order [OrderTopology α] (a : α) :
    𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}, 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}, 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
  iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem deriv_arccos : deriv arccos = fun x => -(1 / √(1 - x ^ 2)) :=
  funext fun x => (deriv_const_sub _).trans <| by simp only [deriv_arcsin]

Proof state:
x : ℝ
⊢ -deriv arcsin x = -(1 / √(1 - x ^ 2))

Tactic:
simp only [deriv_arcsin]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem differentiableWithinAt_dslope_of_ne (h : b ≠ a) :
    DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b

Tactic:
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)

Tactic:
refine (eqOn_dslope_slope _ _).eventuallyEq_of_mem ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b

Tactic:
refine ⟨DifferentiableWithinAt.of_dslope, fun hd => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b

Tactic:
refine (((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul
  (hd.sub_const (f a))).congr_of_eventuallyEq ?_ (dslope_of_ne _ h)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive] lemma pow_mul_pow_eq_one : ∀ n, a * b = 1 → a ^ n * b ^ n = 1
  | 0, _ => by simp
  | n + 1, h =>
    calc
      a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Proof state:
M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
rw [pow_succ, pow_succ']

Result:
no goals

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

Tactic:
simp only [mul_assoc]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
a b : M
x✝ : a * b = 1
⊢ a ^ 0 * b ^ 0 = 1

Tactic:
simp

Result:
no goals

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

Tactic:
simp [h, pow_mul_pow_eq_one]

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem normalizer_mono (h : N₁ ≤ N₂) : normalizer N₁ ≤ normalizer N₂

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : m ∈ N₁.normalizer
⊢ m ∈ N₂.normalizer

Tactic:
rw [mem_normalizer] at hm ⊢

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂

Tactic:
exact fun x ↦ h (hm x)

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ N₁.normalizer ≤ N₂.normalizer

Tactic:
intro m hm

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : m ∈ N₁.normalizer
⊢ m ∈ N₂.normalizer
-- Mathlib/Data/Matroid/Constructions.lean
lemma uniqueBaseOn_rankFinite (hI : I.Finite) : RankFinite (uniqueBaseOn I E)

Proof state:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).RankFinite

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Result:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite

Proof state:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite

Tactic:
rw [uniqueBaseOn_isBase_iff inter_subset_right, and_iff_right rfl]

Result:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite

Proof state:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite

Tactic:
exact hI.subset inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite

Tactic:
refine ⟨I ∩ E, ?_⟩

Result:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite
-- Mathlib/Topology/Basic.lean
theorem IsClosed.union : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

Tactic:
simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma isIso_homologyι (hg : S.g = 0) [S.HasHomology] :
    IsIso S.homologyι

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
⊢ IsIso S.homologyι

Tactic:
have := S.isIso_rightHomologyι hg

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
this : IsIso S.rightHomologyι
⊢ IsIso S.homologyι

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
this : IsIso S.rightHomologyι
⊢ IsIso (S.rightHomologyIso.inv ≫ S.rightHomologyι)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
this : IsIso S.rightHomologyι
⊢ IsIso S.homologyι

Tactic:
dsimp only [homologyι]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
this : IsIso S.rightHomologyι
⊢ IsIso (S.rightHomologyIso.inv ≫ S.rightHomologyι)
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma AbsolutelyContinuous.comp_right (hμν : μ ≪ ν) (κ : Kernel α γ) :
    κ ∘ₘ μ ≪ κ ∘ₘ ν

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (⇑κ ∘ₘ ν) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Tactic:
rw [Measure.bind_apply hs (Kernel.measurable _),
  lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Result:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (fun a => (κ a) s) =ᶠ[ae ν] 0
⊢ (fun a => (κ a) s) =ᶠ[ae μ] 0

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
⊢ ⇑κ ∘ₘ μ ≪ ⇑κ ∘ₘ ν

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Result:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (⇑κ ∘ₘ ν) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (fun a => (κ a) s) =ᶠ[ae ν] 0
⊢ (fun a => (κ a) s) =ᶠ[ae μ] 0

Tactic:
exact hμν.ae_eq hs_zero

Result:
no goals