harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Rat.lean
theorem _root_.Int.norm_cast_rat (m : ℤ) : ‖(m : ℚ)‖ = ‖m‖

Proof state:
m : ℤ
⊢ ‖↑m‖ = ‖m‖

Tactic:
rw [← Rat.norm_cast_real, ← Int.norm_cast_real]

Result:
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖

Proof state:
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖

Tactic:
congr 1

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

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
ι : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : Module.Finite R L
inst✝⁹ : Module.Free R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R M
inst✝² : Fintype ι
b : Basis ι R L
inst✝¹ : Nontrivial R
inst✝ : DecidableEq ι
⊢ rank R L M = ((↑(toEnd R L M)).polyCharpoly b).natTrailingDegree

Tactic:
apply nilRank_eq_polyCharpoly_natTrailingDegree

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem neg_conj_apply [AddGroup G] (g h : G) : (-conj g) h = -g + h + g

Proof state:
G : Type u_3
inst✝ : AddGroup G
g h : G
⊢ (Additive.toMul (-conj g)) h = -g + h + g

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited β]  (h : m.1.WF) {l : List (α × β)} {k : α}
    (h' : (l.map Prod.fst).contains k = false) :
    get! (insertMany m l).1 k = get! m k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
l : List (α × β)
k : α
h' : (List.map Prod.fst l).contains k = false
⊢ get! (insertMany m l).val k = get! m k

Tactic:
simp_to_model [Const.insertMany] using List.getValue!_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma mem_limsup_iff_frequently_mem : (a ∈ limsup s 𝓕) ↔ (∃ᶠ i in 𝓕, a ∈ s i)

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simp only [Filter.Frequently, iff_not_comm, ← mem_compl_iff, limsup_compl, comp_apply,
  mem_liminf_iff_eventually_mem]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
theorem pushoutCoconeOfRightIso_ι_app_none : (pushoutCoconeOfRightIso f g).ι.app none = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app none = f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma uIoc_of_ge (h : b ≤ a) : Ι a b = Ioc b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ι a b = Ioc b a

Tactic:
simp [uIoc, h]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
lemma norm_exp_le_exp_norm (x : ℂ) : ‖exp x‖ ≤ Real.exp ‖x‖

Proof state:
x : ℂ
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖

Tactic:
convert norm_exp_sub_sum_le_exp_norm_sub_sum x 0 using 1 <;> simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem inner_eq_mul_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) : ⟪x, y⟫ = ‖x‖ * ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ inner x y = ‖x‖ * ‖y‖

Tactic:
simp [← cos_angle_mul_norm_mul_norm, h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem abs_max_sub_max_le_abs (a b c : α) : |max a c - max b c| ≤ |a - b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a ⊔ c - b ⊔ c| ≤ |a - b|

Tactic:
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
  using abs_max_sub_max_le_max a c b c

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_eq_of_countable_range' (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω = i}

Tactic:
exact hτ.measurableSet_eq_of_countable_range h_countable i

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_right_eq_empty (ha : a ∉ s) : Prod.mk a ⁻¹' s ×ˢ t = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∉ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∉ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∉ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ ∅

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
lemma lipschitzWith_negPart : LipschitzWith 1 (negPart : α → α)

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ LipschitzWith 1 negPart

Tactic:
simpa [Function.comp] using lipschitzWith_posPart.comp LipschitzWith.id.neg

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isUpperSet_iff_Ioi_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s

Tactic:
simp [isUpperSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- An open set is everywhere positive for a measure which is positive on open sets. -/
lemma _root_.IsOpen.isEverywherePos [IsOpenPosMeasure μ] (hs : IsOpen s) : IsEverywherePos μ s

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
⊢ μ.IsEverywherePos s

Tactic:
intro x xs n hn

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < μ n

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
u : Set α
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ s ⊆ n
⊢ 0 < μ (u ∩ s)

Tactic:
exact (u_open.inter hs).measure_pos μ ⟨x, ⟨xu, xs⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < μ n

Tactic:
rcases mem_nhdsWithin.1 hn with ⟨u, u_open, xu, hu⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
u : Set α
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ s ⊆ n
⊢ 0 < μ n

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
u : Set α
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ s ⊆ n
⊢ 0 < μ n

Tactic:
apply lt_of_lt_of_le _ (measure_mono hu)

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
u : Set α
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ s ⊆ n
⊢ 0 < μ (u ∩ s)
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel'_kernelSubobjectIso (w : f ≫ g = 0) :
    imageToKernel' f g w ≫ (kernelSubobjectIso g).inv =
      (imageSubobjectIso f).inv ≫ imageToKernel f g w

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ (kernelSubobject g).arrow =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ (kernelSubobject g).arrow =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Tactic:
simp [imageToKernel']

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_self_apply (a) : trace R R a = a

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
⊢ (trace R R) a = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffOn_Ioc (a b : ℝ) : UniqueDiffOn ℝ (Ioc a b) :=
  if hab : a < b then
    uniqueDiffOn_convex (convex_Ioc a b) <| by simp only [interior_Ioc, nonempty_Ioo, hab]
  else by simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]

Proof state:
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ioc a b)

Tactic:
simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]

Result:
no goals

Proof state:
a b : ℝ
hab : a < b
⊢ (interior (Ioc a b)).Nonempty

Tactic:
simp only [interior_Ioc, nonempty_Ioo, hab]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma map_genWeightSpace_eq (e : M ≃ₗ⁅R,L⁆ M₂) :
    (genWeightSpace M χ).map e = genWeightSpace M₂ χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map e.toLieModuleHom (genWeightSpace M χ) = genWeightSpace M₂ χ

Tactic:
simp [map_genWeightSpace_eq_of_injective e.injective]

Result:
no goals
-- Mathlib/Data/List/SplitLengths.lean
theorem length_splitLengths_getElem_eq {i : ℕ} (hi : i < sz.length)
    (h : (sz.take (i + 1)).sum ≤ l.length) :
    ((sz.splitLengths l)[i]'(by simpa)).length = sz[i]

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ i < (sz.splitLengths l).length

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ ((take (i + 1) sz).splitLengths l)[i].length = sz[i]

Tactic:
conv_rhs =>
  rw [List.getElem_take' (hj := i.lt_add_one)]
  simp (config := {singlePass := true}) only [← map_splitLengths_length l _ h]
  rw [getElem_map]

Result:
no goals

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]

Result:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (take (i + 1) (sz.splitLengths l))[i].length = sz[i]

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (take (i + 1) (sz.splitLengths l))[i].length = sz[i]

Tactic:
simp only [take_splitLength]

Result:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ ((take (i + 1) sz).splitLengths l)[i].length = sz[i]
-- Mathlib/Data/Finset/Max.lean
theorem isGLB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i)
    (hs : s.Nonempty) : i ∈ s

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
rw [← mem_coe]

Result:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ ↑s

Proof state:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ ↑s

Tactic:
exact ((isGLB_iff_isLeast i s hs).mp his).1

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_sub_center_inv (c : ℂ) {R : ℝ} (hR : R ≠ 0) :
    (∮ z in C(c, R), (z - c)⁻¹) = 2 * π * I

Proof state:
c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑π * I

Tactic:
simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center hR),
  intervalIntegral.integral_const I]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp] lemma Dual.eval_comp_comp_evalEquiv_eq
    {M' : Type*} [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} :
    Dual.eval R M' ∘ₗ f ∘ₗ (evalEquiv R M).symm = f.dualMap.dualMap

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = f.dualMap.dualMap

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
  evalEquiv_toLinearMap, eval_naturality]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem subalgebra_top_rank_eq_submodule_top_rank :
    Module.rank F (⊤ : Subalgebra F E) = Module.rank F (⊤ : Submodule F E)

Proof state:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥(Subalgebra.toSubmodule ⊤)

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]

Result:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥(Subalgebra.toSubmodule ⊤)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c

Proof state:
case succ
a b c : Nat
ih : a - (b + c) = a - b - c
⊢ a - (b + (c + 1)) = a - b - (c + 1)

Tactic:
simp only [Nat.add_succ, Nat.sub_succ, ih]

Result:
no goals

Proof state:
a b c : Nat
⊢ a - (b + c) = a - b - c

Tactic:
induction c with
| zero => simp
| succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]

Result:
no goals

Proof state:
case zero
a b : Nat
⊢ a - (b + 0) = a - b - 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem toOuterMeasure_trim_eq_trim_toOuterMeasure (μ : Measure α) (hm : m ≤ m0) :
    @Measure.toOuterMeasure _ m (μ.trim hm) = @OuterMeasure.trim _ m μ.toOuterMeasure

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ (μ.trim hm).toOuterMeasure = μ.trim

Tactic:
rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]

Result:
no goals
-- Mathlib/RingTheory/Prime.lean
theorem Prime.abs [LinearOrder α] {p : α} (hp : Prime p) : Prime (abs p)

Proof state:
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
⊢ Prime |p|

Tactic:
obtain h | h := abs_choice p <;> rw [h]

Result:
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p

case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Proof state:
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p

Tactic:
exact hp

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Tactic:
exact hp.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = [] ↔ l = []

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = [] ↔ l = []

Tactic:
rw [mapFinIdx_eq_zipIdx_map, map_eq_nil_iff, attach_eq_nil_iff, zipIdx_eq_nil_iff]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@[simp]
lemma ofTensorProductEquivOfFiniteNoetherian_symm_of
    [Module.Finite R M] (x : M) :
    (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ x

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)
⊢ (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ[R] x

Tactic:
rw [h, LinearEquiv.symm_apply_apply]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
⊢ (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
⊢ (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ[R] x

Tactic:
have h : (of I M) x = ofTensorProductEquivOfFiniteNoetherian I M (1 ⊗ₜ x) := by
  simp

Result:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)
⊢ (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ[R] x
-- Mathlib/Topology/Order/OrderClosedExtr.lean
/-- If `f` is antitone on `(a,b]` and monotone on `[b,c)` then `f` has
a local minimum at `b`. -/
lemma isLocalMin_of_anti_mono
    {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
    {β : Type*} [Preorder β] {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β}
    (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) : IsLocalMin f b :=
  mem_of_superset (Ioo_mem_nhds g₀ g₁) (fun x hx => by rcases le_total x b <;> aesop)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
β : Type u_2
inst✝ : Preorder β
a b c : α
g₀ : a < b
g₁ : b < c
f : α → β
h₀ : AntitoneOn f (Ioc a b)
h₁ : MonotoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
⊢ x ∈ {x | (fun x => f b ≤ f x) x}

Tactic:
rcases le_total x b <;> aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_add_inv {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) :
    A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

Tactic:
simpa only [nonsing_inv_eq_ring_inverse] using Ring.inverse_add_inverse h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
  ⟨Nat.dvd_add h,
    match m, h with
    | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ =>
      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩

Proof state:
k m n : Nat
h : k ∣ m
d : Nat
x✝ : k ∣ k * d + n
e : Nat
he : k * d + n = k * e
⊢ n = k * (e - d)

Tactic:
rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_extendDomain (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e

Proof state:
α : Type u
inst✝⁴ : DecidableEq α
β : Type v
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
e : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ sign (e.extendDomain f) = sign e

Tactic:
simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem right_ne_zero_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : y ≠ 0 :=
  o.right_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Exterior.lean
theorem exterior_union (s t : Set X) : exterior (s ∪ t) = exterior s ∪ exterior t

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ exterior (s ∪ t) = exterior s ∪ exterior t

Tactic:
simp only [exterior, nhdsSet_union, ker_sup]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integrable_comp_mul_left_iff (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) :
    (Integrable fun x => g (R * x)) ↔ Integrable g

Proof state:
F : Type u_1
inst✝ : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ Integrable (fun x => g (R * x)) volume ↔ Integrable g volume

Tactic:
simpa only [smul_eq_mul] using integrable_comp_smul_iff volume g hR

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem eq_unbot_iff {a : α} {b : WithBot α} (h : b ≠ ⊥) :
    a = b.unbot h ↔ a = b

Proof state:
case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
b : WithBot α
h : b ≠ ⊥
⊢ a = b.unbot h ↔ ↑a = b

Tactic:
induction b

Result:
case bot
α : Type u_1
a : α
h : ⊥ ≠ ⊥
⊢ a = ⊥.unbot h ↔ ↑a = ⊥

case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝

Proof state:
case bot
α : Type u_1
a : α
h : ⊥ ≠ ⊥
⊢ a = ⊥.unbot h ↔ ↑a = ⊥

Tactic:
simpa using h rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma homologyIsoSc'_hom_ι :
    (K.homologyIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyι =
      K.homologyι j ≫ (K.opcyclesIsoSc' i j k hi hk).hom

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
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.homologyIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyι = K.homologyι j ≫ (K.opcyclesIsoSc' i j k hi hk).hom

Tactic:
apply ShortComplex.homologyι_naturality

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} {v : β} :
    get! (m.insert k v) a = if k == a then v else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k a : α
v : β
⊢ get! (m.insert k v) a = if (k == a) = true then v else get! m a

Tactic:
simp_to_raw using Raw₀.Const.get!_insert

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_smul_le_mul_eLpNorm {p q r : ℝ≥0∞} {f : α → E} (hf : AEStronglyMeasurable f μ)
    {φ : α → 𝕜} (hφ : AEStronglyMeasurable φ μ) [hpqr : HolderTriple p q r] :
    eLpNorm (φ • f) r μ ≤ eLpNorm φ p μ * eLpNorm f q μ

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : BoundedSMul 𝕜 E
p q r : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hpqr : p.HolderTriple q r
x✝ : α
⊢ ‖(fun x1 x2 => x1 • x2) (φ x✝) (f x✝)‖₊ ≤ 1 * ‖φ x✝‖₊ * ‖f x✝‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
lemma nonneg_iff_isPositive (f : E →L[𝕜] E) : 0 ≤ f ↔ f.IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ 0 ≤ f ↔ f.IsPositive

Tactic:
simpa using le_def 0 f

Result:
no goals