harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma zero_sub (t : Multiset α) : 0 - t = 0 :=
  Multiset.induction_on t rfl fun a s ih => by simp [ih]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
ih : 0 - s = 0
⊢ 0 - a ::ₘ s = 0

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
lemma exists_mem_image {p : β → Prop} : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
⊢ (∃ y ∈ image f s, p y) ↔ ∃ x ∈ s, p (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem one_lt_prod (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) : 1 < ∏ i ∈ s, f i :=
  lt_of_le_of_lt (by rw [prod_const_one]) <| prod_lt_prod_of_nonempty' hs h

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s : Finset ι
h : ∀ i ∈ s, 1 < f i
hs : s.Nonempty
⊢ 1 ≤ ∏ i ∈ s, 1

Tactic:
rw [prod_const_one]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldl_prod_map_ι (l : List M) (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) :
    foldl Q f hf n (l.map <| ι Q).prod = List.foldl (fun m n => f n m) n l

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldl Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldl (fun m n => (f n) m) n l

Tactic:
rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ [a]), p x) ↔ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
⊢ (∀ (x : α), x ∈ [a] → p x) ↔ p a

Tactic:
simp only [mem_singleton, forall_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
@[simp]
lemma charpoly_fromBlocks_zero₂₁ :
    (fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = (M₁₁.charpoly * M₂₂.charpoly)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly

Tactic:
simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero,
  det_fromBlocks_zero₂₁]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem bddBelow_insert [IsDirected α (· ≥ ·)] {s : Set α} {a : α} :
    BddBelow (insert a s) ↔ BddBelow s

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
s : Set α
a : α
⊢ BddBelow (insert a s) ↔ BddBelow s

Tactic:
simp only [insert_eq, bddBelow_union, bddBelow_singleton, true_and]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive]
lemma HasCompactMulSupport.exists_bound_of_continuous [TopologicalSpace α]
    {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) : ∃ C, ∀ x, ‖f x‖ ≤ C

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : SeminormedGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_map {f : α → β} {l : Vector α n} {P : β → Prop} :
    (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
P : β → Prop
⊢ (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem and_elim_right : ∀ {a b : Bool}, a && b → b

Proof state:
⊢ ∀ {a b : Bool}, (a && b) = true → b = true

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_left' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (g : α → ℝ≥0∞) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral_congr_ae hf.ae_eq_mk, ← lintegral_add_left hf.measurable_mk,
  lintegral_congr_ae (hf.ae_eq_mk.add (ae_eq_refl g))]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_ne_zero [Nontrivial R] : (X : R[X]) ≠ 0 :=
  mt (congr_arg fun p => coeff p 1) (by simp)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertManyIfNewUnit_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit m l) k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
l : List α
k : α
fallback : Unit
⊢ getD (insertManyIfNewUnit m l) k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem isOpen_iff_generate_intervals [t : OrderTopology α] {s : Set α} :
    IsOpen s ↔ GenerateOpen { s | ∃ a, s = Ioi a ∨ s = Iio a } s

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l

Proof state:
α : Type u
a : α
n : Nat
l : List α
⊢ (insertIdx n a l).eraseIdx n = l

Tactic:
rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]

Result:
α : Type u
a : α
n : Nat
l : List α
⊢ modifyTailIdx (tail ∘ cons a) n l = l

Proof state:
α : Type u
a : α
n : Nat
l : List α
⊢ modifyTailIdx (tail ∘ cons a) n l = l

Tactic:
exact modifyTailIdx_id _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem tan_int_mul_pi_div_two (n : ℤ) : tan (n * π / 2) = 0 :=
  tan_eq_zero_iff.mpr (by use n)

Proof state:
n : ℤ
⊢ ∃ k, ↑k * π / 2 = ↑n * π / 2

Tactic:
use n

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
/-- The assignment `x ↦ dirac x` is injective, assuming the measurable space separates points. -/
lemma injective_dirac [SeparatesPoints α] :
    Function.Injective (fun (x : α) ↦ dirac x) := fun x y x_ne_y ↦ by rwa [← dirac_eq_dirac_iff]

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : (fun x => dirac x) x = (fun x => dirac x) y
⊢ x = y

Tactic:
rwa [← dirac_eq_dirac_iff]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem compl_sUnion (S : Set (Set α)) : (⋃₀ S)ᶜ = ⋂₀ (compl '' S) :=
  ext fun x => by simp

Proof state:
α : Type u_1
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem measure_preimage_emb {f : α → β} (hf : MeasurePreserving f μa μb)
    (hfe : MeasurableEmbedding f) (s : Set β) : μa (f ⁻¹' s) = μb s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
hfe : MeasurableEmbedding f
s : Set β
⊢ μa (f ⁻¹' s) = μb s

Tactic:
rw [← hf.map_eq, hfe.map_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_zero_right (y : M) : polar Q y 0 = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
y : M
⊢ polar (⇑Q) y 0 = 0

Tactic:
simp only [add_zero, polar, QuadraticMap.map_zero, sub_self]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
lemma apply_inl (h : l.idxFun i = Sum.inl a) : l x i = a

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
a : α
h : l.idxFun i = Sum.inl a
⊢ ↑l x i = a

Tactic:
simp [apply_def, h]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem uniformSpace_eq [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
    instUniformSpace σ F 𝔖 =
      UniformSpace.comap (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)
        (UniformOnFun.uniformSpace E F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ instUniformSpace σ F 𝔖 = UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)

Tactic:
rw [instUniformSpace, UniformSpace.replaceTopology_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem erase_zero (n : ℕ) : (0 : R[X]).erase n = 0 :=
  toFinsupp_injective <| by simp

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (erase n 0).toFinsupp = toFinsupp 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_diff_Ioi : Ioi a \ Ioi b = Ioc a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ioi b = Ioc a b

Tactic:
rw [diff_eq, compl_Ioi, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_iInf {ι : Type*} [Finite ι] (u : ι → ℕ → ℝ≥0∞) :
    expGrowthInf (⨅ i, u i) = ⨅ i, expGrowthInf (u i)

Proof state:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthInf (⨅ i, u i) = ⨅ i, expGrowthInf (u i)

Tactic:
rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma lt_succ_sqrt' (n : ℕ) : n < succ (sqrt n) ^ 2

Proof state:
n : ℕ
⊢ n < n.sqrt.succ ^ 2

Tactic:
simpa [Nat.pow_two] using lt_succ_sqrt n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_range : (Vector.range n).toList = List.range n

Proof state:
n : Nat
⊢ (range n).toList = List.range n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_right_eq_self : a * b = a ↔ b = 1 := calc
  a * b = a ↔ a * b = a * 1

Proof state:
M : Type u_4
inst✝ : LeftCancelMonoid M
a b : M
⊢ a * b = a ↔ a * b = a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union_add_inter₀ (s : Set α) (ht : NullMeasurableSet t μ) :
    μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
rw [← restrict_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
  restrict_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- Strictly monotone functions preserve the colex ordering. -/
lemma toColex_image_le_toColex_image (hf : StrictMono f) :
    toColex (s.image f) ≤ toColex (t.image f) ↔ toColex s ≤ toColex t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s t : Finset α
hf : StrictMono f
⊢ { ofColex := image f s } ≤ { ofColex := image f t } ↔ { ofColex := s } ≤ { ofColex := t }

Tactic:
simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem add_lt_add_iff_left {x y z : PartENat} (hz : z ≠ ⊤) : z + x < z + y ↔ x < y

Proof state:
x y z : PartENat
hz : z ≠ ⊤
⊢ z + x < z + y ↔ x < y

Tactic:
rw [add_comm z, add_comm z, PartENat.add_lt_add_iff_right hz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} {k fallback : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k fallback : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_source_of_mem_source
    [IsManifold I n M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
    ContMDiffAt I I' n f x' ↔
      ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (extChartAt I x).symm) (range I) (extChartAt I x 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
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x' : M
hx' : x' ∈ (chartAt H x).source
⊢ ContMDiffAt I I' n f x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
simp_rw [ContMDiffAt, contMDiffWithinAt_iff_source_of_mem_source hx', preimage_univ, univ_inter]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/ModEq.lean
theorem frequently_mod_eq {d n : ℕ} (h : d < n) : ∃ᶠ m in atTop, m % n = d

Proof state:
d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d

Tactic:
simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem imp_false_eq (p : Prop) : (p → False) = ¬p

Proof state:
p : Prop
⊢ (p → False) = ¬p

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem DirectSum.IsInternal.collectedOrthonormalBasis_mem [DecidableEq ι]
    (h : DirectSum.IsInternal A) {α : ι → Type*} [∀ i, Fintype (α i)]
    (hV : OrthogonalFamily 𝕜 (fun i => A i) fun i => (A i).subtypeₗᵢ)
    (v : ∀ i, OrthonormalBasis (α i) 𝕜 (A i)) (a : Σi, α i) :
    h.collectedOrthonormalBasis hV v a ∈ A a.1

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
A : ι → Submodule 𝕜 E
inst✝¹ : DecidableEq ι
h : IsInternal A
α : ι → Type u_7
inst✝ : (i : ι) → Fintype (α i)
hV : OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ
v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)
a : (i : ι) × α i
⊢ (collectedOrthonormalBasis hV h v) a ∈ A a.fst

Tactic:
simp [DirectSum.IsInternal.collectedOrthonormalBasis]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem sup_principal {s t : Set α} : 𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t) :=
  Filter.ext fun u => by simp only [union_subset_iff, mem_sup, mem_principal]

Proof state:
α : Type u
s t u : Set α
⊢ u ∈ 𝓟 s ⊔ 𝓟 t ↔ u ∈ 𝓟 (s ∪ t)

Tactic:
simp only [union_subset_iff, mem_sup, mem_principal]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] protected lemma LinearOrder.infClosed (s : Set α) : InfClosed s :=
  fun a ha b hb ↦ by cases le_total a b <;> simp [*]

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a ⊓ b ∈ s

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

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem fderiv_norm_smul_pos (ht : 0 < t) :
    fderiv ℝ (‖·‖) (t • x) = fderiv ℝ (‖·‖) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
ht : 0 < t
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = fderiv ℝ (fun x => ‖x‖) x

Tactic:
simp [fderiv_norm_smul, ht]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b)

Proof state:
⊢ ∀ (a b : Bool), (a || b) = !(!a && !b)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertEntry [BEq α] [PartialEquivBEq α]
    {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntry k v l))
    (h₂ : (k == a) = false) : containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntry k v l) = true
h₂ : (k == a) = false
⊢ containsKey a l = true

Tactic:
rwa [containsKey_insertEntry, h₂, Bool.false_or] at h₁

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/BaseChange.lean
@[simp] lemma restrictScalars_toPerfectPairing_apply_apply
    (x : span K (range P.root)) (y : span K (range P.coroot)) :
    algebraMap K L ((P.restrictScalars' K hP).toPerfectPairing x y) = P.toPerfectPairing x y

Proof state:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Field L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module L M
inst✝⁷ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : Algebra K L
inst✝⁴ : Module K M
inst✝³ : Module K N
inst✝² : IsScalarTower K L M
inst✝¹ : IsScalarTower K L N
inst✝ : P.IsBalanced
hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range
x : ↥(span K (range ⇑P.root))
y : ↥(span K (range ⇑P.coroot))
⊢ (algebraMap K L) (((P.restrictScalars' K hP).toPerfectPairing x) y) = (P.toPerfectPairing ↑x) ↑y

Tactic:
simp [restrictScalars']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem lhs_get_cast {aig1 aig2 : AIG α} (s : BinaryRefVec aig1 len) (idx : Nat)
    (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).lhs.get idx hidx
      =
    (s.lhs.get idx hidx).cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig1 aig2 : AIG α
s : aig1.BinaryRefVec len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).lhs.get idx hidx = (s.lhs.get idx hidx).cast hcast

Tactic:
simp [cast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_nonsingular (hf : Function.Injective f) (P : Fin 3 → R) :
    (W'.map f).toJacobian.Nonsingular (f ∘ P) ↔ W'.Nonsingular P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (map W' f).toJacobian.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

Tactic:
simp only [Nonsingular, map_equation hf, map_polynomialX, map_polynomialY, map_polynomialZ,
  eval_map, ← eval₂_comp, map_ne_zero_iff f hf]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
nonrec lemma ContDiffAt.contDiffOn (h : ContDiffAt 𝕜 n f x) (hm : m ≤ n) (h' : m = ∞ → n = ω):
    ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 m f u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
m n : WithTop ℕ∞
h : ContDiffAt 𝕜 n f x
hm : m ≤ n
h' : m = ∞ → n = ω
⊢ ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 m f u

Tactic:
simpa [nhdsWithin_univ] using h.contDiffOn hm h'

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousOn_iff' [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff']

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_eq_of_basis [DecidableEq ιM] (bₘ : Basis ιM R M) :
    polyCharpoly φ b =
    (charpoly.univ R ιM).map (MvPolynomial.bind₁ (φ.toMvPolynomial b bₘ.end))

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpoly b = Polynomial.map (↑(MvPolynomial.bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)

Tactic:
rw [polyCharpoly, φ.polyCharpolyAux_basisIndep b (Module.Free.chooseBasis R M) bₘ,
  polyCharpolyAux]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Additive.lean
lemma right_adjoint_additive [F.Additive] : G.Additive where
  map_add {X Y} f g := (adj.homEquiv _ _).symm.injective (by simp [homEquiv_counit])

Proof state:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X Y : D
f g : X ⟶ Y
⊢ (adj.homEquiv (G.obj X) Y).symm (G.map (f + g)) = (adj.homEquiv (G.obj X) Y).symm (G.map f + G.map g)

Tactic:
simp [homEquiv_counit]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Units.lean
@[to_additive]
lemma mem_ofUnits_iff_toUnits_mem (H : Subgroup Gˣ) (x : G) : x ∈ H.ofUnits ↔ (toUnits x) ∈ H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : G
⊢ x ∈ H.ofUnits ↔ toUnits x ∈ H

Tactic:
simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_one' (h : y - 1 ≠ 0) (x : ℝ≥0) : x ^ (y - 1) = x ^ y / x

Proof state:
y : ℝ
h : y - 1 ≠ 0
x : ℝ≥0
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
rw [rpow_sub' h, rpow_one]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma extendToSucc_obj_succ_eq :
    (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ = X :=
  extendToSucc.obj_succ_eq hj F X

Proof state:
C : Type u_1
inst✝² : Category.{?u.62050, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ Order.succ j ∈ Set.Iic (Order.succ j)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem comp_ι_sq_scalar (g : CliffordAlgebra Q →ₐ[R] A) (m : M) :
    g (ι Q m) * g (ι Q m) = algebraMap _ _ (Q m)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ g ((ι Q) m) * g ((ι Q) m) = (algebraMap R A) (Q m)

Tactic:
rw [← map_mul, ι_sq_scalar, AlgHom.commutes]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_alterKey {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} :
    (alterKey k f l).isEmpty = ((l.isEmpty || (l.length == 1 && containsKey k l)) &&
      (f (getValueCast? k l)).isNone)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (alterKey k f l).isEmpty = ((l.isEmpty || l.length == 1 && containsKey k l) && (f (getValueCast? k l)).isNone)

Tactic:
rw [isEmpty_alterKey_eq_isEmpty_eraseKey, isEmpty_eraseKey]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem mem_nhds_iff {x : CofiniteTopology X} {s : Set (CofiniteTopology X)} :
    s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite

Proof state:
X : Type u
x : CofiniteTopology X
s : Set (CofiniteTopology X)
⊢ s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite

Tactic:
simp [nhds_eq]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma lt_untopD_iff (hy : y = ⊤ → a < b) : a < y.untopD b ↔ a < y

Proof state:
α : Type u_1
a b : α
inst✝ : LT α
y : WithTop α
hy : y = ⊤ → a < b
⊢ a < untopD b y ↔ ↑a < y

Tactic:
cases y <;> simp [hy]

Result:
no goals