harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none

Proof state:
case succ
α✝ : Type u_1
p : α✝ → Bool
a : α✝
n✝ : Nat
⊢ find? p (replicate (n✝ + 1) a) = if n✝ + 1 = 0 then none else if p a = true then some a else none

Tactic:
by_cases p a <;> simp_all [replicate_succ]

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
⊢ find? p (replicate n a) = if n = 0 then none else if p a = true then some a else none

Tactic:
cases n

Result:
case zero
α✝ : Type u_1
p : α✝ → Bool
a : α✝
⊢ find? p (replicate 0 a) = if 0 = 0 then none else if p a = true then some a else none

case succ
α✝ : Type u_1
p : α✝ → Bool
a : α✝
n✝ : Nat
⊢ find? p (replicate (n✝ + 1) a) = if n✝ + 1 = 0 then none else if p a = true then some a else none

Proof state:
case zero
α✝ : Type u_1
p : α✝ → Bool
a : α✝
⊢ find? p (replicate 0 a) = if 0 = 0 then none else if p a = true then some a else none

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp] lemma toNat_le {n : ℕ} : toNat m ≤ n ↔ m ≤ n

Proof state:
m : ℤ
n : ℕ
⊢ m.toNat ≤ n ↔ m ≤ ↑n

Tactic:
rw [ofNat_le.symm, toNat_eq_max, Int.max_le]

Result:
m : ℤ
n : ℕ
⊢ m ≤ ↑n ∧ 0 ≤ ↑n ↔ m ≤ ↑n

Proof state:
m : ℤ
n : ℕ
⊢ m ≤ ↑n ∧ 0 ≤ ↑n ↔ m ≤ ↑n

Tactic:
exact and_iff_left (ofNat_zero_le _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow_left_iff_of_base_lt_one (hx0 : 0 < x) (hx1 : x < 1) :
    x ^ y < x ^ z ↔ z < y

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y < x ^ z ↔ z < y

Tactic:
rw [lt_iff_not_le, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_le]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nnnorm_pow_le' (a : α) : ∀ {n : ℕ}, 0 < n → ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
  | 1, _ => by simp only [pow_one, le_rfl]
  | n + 2, _ => by
    simpa only [pow_succ' _ (n + 1)] using
      le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)

Tactic:
simpa only [pow_succ' _ (n + 1)] using
  le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1

Tactic:
simp only [pow_one, le_rfl]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
@[simp] lemma measure_closedBall_pos_iff {X : Type*} [MetricSpace X] {m : MeasurableSpace X}
    (μ : Measure X) [IsOpenPosMeasure μ] [NoAtoms μ] {x : X} {r : ℝ} :
    0 < μ (closedBall x r) ↔ 0 < r

Proof state:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NoAtoms μ
x : X
r : ℝ
h : 0 < μ (closedBall x r)
⊢ 0 < r

Tactic:
contrapose! h

Result:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
⊢ μ (closedBall x r) ≤ 0

Proof state:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
⊢ μ (closedBall x r) ≤ 0

Tactic:
rw [(subsingleton_closedBall x h).measure_zero μ]

Result:
no goals

Proof state:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NoAtoms μ
x : X
r : ℝ
⊢ 0 < μ (closedBall x r) ↔ 0 < r

Tactic:
refine ⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩

Result:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NoAtoms μ
x : X
r : ℝ
h : 0 < μ (closedBall x r)
⊢ 0 < r
-- Mathlib/Data/Finset/Powerset.lean
theorem powerset_eq_singleton_empty : s.powerset = {∅} ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
⊢ s.powerset = {∅} ↔ s = ∅

Tactic:
rw [← powerset_empty, powerset_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setLIntegral_rnDeriv' [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α}
    (hs : MeasurableSet s) :
    ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

Tactic:
rw [← withDensity_apply _ hs, Measure.withDensity_rnDeriv_eq _ _ hμν]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_pair (x y : ZFSet.{u}) : (pair x y).toSet = {{x}, {x, y}}

Proof state:
x y : ZFSet.{u}
⊢ (x.pair y).toSet = {{x}, {x, y}}

Tactic:
simp [pair]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_add_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) :
    det (updateCol A i fun k => A k i + A k j) = det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateCol i fun k => A k i + A k j).det = A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun k => A k i + A k j).det = Aᵀ.det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun k => A k i + A k j).det = Aᵀ.det

Tactic:
exact det_updateRow_add_self Aᵀ hij

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodalWeight_eq_eval_nodal_erase_inv :
    nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
⊢ nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹

Tactic:
rw [eval_nodal, nodalWeight, prod_inv_distrib]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_eq_top_iff' (κ η : Kernel α γ) (a : α) (x : γ) :
    rnDeriv κ η a x = ∞ ↔ x ∈ mutuallySingularSetSlice κ η a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ κ.rnDeriv η a x = ⊤ ↔ x ∈ κ.mutuallySingularSetSlice η a

Tactic:
rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
/-- The first two terms of the taylor expansion of `det (1 + r • M)` at `r = 0`. -/
lemma det_one_add_smul (r : R) (M : Matrix n n R) :
    det (1 + r • M) =
      1 + trace M * r + (det (1 + (X : R[X]) • M.map C)).divX.divX.eval r * r ^ 2

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
r : R
M : Matrix n n R
⊢ (1 + r • M).det = 1 + M.trace * r + eval r (1 + X • M.map ⇑C).det.divX.divX * r ^ 2

Tactic:
simpa [eval_det, ← smul_eq_mul_diagonal] using congr_arg (eval r) (Matrix.det_one_add_X_smul M)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_natTrailingDegree : p.mirror.natTrailingDegree = p.natTrailingDegree

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
  natTrailingDegree_reverse, zero_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
rw [hp, mirror_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_bmod : bmod (bmod x m) m = bmod x m

Proof state:
x : Int
m : Nat
⊢ (x.bmod m).bmod m = x.bmod m

Tactic:
rw [bmod, bmod_emod]

Result:
x : Int
m : Nat
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) = x.bmod m

Proof state:
x : Int
m : Nat
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) = x.bmod m

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma opcycles_ext_iff {A : C} (f₁ f₂ : S.opcycles ⟶ A) :
    f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
A : C
f₁ f₂ : S.opcycles ⟶ A
⊢ f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂

Tactic:
rw [cancel_epi]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma isIso_ι_of_isColimit {c : Cocone F} (hc : IsColimit c) :
    IsIso (c.ι.app i₀)

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (hc.coconePointUniqueUpToIso h.isColimitCocone).inv

Tactic:
infer_instance

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (c.ι.app i₀)

Tactic:
simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀,
  cocone_ι_app, coconeιApp_eq_id, id_comp]

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (hc.coconePointUniqueUpToIso h.isColimitCocone).inv
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem includeLeftRingHom_comp_algebraMap :
    (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) =
      includeRight.toRingHom.comp (algebraMap R B)

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : R
⊢ (includeLeftRingHom.comp (algebraMap R A)) x✝ = (includeRight.comp (algebraMap R B)) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ includeLeftRingHom.comp (algebraMap R A) = includeRight.comp (algebraMap R B)

Tactic:
ext

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : R
⊢ (includeLeftRingHom.comp (algebraMap R A)) x✝ = (includeRight.comp (algebraMap R B)) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    [Inhabited (β k)] (hl : DistinctKeys l) : getValueCast! k (eraseKey k l) = default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
hl : DistinctKeys l
⊢ getValueCast! k (eraseKey k l) = default

Tactic:
simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey_self hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
    forIn' none b f = pure b

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
b : β
f : (a : α) → a ∈ none → β → m (ForInStep β)
⊢ forIn' none b f = pure b

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem self_sub_C_mul_X_pow {R : Type*} [Ring R] (f : R[X]) :
    f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead

Proof state:
R : Type u_2
inst✝ : Ring R
f : R[X]
⊢ f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead

Tactic:
rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
    (g : ι → M) (h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) : (∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i)

Proof state:
case insert
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
classical
convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
rw [Finset.prod_insert hjs, Finset.prod_insert hjs]
exact Associated.mul_mul (h j (Finset.mem_insert_self j s))
  (IH (fun i hi ↦ h i (Finset.mem_insert_of_mem hi)))

Result:
no goals

Proof state:
case empty
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ 1 ~ᵤ 1

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i

Tactic:
induction s using Finset.induction with
| empty =>
  simp only [Finset.prod_empty]
  rfl
| @insert j s hjs IH =>
  classical
  convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
  rw [Finset.prod_insert hjs, Finset.prod_insert hjs]
  exact Associated.mul_mul (h j (Finset.mem_insert_self j s))
    (IH (fun i hi ↦ h i (Finset.mem_insert_of_mem hi)))

Result:
no goals

Proof state:
case empty
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ ∏ i ∈ ∅, f i ~ᵤ ∏ i ∈ ∅, g i

Tactic:
simp only [Finset.prod_empty]

Result:
case empty
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ 1 ~ᵤ 1

Proof state:
case insert
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
rw [Finset.prod_insert hjs, Finset.prod_insert hjs]

Result:
case insert
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ f j * ∏ x ∈ s, f x ~ᵤ g j * ∏ x ∈ s, g x

Proof state:
case insert
M : Type u_5
inst✝ : CommMonoid M
ι : Type u_6
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ f j * ∏ x ∈ s, f x ~ᵤ g j * ∏ x ∈ s, g x

Tactic:
exact Associated.mul_mul (h j (Finset.mem_insert_self j s))
  (IH (fun i hi ↦ h i (Finset.mem_insert_of_mem hi)))

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem image_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).image some = s.erase none

Proof state:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (eraseNone s) = s.erase none

Tactic:
ext (_ | x) <;> simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem degrees_sub_le [DecidableEq σ] {p q : MvPolynomial σ R} :
    (p - q).degrees ≤ p.degrees ∪ q.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p - q).degrees ≤ p.degrees ∪ q.degrees

Tactic:
simpa [degrees_def] using AddMonoidAlgebra.supDegree_sub_le

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem get_toList (n : ℕ) (hn : n < length (toList p x)) :
    (toList p x).get ⟨n, hn⟩ = (p ^ n) x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hn : n < (p.toList x).length
⊢ (p.toList x).get ⟨n, hn⟩ = (p ^ n) x

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem dvd_add_iff : ∀ {a b c : Ordinal}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
  | a, _, c, ⟨b, rfl⟩ =>
    ⟨fun ⟨d, e⟩ => ⟨d - b, by rw [mul_sub, ← e, add_sub_cancel]⟩, fun ⟨d, e⟩ => by
      rw [e, ← mul_add]
      apply dvd_mul_right⟩

Proof state:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + c

Tactic:
rw [e, ← mul_add]

Result:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)

Proof state:
a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * (d - b)

Tactic:
rw [mul_sub, ← e, add_sub_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x)

Proof state:
case zero
α : Sort u_1
f : Fin (0 + 1) → α → α
x : α
⊢ foldr (0 + 1) f x = foldr 0 (fun x => f x.castSucc) (f (last 0) x)

Tactic:
simp [foldr_succ, Fin.last]

Result:
no goals

Proof state:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : Fin (n + 1) → α → α) (x : α), foldr (n + 1) f x = foldr n (fun x => f x.castSucc) (f (last n) x)
f : Fin (n + 1 + 1) → α → α
x : α
⊢ f 0 (foldr n (fun x => f x.castSucc.succ) (f (last n).succ x)) =
    f (castSucc 0) (foldr n (fun i => f i.succ.castSucc) (f (last (n + 1)) x))

Tactic:
simp [succ_castSucc]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- Any object with non-empty fiber admits a hom from a Galois object. -/
lemma exists_hom_from_galois_of_fiber_nonempty (X : C) (h : Nonempty (F.obj X)) :
    ∃ (A : C) (_ : A ⟶ X), IsGalois A

Proof state:
case intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
⊢ ∃ A x, IsGalois A

Tactic:
obtain ⟨A, f, a, h1, _⟩ := exists_hom_from_galois_of_fiber F X x

Result:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
f : A ⟶ X
a : (F.obj A).carrier
h1 : IsGalois A
right✝ : F.map f a = x
⊢ ∃ A x, IsGalois A

Proof state:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
f : A ⟶ X
a : (F.obj A).carrier
h1 : IsGalois A
right✝ : F.map f a = x
⊢ ∃ A x, IsGalois A

Tactic:
exact ⟨A, f, h1⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
h : Nonempty (F.obj X).carrier
⊢ ∃ A x, IsGalois A

Tactic:
obtain ⟨x⟩ := h

Result:
case intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
⊢ ∃ A x, IsGalois A
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_uIcc : Neg.neg '' [[a, b]] = [[-a, -b]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem bind_bind {γ} [MeasurableSpace γ] {m : Measure α} {f : α → Measure β} {g : β → Measure γ}
    (hf : Measurable f) (hg : Measurable g) : bind (bind m f) g = bind m fun a => bind (f a) g

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ((m.bind f).bind g) s = (m.bind fun a => (f a).bind g) s

Tactic:
erw [bind_apply hs hg, bind_apply hs ((measurable_bind' hg).comp hf),
  lintegral_bind hf ((measurable_coe hs).comp hg)]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), (((fun m => m.bind g) ∘ f) a) s ∂m

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), ∫⁻ (a : β), (g a) s ∂f a ∂m

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
⊢ (m.bind f).bind g = m.bind fun a => (f a).bind g

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ((m.bind f).bind g) s = (m.bind fun a => (f a).bind g) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), (((fun m => m.bind g) ∘ f) a) s ∂m

Tactic:
conv_rhs => enter [2, a]; erw [bind_apply hs hg]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), ∫⁻ (a : β), (g a) s ∂f a ∂m
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.add_add (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
    (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖

Tactic:
refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_) <;> simp [abs_of_nonneg, add_nonneg]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.abs {β} [NormedLatticeAddCommGroup β] {f : α → β} (hf : Integrable f μ) :
    Integrable (fun a => |f a|) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ Integrable (fun a => |f a|) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : MemLp f 1 μ
⊢ MemLp (fun a => |f a|) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : MemLp f 1 μ
⊢ MemLp (fun a => |f a|) 1 μ

Tactic:
exact hf.abs

Result:
no goals