harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
theorem contMDiffOn_iff_contDiffOn {f : E → E'} {s : Set E} :
    ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f s ↔ ContDiffOn 𝕜 n f s :=
  forall_congr' <| by simp [contMDiffWithinAt_iff_contDiffWithinAt]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
⊢ ∀ (a : E), a ∈ s → ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s a ↔ a ∈ s → ContDiffWithinAt 𝕜 n f s a

Tactic:
simp [contMDiffWithinAt_iff_contDiffWithinAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_alter {k k' : α} (h : m.1.WF) [Inhabited β] {f : Option β → Option β} :
    Const.get! (Const.alter m k f) k' =
      if k == k' then
        (f (Const.get? m k)).get!
      else
        Const.get! m k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
k k' : α
h : m.val.WF
inst✝ : Inhabited β
f : Option β → Option β
⊢ get! (alter m k f) k' = if (k == k') = true then (f (get? m k)).get! else get! m k'

Tactic:
simp_to_model [Const.alter] using List.Const.getValue!_alterKey

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem reverse_ι (m : M) : reverse (ι Q m) = ι 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
m : M
⊢ reverse ((ι Q) m) = (ι Q) m

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma acyclic_iff :
    K.Acyclic ↔ ∀ i, K.ExactAt i

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
⊢ K.Acyclic ↔ ∀ (i : ι), K.ExactAt i

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem decay_smul_aux (k n : ℕ) (f : 𝓢(E, F)) (c : 𝕜) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • (f : E → F)) x‖ =
      ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

Tactic:
rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
  norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]

Result:
no goals
-- Mathlib/Tactic/Qify.lean
@[qify_simps] lemma intCast_eq (a b : ℤ) : a = b ↔ (a : ℚ) = (b : ℚ)

Proof state:
a b : ℤ
⊢ a = b ↔ ↑a = ↑b

Tactic:
simp only [Int.cast_inj]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_bot (hh : Monotone h) : (⊥ : Filter α).lift' h = 𝓟 (h ∅)

Proof state:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ ⊥.lift' h = 𝓟 (h ∅)

Tactic:
rw [← principal_empty, lift'_principal hh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) :
    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
L : List (List α)
⊢ foldr f b L.flatten = foldr (fun l b => foldr f b l) b L

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasDerivAt.inner {f g : ℝ → E} {f' g' : E} {x : ℝ} :
    HasDerivAt f f' x → HasDerivAt g g' x →
      HasDerivAt (fun t => ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
f' g' : E
x : ℝ
⊢ HasDerivAt f f' x →
    HasDerivAt g g' x → HasDerivAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) x

Tactic:
simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem of_intCast [AddGroupWithOne α] (n : ℤ) : ((n : ZNum) : α) = n

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑n = ↑n

Tactic:
rw [← cast_to_int, to_of_int]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem C_mul_X_eq_monomial : C a * X = monomial 1 a

Proof state:
R : Type u
a : R
inst✝ : Semiring R
⊢ C a * X = (monomial 1) a

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem leftCoset_rightCoset (s : Set α) (a b : α) : op b • a • s = a • (op b • s)

Proof state:
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ op b • a • s = a • op b • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
nonrec lemma StrongConcaveOn.mono (hmn : m ≤ n) (hf : StrongConcaveOn s n f) :
    StrongConcaveOn s m f := hf.mono fun r ↦ by gcongr

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
m n : ℝ
hmn : m ≤ n
hf : StrongConcaveOn s n f
r : ℝ
⊢ m / 2 * r ^ 2 ≤ n / 2 * r ^ 2

Tactic:
gcongr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem addPos_addNeg_eq_both (assignment : Assignment) :
    addPosAssignment (addNegAssignment assignment) = both

Proof state:
assignment : Assignment
⊢ assignment.addNegAssignment.addPosAssignment = both

Tactic:
cases assignment <;> simp [addPosAssignment, addNegAssignment]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
@[simp]
lemma IsPerfectMatching.toSubgraph_iff (h : M.spanningCoe ≤ G') :
    (G'.toSubgraph M.spanningCoe h).IsPerfectMatching ↔ M.IsPerfectMatching

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.spanningCoe ≤ G'
⊢ (toSubgraph M.spanningCoe h).IsPerfectMatching ↔ M.IsPerfectMatching

Tactic:
simp only [isPerfectMatching_iff, toSubgraph_adj, spanningCoe_adj]

Result:
no goals
-- Mathlib/Tactic/Push.lean
theorem ne_empty_eq_nonempty (s : Set β) : (s ≠ ∅) = s.Nonempty

Proof state:
β : Type u_2
s : Set β
⊢ (s ≠ ∅) = s.Nonempty

Tactic:
rw [ne_eq, ← not_nonempty_eq s, not_not]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem IsFormalAdjoint.symm (h : T.IsFormalAdjoint S) :
    S.IsFormalAdjoint T := fun y _ => by
  rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
h : T.IsFormalAdjoint S
y : ↥S.domain
x✝ : ↥T.domain
⊢ inner (↑S y) ↑x✝ = inner (↑y) (↑T x✝)

Tactic:
rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ]
    {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    (μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ a in s, κ a t ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ

Tactic:
simp [compProd, Kernel.compProd_apply_prod hs ht]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma small_of_hasSmallLocalizedHom [HasSmallLocalizedHom.{w} W X Y] :
    Small.{w} (L.obj X ⟶ L.obj Y)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
rwa [← hasSmallLocalizedHom_iff W]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_eq_natDegree {q : S[X]} (hpq : p.degree = q.degree) :
    p.natDegree = q.natDegree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hpq : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
simp [natDegree, hpq]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_eq_image (x y : E) :
    [x -[𝕜] y] = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Icc (0 : 𝕜) 1 :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
      ⟨b, ⟨hb, hab ▸ le_add_of_nonneg_left ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
      fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_nonneg.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y x✝¹ : E
x✝ : x✝¹ ∈ [x-[𝕜]y]
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = x✝¹
⊢ (fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

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 (α × β)} {k fallback : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (insertMany m l).getKeyD k fallback = m.getKeyD k fallback

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

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_lTensor_injective :
    Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective (I.subtype.lTensor M)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lTensor M (Submodule.subtype I))

Tactic:
simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_append_iff {f : α → β} :
    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
l : Array α
L₁ L₂ : Array β
f : α → β
⊢ map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rw [← filterMap_eq_map, filterMap_eq_append_iff]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem Int.erdos_ginzburg_ziv_prime (a : ι → ℤ) (hs : #s = 2 * p - 1) :
    ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Proof state:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ℤ
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Tactic:
simpa [← Int.cast_sum, ZMod.intCast_zmod_eq_zero_iff_dvd]
  using ZMod.erdos_ginzburg_ziv_prime (Int.cast ∘ a) hs

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Monovary.sum_smul_comp_perm_eq_sum_smul_iff (hfg : Monovary f g) :
    ∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Monovary f (g ∘ σ)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Monovary f (g ∘ ⇑σ)

Tactic:
simp [(hfg.monovaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_fst_darts_append {u v : V} (p : G.Walk u v) :
    p.darts.map (·.fst) ++ [v] = p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x => x.toProd.1) p.darts ++ [v] = p.support

Tactic:
induction p <;> simp! [*]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem bddBelow_bddAbove_iff_subset_Icc : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b

Tactic:
simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici,
  bddAbove_iff_subset_Iic, exists_and_left, exists_and_right]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Sbtw.oangle_eq_add_pi_right
    {p₁ p₂ p₃ p₃' : P} (h : Sbtw ℝ p₃ p₂ p₃') (hp₁p₂ : p₁ ≠ p₂) :
    ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + π

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)
p₁ p₂ p₃ p₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ↑π

Tactic:
rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_div_cancel (h : IsUnit a) : a / (a / b) = b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / (a / b) = b

Tactic:
rw [div_div_eq_mul_div, h.mul_div_cancel_left]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem frequently_atTop : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b ≥ a, p b :=
  atTop_basis.frequently_iff.trans <| by simp

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
p : α → Prop
inst✝ : Nonempty α
⊢ (∀ (i : α), True → ∃ x ∈ Ici i, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
lemma swap_mul_of_ne {i j a : n} {b : m} (hai : a ≠ i) (haj : a ≠ j) (g : Matrix n m R) :
    (swap R i j * g) a b = g a b

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 a : n
b : m
hai : a ≠ i
haj : a ≠ j
g : Matrix n m R
⊢ (swap R i j * g) a b = g a b

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mul, Equiv.swap_apply_of_ne_of_ne hai haj]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma mem_orbit_symm {a₁ a₂ : α} : a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
simp_rw [← orbit_eq_iff, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem decide_exists_mem {l : List α} {p : α → Prop} [DecidablePred p] :
    decide (∃ x, x ∈ l ∧ p x) = l.any p

Proof state:
α : Type u_1
l : List α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, x ∈ l ∧ p x) = l.any fun b => decide (p b)

Tactic:
simp [any_eq]

Result:
no goals
-- Mathlib/Algebra/Lie/Rank.lean
lemma rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] :
    rank R L = (polyCharpoly (ad R L).toLinearMap b).natTrailingDegree

Proof state:
R : Type u_1
L : Type u_3
ι : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : Module.Finite R L
inst✝³ : Module.Free R L
inst✝² : Fintype ι
b : Basis ι R L
inst✝¹ : Nontrivial R
inst✝ : DecidableEq ι
⊢ rank R L = ((↑(ad R L)).polyCharpoly b).natTrailingDegree

Tactic:
apply nilRank_eq_polyCharpoly_natTrailingDegree

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_castSucc_of_lt (p i : Fin n) (h : p < i) (hi := castSucc_ne_zero_of_lt h) :
    p.predAbove (castSucc i) = i.castSucc.pred hi

Proof state:
n : ℕ
p i : Fin n
h : p < i
hi : optParam (i.castSucc ≠ 0) ⋯
⊢ p.predAbove i.castSucc = i.castSucc.pred hi

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_le_add {f : α → ℝ} (h : ∀ x y, f x ≤ f y + dist x y) : LipschitzWith 1 f :=
  LipschitzWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
h : ∀ (x y : α), f x ≤ f y + dist x y
⊢ ∀ (x y : α), f x ≤ f y + ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean
theorem contsAux_recurrence {gp ppred pred : Pair K} (nth_s_eq : g.s.get? n = some gp)
    (nth_contsAux_eq : g.contsAux n = ppred)
    (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) :
    g.contsAux (n + 2) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
simp [*, contsAux, nextConts, nextDen, nextNum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
    k' ∈ Const.modify m k f ↔ k' ∈ m

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ k' ∈ modify m k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_modify h]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsConj.symm (hσ : IsConj φ σ) :
    IsConj φ σ.symm := RingHom.ext fun x ↦ by simpa using congr_arg star (hσ.eq (σ.symm x))

Proof state:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
hσ : IsConj φ σ
x : K
⊢ (conjugate φ) x = (φ.comp ↑σ.symm) x

Tactic:
simpa using congr_arg star (hσ.eq (σ.symm x))

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_castPred_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
    j ≤ castPred i hi ↔ castSucc j ≤ i

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Int.lean
theorem toNat_add_toNat_neg_eq_norm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖

Proof state:
n : ℤ
⊢ ↑n.toNat + ↑(-n).toNat = ‖n‖

Tactic:
simpa only [NNReal.coe_natCast, NNReal.coe_add] using
  congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
/-- If the indicator functions of measurable sets `Aᵢ` converge to the indicator function of
a set `A` along a nontrivial countably generated filter, then `A` is also measurable. -/
lemma measurableSet_of_tendsto_indicator [NeBot L] (As_mble : ∀ i, MeasurableSet (As i))
    (h_lim : ∀ x, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) :
    MeasurableSet A

Proof state:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ MeasurableSet A

Tactic:
simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢

Result:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), Measurable ((As i).indicator fun x => 1)
⊢ Measurable (A.indicator fun x => 1)

Proof state:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), Measurable ((As i).indicator fun x => 1)
⊢ Measurable (A.indicator fun x => 1)

Tactic:
exact ENNReal.measurable_of_tendsto' L As_mble
  ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENat_ne_top {a : Cardinal} : toENat a ≠ ⊤ ↔ a < ℵ₀

Proof state:
a : Cardinal.{u_1}
⊢ toENat a ≠ ⊤ ↔ a < ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma of_le {κ' : Cardinal.{v}} (hκ' : κ ≤ κ') :
    HasCardinalLT X κ' :=
  lt_of_lt_of_le h (by simpa only [Cardinal.lift_le] using hκ')

Proof state:
X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
κ' : Cardinal.{v}
hκ' : κ ≤ κ'
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ'

Tactic:
simpa only [Cardinal.lift_le] using hκ'

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_iInf_eq {f : ι → Filter α} {m : α → β} (hf : Directed (· ≥ ·) f) [Nonempty ι] :
    map m (iInf f) = ⨅ i, map m (f i) :=
  map_iInf_le.antisymm fun s (hs : m ⁻¹' s ∈ iInf f) =>
    let ⟨i, hi⟩ := (mem_iInf_of_directed hf _).1 hs
    have : ⨅ i, map m (f i) ≤ 𝓟 s :=
      iInf_le_of_le i <| by simpa only [le_principal_iff, mem_map]
    Filter.le_principal_iff.1 this

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → Filter α
m : α → β
hf : Directed (fun x1 x2 => x1 ≥ x2) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ map m (f i) ≤ 𝓟 s

Tactic:
simpa only [le_principal_iff, mem_map]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S k] (a : S) (b : G →₀ k) :
    (⟨a • b⟩ : SkewMonoidAlgebra k G) = (a • ⟨b⟩ : SkewMonoidAlgebra k G) :=
  show _ = smul _ _ by rw [smul]

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
a : S
b : G →₀ k
⊢ { toFinsupp := a • b } = SkewMonoidAlgebra.smul a { toFinsupp := b }

Tactic:
rw [smul]

Result:
no goals
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem nullhomotopic_of_constant (y : Y) : Nullhomotopic (ContinuousMap.const X y) :=
  ⟨y, by rfl⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ (const X y).Homotopic (const X y)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
@[simp] lemma directLimitRight_symm_of_tmul {i : ι} (m : M) (g : G i) :
    (directLimitRight f M).symm (of _ _ _ _ _ (m ⊗ₜ g)) = m ⊗ₜ of _ _ _ f _ g

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
g : G i
⊢ (directLimitRight f M).symm
      ((of R ι (fun x => M ⊗[R] G x) (fun i j h => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)) =
    m ⊗ₜ[R] (of R ι G f i) g

Tactic:
simp [directLimitRight, congr_symm_apply_of]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem le_iff (a b : ℚ) : a ≤ b ↔ a.num * b.den ≤ b.num * a.den

Proof state:
a b : ℚ
⊢ a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den

Tactic:
simpa only [Rat.not_lt, not_lt] using (Rat.lt_iff b a).not

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setAverage_congr_fun (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
    ⨍ x in s, f x ∂μ = ⨍ x in s, g x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
s : Set α
f g : α → E
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in s, g x ∂μ

Tactic:
simp only [average_eq, setIntegral_congr_ae hs h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem le_logb_iff_rpow_le (hy : 0 < y) : x ≤ logb b y ↔ b ^ x ≤ y

Proof state:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x ≤ logb b y ↔ b ^ x ≤ y

Tactic:
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_eq_get! [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] {h} :
    m.get a h = m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h✝ : m.val.WF
a : α
inst✝ : Inhabited (β a)
h : m.contains a = true
⊢ m.get a h = m.get! a

Tactic:
simp_to_model using List.getValueCast_eq_getValueCast!

Result:
no goals