harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem insert_toList_zoom {t : RBNode α} (ht : Balanced t c n)
    (e : zoom (cmp v) t = (t', p)) :
    (t.insert cmp v).toList = p.withList (t'.setRoot v).toList

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
p : Path α
v : α
t : RBNode α
ht : t.Balanced c n
e : zoom (cmp v) t = (t', p)
⊢ (insert cmp t v).toList = p.withList (setRoot v t').toList

Tactic:
rw [← setBlack_toList, ← Path.zoom_insert ht e, setBlack_toList, Path.insert_toList]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma antitone_of_le_sub_one : (∀ a, ¬ IsMin a → f a ≤ f (a - 1)) → Antitone f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a ≤ f (a - 1)) → Antitone f

Tactic:
simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem mvPolynomial (ι : Type*) [Finite ι] : FiniteType R (MvPolynomial ι R)

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
⊢ FiniteType R (MvPolynomial ι R)

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]

Result:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range MvPolynomial.X) = ⊤

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range MvPolynomial.X) = ⊤

Tactic:
exact MvPolynomial.adjoin_range_X

Result:
no goals

Proof state:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)

Tactic:
exact
  ⟨⟨Finset.univ.image MvPolynomial.X, by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact MvPolynomial.adjoin_range_X⟩⟩

Result:
no goals

Proof state:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)

Tactic:
classical
exact
  ⟨⟨Finset.univ.image MvPolynomial.X, by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact MvPolynomial.adjoin_range_X⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_eq_singleton_iff {s n a : Nat} : range' s n = #[a] ↔ s = a ∧ n = 1

Proof state:
s n a : Nat
⊢ (range' s n).toList = #[a].toList ↔ s = a ∧ n = 1

Tactic:
simp

Result:
no goals

Proof state:
s n a : Nat
⊢ range' s n = #[a] ↔ s = a ∧ n = 1

Tactic:
rw [← toList_inj]

Result:
s n a : Nat
⊢ (range' s n).toList = #[a].toList ↔ s = a ∧ n = 1
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
    ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x

Tactic:
simp only [← Finset.prod_apply]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => (∏ c ∈ t, f c) x) s x

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => (∏ c ∈ t, f c) x) s x

Tactic:
exact contMDiffWithinAt_finset_prod' h

Result:
no goals
-- Mathlib/Data/List/Palindrome.lean
theorem reverse_eq {l : List α} (p : Palindrome l) : reverse l = l

Proof state:
case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

Tactic:
(exact rfl)

Result:
no goals

Proof state:
case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
induction p <;> try (exact rfl)

Result:
case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])

Proof state:
case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_singleton (b : β) (f : β → α) : ∏' x : ({b} : Set β), f x = f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
b : β
f : β → α
⊢ ∏' (x : ↑{b}), f ↑x = f b

Tactic:
rw [← coe_singleton, Finset.tprod_subtype', prod_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_replicate (p : α → Bool) :
    (replicate n a).dropWhile p = if p a then [] else replicate n a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ dropWhile p (replicate n a) = if p a = true then [] else replicate n a

Tactic:
simp only [dropWhile_replicate_eq_filter_not, filter_replicate]

Result:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ (if (!p a) = true then replicate n a else []) = if p a = true then [] else replicate n a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ (if (!p a) = true then replicate n a else []) = if p a = true then [] else replicate n a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.rotateR {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateR l x r) :=
  Sized.dual_iff.1 <| by rw [dual_rotateR]; exact hr.dual.rotateL hl.dual

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized

Tactic:
exact hr.dual.rotateL hl.dual

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateR x r).dual.Sized

Tactic:
rw [dual_rotateR]

Result:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized
-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem Integrable.integral_eq_integral_meas_le
    (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
    ∫ ω, f ω ∂μ = ∫ t in Set.Ioi 0, ENNReal.toReal (μ {a : α | t ≤ f a})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal

Tactic:
apply integral_congr_ae

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ (fun a => (μ {a_1 | a < f a_1}).toReal) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => (μ {a_1 | a ≤ f a_1}).toReal

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal

Tactic:
rw [Integrable.integral_eq_integral_meas_lt f_intble f_nn]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ (fun a => (μ {a_1 | a < f a_1}).toReal) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => (μ {a_1 | a ≤ f a_1}).toReal

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ (μ {a | t < f a}).toReal = (μ {a | t ≤ f a}).toReal

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ (μ {a | t < f a}).toReal = (μ {a | t ≤ f a}).toReal

Tactic:
exact congrArg ENNReal.toReal ht.symm

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem P_f_idem (q n : ℕ) : ((P q).f n : X _⦋n⦌ ⟶ _) ≫ (P q).f n = (P q).f n

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)

Tactic:
exact (HigherFacesVanish.of_P q n).comp_P_eq_self

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f n ≫ (P q).f n = (P q).f n

Tactic:
rcases n with (_|n)

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 ≫ (P q).f 0 = (P q).f 0

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 ≫ (P q).f 0 = (P q).f 0

Tactic:
rw [P_f_0_eq q, comp_id]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
lemma IsUniform.cond {s : Set E} :
    IsUniform (id : E → E) s (ProbabilityTheory.cond μ s) μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
⊢ IsUniform id s (ProbabilityTheory.cond μ s) μ

Tactic:
unfold IsUniform

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
⊢ Measure.map id (ProbabilityTheory.cond μ s) = ProbabilityTheory.cond μ s

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
⊢ Measure.map id (ProbabilityTheory.cond μ s) = ProbabilityTheory.cond μ s

Tactic:
rw [Measure.map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α]
    {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew 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 (insertEntryIfNew k v l) = true
h₂ : (k == a) = false
⊢ containsKey a l = true

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

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_prime_mul_X_sub_one (R : Type*) [Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)] :
    cyclotomic p R * (X - 1) = X ^ p - 1

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic p R * (X - 1) = X ^ p - 1

Tactic:
rw [cyclotomic_prime, geom_sum_mul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem dist_div_sin_oangle_eq_two_mul_radius {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) :
    dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| = 2 * s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius

Tactic:
rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃,
  mul_div_cancel₀ _ (two_ne_zero' ℝ)]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDeriv_zero_fun {n : ℕ} : (iteratedFDeriv 𝕜 n fun _ : E ↦ (0 : F)) = 0 :=
  funext fun x ↦ by simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_zero_fun]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : E
⊢ iteratedFDeriv 𝕜 n (fun x => 0) x = 0 x

Tactic:
simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_zero_fun]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem induce_self_verts : G'.induce G'.verts = G'

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝

Tactic:
constructor <;>
  simp +contextual only [induce_adj, imp_true_iff, and_true]

Result:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts

Proof state:
case verts.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce G'.verts).verts ↔ x✝ ∈ G'.verts

Tactic:
simp

Result:
no goals

Proof state:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts

Tactic:
exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce G'.verts = G'

Tactic:
ext

Result:
case verts.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce G'.verts).verts ↔ x✝ ∈ G'.verts

case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail?

Proof state:
α : Type u_1
l l' : List α
⊢ (l ++ l').tail? = (Option.map (fun x => x ++ l') l.tail?).or l'.tail?

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem inter_insert_of_not_mem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) :
    s₁ ∩ insert a s₂ = s₁ ∩ s₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
rw [inter_comm, insert_inter_of_not_mem h, inter_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem Fintype.linearIndependent_iffₛ [Fintype ι] :
    LinearIndependent R v ↔ ∀ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i → ∀ i, f i = g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i : ι, f i • v i = ∑ i : ι, g i • v i → ∀ (i : ι), f i = g i

Tactic:
simp_rw [Fintype.linearIndependent_iff_injective,
  Injective, Fintype.linearCombination_apply, funext_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem Presieve.in_coverByImage (G : C ⥤ D) {X : D} {Y : C} (f : G.obj Y ⟶ X) :
    Presieve.coverByImage G X f :=
  ⟨⟨Y, 𝟙 _, f, by simp⟩⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
X : D
Y : C
f : G.obj Y ⟶ X
⊢ 𝟙 (G.obj Y) ≫ f = f

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem of_equiv_symm_iff {β} (e : β ≃ α) {f : σ → α} :
    haveI := Primcodable.ofEquiv α e
    (Primrec fun a => e.symm (f a)) ↔ Primrec f :=
  letI := Primcodable.ofEquiv α e
  ⟨fun h => (of_equiv.comp h).of_eq fun a => by simp, of_equiv_symm.comp⟩

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → α
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a => e.symm (f a)
a : σ
⊢ e (e.symm (f a)) = f a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_iff_superpolynomialDecay_norm :
    SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖ :=
  (superpolynomialDecay_iff_norm_tendsto_zero l k f).trans (by simp [SuperpolynomialDecay])

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝ : NormedLinearOrderedField β
⊢ (∀ (n : ℕ), Tendsto (fun a => ‖k a ^ n * f a‖) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖

Tactic:
simp [SuperpolynomialDecay]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem inclusion_faithful {S T : Subgroupoid C} (h : S ≤ T) (s t : S.objs) :
    Function.Injective fun f : s ⟶ t => (inclusion h).map f := fun ⟨f, hf⟩ ⟨g, hg⟩ => by
  -- Porting note: was `...; simpa only [Subtype.mk_eq_mk] using id`
  dsimp only [inclusion]; rw [Subtype.mk_eq_mk, Subtype.mk_eq_mk]; exact id

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ f = g → f = g

Tactic:
exact id

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ ⟨f, ⋯⟩ = ⟨g, ⋯⟩ → ⟨f, hf⟩ = ⟨g, hg⟩

Tactic:
rw [Subtype.mk_eq_mk, Subtype.mk_eq_mk]

Result:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ f = g → f = g

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ (fun f => (inclusion h).map f) ⟨f, hf⟩ = (fun f => (inclusion h).map f) ⟨g, hg⟩ → ⟨f, hf⟩ = ⟨g, hg⟩

Tactic:
dsimp only [inclusion]

Result:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ ⟨f, ⋯⟩ = ⟨g, ⋯⟩ → ⟨f, hf⟩ = ⟨g, hg⟩
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions :
    L.mapArrow.EssSurj where
  mem_essImage f

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
f : Arrow D
⊢ L.mapArrow.essImage f

Tactic:
have := Localization.essSurj_mapArrow L.op W.op

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
f : Arrow D
this : L.op.mapArrow.EssSurj
⊢ L.mapArrow.essImage f

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
f : Arrow D
this : L.op.mapArrow.EssSurj
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨g, ⟨e⟩⟩ : ∃ (g : _), Nonempty (L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op) :=
  ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
f : Arrow D
this : L.op.mapArrow.EssSurj
g : Arrow Cᵒᵖ
e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op
⊢ L.mapArrow.essImage f

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
f : Arrow D
this : L.op.mapArrow.EssSurj
g : Arrow Cᵒᵖ
e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op
⊢ L.mapArrow.essImage f

Tactic:
exact ⟨Arrow.mk g.hom.unop, ⟨Arrow.isoMk (Arrow.rightFunc.mapIso e.symm).unop
  (Arrow.leftFunc.mapIso e.symm).unop (Quiver.Hom.op_inj e.inv.w.symm)⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.containsThenInsert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) :
    (m.containsThenInsert a b).2.WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
b : β a
h : m.WF
⊢ (m.containsThenInsert a b).snd.WF

Tactic:
simpa [Raw.containsThenInsert, h.size_buckets_pos] using .containsThenInsert₀ h

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ico (a b : α) {c : α} (h : 0 < c) :
    (c * ·) ⁻¹' Ico a b = Ico (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => c * x) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iio, h]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma SMulPosStrictMono.lift [SMulPosStrictMono α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b)
    (zero : f 0 = 0) : SMulPosStrictMono α β where
  elim b hb a₁ a₂ ha

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : α → β → True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b

Tactic:
exact smul_lt_smul_of_pos_right ha hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • b < a₂ • b

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : α → β → True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_le_add_right {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k

Proof state:
n m : Nat
h : n ≤ m
k : Nat
⊢ k + n ≤ k + m

Tactic:
apply Nat.add_le_add_left

Result:
case h
n m : Nat
h : n ≤ m
k : Nat
⊢ n ≤ m

Proof state:
case h
n m : Nat
h : n ≤ m
k : Nat
⊢ n ≤ m

Tactic:
assumption

Result:
no goals

Proof state:
n m : Nat
h : n ≤ m
k : Nat
⊢ n + k ≤ m + k

Tactic:
rw [Nat.add_comm n k, Nat.add_comm m k]

Result:
n m : Nat
h : n ≤ m
k : Nat
⊢ k + n ≤ k + m