harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Semiquot.lean
theorem IsPure.min {s t : Semiquot α} (h : IsPure t) : s ≤ t ↔ s = t :=
  ⟨fun st =>
    le_antisymm st <| by
      rw [eq_pure h, eq_pure (h.mono st)]; simpa using h _ (get_mem _) _ (st <| get_mem _),
    le_of_eq⟩

Proof state:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)

Tactic:
simpa using h _ (get_mem _) _ (st <| get_mem _)

Result:
no goals

Proof state:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ t ≤ s

Tactic:
rw [eq_pure h, eq_pure (h.mono st)]

Result:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ioc_consecutive (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
    ((∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)

Tactic:
apply disjoint_left.2 fun x hx h'x => _

Result:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ x ∈ Ioc m n, x ∈ Ioc n k → False

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i

Tactic:
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]

Result:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ x ∈ Ioc m n, x ∈ Ioc n k → False

Tactic:
intros x hx h'x

Result:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False

Tactic:
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

Result:
no goals
-- Mathlib/Topology/Constructible.lean
lemma _root_.IsRetrocompact.isCompact (hs : IsRetrocompact s) : IsCompact s

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : CompactSpace X
hs : IsRetrocompact s
⊢ IsCompact s

Tactic:
simpa using hs CompactSpace.isCompact_univ

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_logb (hx : 0 < x) (hxy : x < y) : logb b x < logb b y

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
exact log_lt_log hx hxy

Result:
no goals

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ logb b x < logb b y

Tactic:
rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]

Result:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
-- Mathlib/Topology/Algebra/Monoid.lean
theorem tendsto_list_prod {f : ι → α → M} {x : Filter α} {a : ι → M} :
    ∀ l : List ι,
      (∀ i ∈ l, Tendsto (f i) x (𝓝 (a i))) →
        Tendsto (fun b => (l.map fun c => f c b).prod) x (𝓝 (l.map a).prod)
  | [], _ => by simp [tendsto_const_nhds]
  | f::l, h => by
    simp only [List.map_cons, List.prod_cons]
    exact
      (h f (List.mem_cons_self _ _)).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

Proof state:
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * (List.map (fun c => f✝ c b) l).prod) x (𝓝 (a f * (List.map a l).prod))

Tactic:
exact
  (h f (List.mem_cons_self _ _)).mul
    (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
x✝ : ∀ i ∈ [], Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun b => (List.map (fun c => f c b) []).prod) x (𝓝 (List.map a []).prod)

Tactic:
simp [tendsto_const_nhds]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => (List.map (fun c => f✝ c b) (f :: l)).prod) x (𝓝 (List.map a (f :: l)).prod)

Tactic:
simp only [List.map_cons, List.prod_cons]

Result:
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * (List.map (fun c => f✝ c b) l).prod) x (𝓝 (a f * (List.map a l).prod))
-- Mathlib/Data/Set/BoolIndicator.lean
theorem preimage_boolIndicator (t : Set Bool) :
    s.boolIndicator ⁻¹' t = univ ∨
      s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅

Proof state:
α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅

Tactic:
simp only [preimage_boolIndicator_eq_union]

Result:
α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅

Proof state:
α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅

Tactic:
split_ifs <;> simp [s.union_compl_self]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
/-- Multiplying with `swap R i j` on the left swaps the `j`-th row with the `i`-th row. -/
@[simp]
lemma swap_mul_apply_right (i j : n) (a : m) (g : Matrix n m R) :
    (swap R i j * g) j a = g i a

Proof state:
R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix n m R
⊢ (swap R i j * g) j a = g i a

Tactic:
rw [swap_comm, swap_mul_apply_left]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_balanceL {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
    (H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') :
    size (@balanceL α l x r) = size l + size r + 1

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ (l.balanceL x r).size = l.size + r.size + 1

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_mem_of_size_pos {l : Array α} (h : 0 < l.size) : ∃ a, a ∈ l

Proof state:
case mk
α : Type u_1
toList✝ : List α
h : 0 < { toList := toList✝ }.size
⊢ ∃ a, a ∈ { toList := toList✝ }

Tactic:
simpa using List.exists_mem_of_length_pos h

Result:
no goals

Proof state:
α : Type u_1
l : Array α
h : 0 < l.size
⊢ ∃ a, a ∈ l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
h : 0 < { toList := toList✝ }.size
⊢ ∃ a, a ∈ { toList := toList✝ }
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_iff' {f : α → β} :
    IsUniformEmbedding f ↔
      Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
    (f : α → α) (hj : j < (as.modify i f).size) :
    (as.modify i f)[j] = as[j]'(by simpa using hj)

Proof state:
α : Type u_1
j : Nat
as : Array α
i : Nat
h : i ≠ j
f : α → α
hj : j < (as.modify i f).size
⊢ (as.modify i f)[j] = as[j]

Tactic:
simp [getElem_modify hj, h]

Result:
no goals

Proof state:
α : Type ?u.513361
j : Nat
as : Array α
i : Nat
h : i ≠ j
f : α → α
hj : j < (as.modify i f).size
⊢ j < as.size

Tactic:
simpa using hj

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma Odd.neg_one_pow (h : Odd n) : (-1 : α) ^ n = -1

Proof state:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
rw [h.neg_pow, one_pow]

Result:
no goals
-- Mathlib/Data/Matrix/Reflection.lean
theorem mulᵣ_eq [Mul α] [AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α)
    (B : Matrix (Fin m) (Fin n) α) : mulᵣ A B = A * B

Proof state:
l m n : ℕ
α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ A.mulᵣ B = A * B

Tactic:
simp [mulᵣ, Function.comp, Matrix.transpose]

Result:
l m n : ℕ
α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ of ((fun v₁ => (fun v₂ => v₁ ⬝ᵥ v₂) ∘ of fun x y => B y x) ∘ A) = A * B

Proof state:
l m n : ℕ
α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ of ((fun v₁ => (fun v₂ => v₁ ⬝ᵥ v₂) ∘ of fun x y => B y x) ∘ A) = A * B

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.lift_fst_comp_snd_comp {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z]
    (g : W ⟶ X) (g' : Y ⟶ Z) : prod.lift (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
rw [← prod.lift_map]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
-- Mathlib/Analysis/Convolution.lean
theorem smul_convolution [SMulCommClass ℝ 𝕜 F] {y : 𝕜} : y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g)

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (y • f ⋆[L, μ] g) x✝ = (y • (f ⋆[L, μ] g)) x✝

Tactic:
simp only [Pi.smul_apply, convolution_def, ← integral_smul, L.map_smul₂]

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g)

Tactic:
ext

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (y • f ⋆[L, μ] g) x✝ = (y • (f ⋆[L, μ] g)) x✝
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp]
lemma coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
⊢ ↑s ∩ ↑t = ↑(s.bagInter t)

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)
-- Mathlib/Logic/Function/Basic.lean
theorem update_idem {α} [DecidableEq α] {β : α → Sort*} {a : α} (v w : β a) (f : ∀ a, β a) :
    update (update f a v) a w = update f a w

Proof state:
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w

Tactic:
funext b

Result:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b

Proof state:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b

Tactic:
by_cases h : b = a <;> simp [update, h]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem isAlgebraic_iff_isIntegral {x : A} : IsAlgebraic K x ↔ IsIntegral K x

Proof state:
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ IsIntegral K x

Tactic:
refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩

Result:
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ eval₂ (algebraMap K A) x (p * C p.leadingCoeff⁻¹) = 0

Proof state:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x → IsIntegral K x

Tactic:
rintro ⟨p, hp, hpx⟩

Result:
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ IsIntegral K x

Proof state:
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ eval₂ (algebraMap K A) x (p * C p.leadingCoeff⁻¹) = 0

Tactic:
rw [← aeval_def, map_mul, hpx, zero_mul]

Result:
no goals

Proof state:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x

Tactic:
refine ⟨?_, IsIntegral.isAlgebraic⟩

Result:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x → IsIntegral K x
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem dvd_iterate_derivative_pow (f : R[X]) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) :
    (n : R) ∣ eval c (derivative^[m] (f ^ n))

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m.succ] (f ^ n))

Tactic:
rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast,
  iterate_derivative_natCast_mul, eval_mul, eval_natCast]

Result:
case intro
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n m : ℕ
c : R
hm : m ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (f ^ n))

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm

Result:
case intro
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m.succ] (f ^ n))
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_natCast (n : ℕ) : (n : R[X]).eval₂ f x = n

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ↑n = ↑n

Tactic:
induction n with
| zero => simp only [eval₂_zero, Nat.cast_zero]
| succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

Result:
no goals

Proof state:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑(n + 1) = ↑(n + 1)

Tactic:
rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

Result:
no goals

Proof state:
case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ↑0 = ↑0

Tactic:
simp only [eval₂_zero, Nat.cast_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[]

Proof state:
α : Type u_1
xs : Array α
⊢ #[] = xs ↔ xs = #[]

Tactic:
cases xs <;> simp

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contDiffWithinAtProp_mono_of_mem_nhdsWithin
    (n : WithTop ℕ∞) ⦃s x t⦄ ⦃f : H → H'⦄ (hts : s ∈ 𝓝[t] x)
    (h : ContDiffWithinAtProp I I' n f s x) : ContDiffWithinAtProp I I' n f t x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ↑I.symm ⁻¹' s ∩ range ↑I ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x

Tactic:
refine inter_mem ?_ (mem_of_superset self_mem_nhdsWithin inter_subset_right)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ↑I.symm ⁻¹' s ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ContDiffWithinAtProp I I' n f t x

Tactic:
refine h.mono_of_mem_nhdsWithin ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ↑I.symm ⁻¹' s ∩ range ↑I ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ↑I.symm ⁻¹' s ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x

Tactic:
rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_iff_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot]
    (hε : Tendsto ε l (𝓝[≠] 0)) {S : Set E} :
    IsVonNBounded 𝕜 S ↔ ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0) :=
  ⟨fun hS _ hxS => hS.smul_tendsto_zero (Eventually.of_forall hxS) (le_trans hε nhdsWithin_le_nhds),
    isVonNBounded_of_smul_tendsto_zero (by exact hε self_mem_nhdsWithin)⟩

Proof state:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : Tendsto ε l (𝓝[≠] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0

Tactic:
exact hε self_mem_nhdsWithin

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem concat_eq_reverse_cons (a : α) (l : List α) : concat l a = reverse (a :: reverse l)

Proof state:
α : Type u
a : α
l : List α
⊢ l.concat a = (a :: l.reverse).reverse

Tactic:
simp only [concat_eq_append, reverse_cons, reverse_reverse]

Result:
no goals
-- Mathlib/NumberTheory/WellApproximable.lean
theorem mem_approxOrderOf_iff {A : Type*} [SeminormedGroup A] {n : ℕ} {δ : ℝ} {a : A} :
    a ∈ approxOrderOf A n δ ↔ ∃ b : A, orderOf b = n ∧ a ∈ ball b δ

Proof state:
A : Type u_1
inst✝ : SeminormedGroup A
n : ℕ
δ : ℝ
a : A
⊢ a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ ball b δ

Tactic:
simp only [approxOrderOf, thickening_eq_biUnion_ball, mem_iUnion₂, mem_setOf_eq, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem toSubmodule_injective : Function.Injective ((↑) : LieSubalgebra R L → Submodule R L) :=
  fun L₁' L₂' h ↦ by
  rw [SetLike.ext'_iff] at h
  rw [← coe_set_eq]
  exact h

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
rw [← coe_set_eq]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
rw [SetLike.ext'_iff] at h

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem underlyingIso_top_hom {B : C} : (underlyingIso (𝟙 B)).hom = (⊤ : Subobject B).arrow

Proof state:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
⊢ (underlyingIso (𝟙 B)).hom = (underlyingIso (𝟙 B)).hom ≫ 𝟙 B

Tactic:
simp only [comp_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
⊢ (underlyingIso (𝟙 B)).hom = ⊤.arrow

Tactic:
convert underlyingIso_hom_comp_eq_mk (𝟙 B)

Result:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
⊢ (underlyingIso (𝟙 B)).hom = (underlyingIso (𝟙 B)).hom ≫ 𝟙 B