harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_add_left (hf : IntervalIntegrable f volume a b) (c : ℝ) :
    IntervalIntegrable (fun x => f (c + x)) volume (a - c) (b - c)

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (c + x)) volume (a - c) (b - c)

Tactic:
simpa only [add_comm] using IntervalIntegrable.comp_add_right hf c

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma iUnion_inter_iUnion {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j

Proof state:
α : Type u_1
ι : Sort u_12
κ : Sort u_13
f : ι → Set α
g : κ → Set α
⊢ (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j

Tactic:
simp_rw [iUnion_inter, inter_iUnion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem some_getElem_eq_getElem?_iff (xs : List α) (i : Nat) (h : i < xs.length) :
    (some xs[i] = xs[i]?) ↔ True

Proof state:
α : Type u_1
xs : List α
i : Nat
h : i < xs.length
⊢ some xs[i] = xs[i]? ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/IsLocalHomeomorph.lean
lemma isLocallyInjective (hf : IsLocalHomeomorph f) : IsLocallyInjective f :=
  fun x ↦ by obtain ⟨f, hx, rfl⟩ := hf x; exact ⟨f.source, f.open_source, hx, f.injOn⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
obtain ⟨f, hx, rfl⟩ := hf x

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
f : PartialHomeomorph X Y
hx : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn (↑f) U

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
f : PartialHomeomorph X Y
hx : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn (↑f) U

Tactic:
exact ⟨f.source, f.open_source, hx, f.injOn⟩

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@[ext]
lemma sections_ext {M : PresheafOfModules.{v} R} (s t : M.sections)
    (h : ∀ (X : Cᵒᵖ), s.val X = t.val X) : s = t :=
  Subtype.ext (by ext; apply h)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
x✝ : Cᵒᵖ
⊢ ↑s x✝ = ↑t x✝

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
⊢ ↑s = ↑t

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
x✝ : Cᵒᵖ
⊢ ↑s x✝ = ↑t x✝
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_le_iff {o f a} : bsup.{u, v} o f ≤ a ↔ ∀ i h, f i h ≤ a :=
  sup_le_iff.trans
    ⟨fun h i hi => by
      rw [← familyOfBFamily_enum o f]
      exact h _, fun h _ => h _ _⟩

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) ≤ a

Tactic:
exact h _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ a

Tactic:
rw [← familyOfBFamily_enum o f]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) ≤ a
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem lapply_comp_lsingle_same [DecidableEq ι] (i : ι) :
    lapply i ∘ₗ lsingle i = (.id : M i →ₗ[R] M i)

Proof state:
case h
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
x✝ : M i
⊢ (lapply i ∘ₗ lsingle i) x✝ = LinearMap.id x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ lapply i ∘ₗ lsingle i = LinearMap.id

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
x✝ : M i
⊢ (lapply i ∘ₗ lsingle i) x✝ = LinearMap.id x✝
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem InitialMonoClass.of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) :
    InitialMonoClass C where
  isInitial_mono_from {I'} X hI'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono (hI'.to X)

Tactic:
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)

Tactic:
apply mono_comp

Result:
no goals
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem implicitToPartialHomeomorphOfComplemented_apply_ker (hf : HasStrictFDerivAt f f' a)
    (hf' : range f' = ⊤) (hker : (ker f').ClosedComplemented) (y : ker f') :
    hf.implicitToPartialHomeomorphOfComplemented f f' hf' hker (y + a) = (f (y + a), y)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : (LinearMap.ker f').ClosedComplemented
y : ↥(LinearMap.ker f')
⊢ ↑(implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) (↑y + a) = (f (↑y + a), y)

Tactic:
simp only [implicitToPartialHomeomorphOfComplemented_apply, add_sub_cancel_right,
  Classical.choose_spec hker]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardDistinctFactors_zero : ω 0 = 0

Proof state:
⊢ ω 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
lemma mapsTo_pow_toEnd_sub_algebraMap {φ : R} {k : ℕ} {x : L} :
    MapsTo ((toEnd R L M x - algebraMap R (Module.End R M) φ) ^ k) N N

Proof state:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo (⇑((toEnd R L M) x - (algebraMap R (Module.End R M)) φ))^[k] ↑N ↑N

Tactic:
exact MapsTo.iterate (fun m hm ↦ N.sub_mem (N.lie_mem hm) (N.smul_mem _ hm)) k

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo ⇑(((toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N

Tactic:
rw [LinearMap.coe_pow]

Result:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo (⇑((toEnd R L M) x - (algebraMap R (Module.End R M)) φ))^[k] ↑N ↑N
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem cast_eq_id {α : Type u} : cast (rfl : α = α) = id

Proof state:
α : Type u
⊢ cast ⋯ = id

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_transpose (M : ∀ i, Matrix (m' i) (n' i) α) :
    (blockDiagonal' M)ᵀ = blockDiagonal' fun k => (M k)ᵀ

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (if h : ji = ii then M ji jx (cast ⋯ ix) else 0) = if h : ii = ji then M ii (cast ⋯ jx) ix else 0

Tactic:
split_ifs <;> cc

Result:
no goals

Proof state:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (blockDiagonal' M)ᵀ ⟨ii, ix⟩ ⟨ji, jx⟩ = blockDiagonal' (fun k => (M k)ᵀ) ⟨ii, ix⟩ ⟨ji, jx⟩

Tactic:
simp only [transpose_apply, blockDiagonal'_apply]

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (if h : ji = ii then M ji jx (cast ⋯ ix) else 0) = if h : ii = ji then M ii (cast ⋯ jx) ix else 0

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᵀ = blockDiagonal' fun k => (M k)ᵀ

Tactic:
ext ⟨ii, ix⟩ ⟨ji, jx⟩

Result:
case a.mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (blockDiagonal' M)ᵀ ⟨ii, ix⟩ ⟨ji, jx⟩ = blockDiagonal' (fun k => (M k)ᵀ) ⟨ii, ix⟩ ⟨ji, jx⟩
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- The right derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `derivWithin` in that case is 0. -/
@[simp]
lemma rightDeriv_klFun : derivWithin klFun (Ioi x) x = log x

Proof state:
case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)

Result:
no goals

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
simp only [h0, log_zero]

Result:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi 0) 0 = 0

Proof state:
x : ℝ
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
by_cases h0 : x = 0

Result:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi x) x = log x

case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi 0) 0 = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Ioi_zero

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma dvd_sum (h : ∀ i ∈ s, a ∣ f i) : a ∣ ∑ i ∈ s, f i :=
  Multiset.dvd_sum fun y hy => by rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx

Proof state:
case intro.intro
ι : Type u_1
α : Type u_3
s : Finset ι
a : α
f : ι → α
inst✝ : NonUnitalSemiring α
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i => f i) s.val
⊢ a ∣ f x

Tactic:
exact h x hx

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
s : Finset ι
a : α
f : ι → α
inst✝ : NonUnitalSemiring α
h : ∀ i ∈ s, a ∣ f i
y : α
hy : y ∈ Multiset.map (fun i => f i) s.val
⊢ a ∣ y

Tactic:
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩

Result:
case intro.intro
ι : Type u_1
α : Type u_3
s : Finset ι
a : α
f : ι → α
inst✝ : NonUnitalSemiring α
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i => f i) s.val
⊢ a ∣ f x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem none_eq_getElem?_iff {a : Vector α n} {i : Nat} : none = a[i]? ↔ n ≤ i

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
⊢ none = a[i]? ↔ n ≤ i

Tactic:
simp [eq_comm (a := none)]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_zero_of_degree_lt_of_eval_finset_eq_zero (degree_f_lt : f.degree < #s)
    (eval_f : ∀ x ∈ s, f.eval x = 0) : f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0

Tactic:
simp_rw [eval_eq_sum_degreeLTEquiv degree_f_lt] at eval_f

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i : Fin #s, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i : Fin #s, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ f = 0

Tactic:
rw [← degreeLTEquiv_eq_zero_iff_eq_zero degree_f_lt]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i : Fin #s, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0

Tactic:
rw [← mem_degreeLT] at degree_f_lt

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
eval_f : ∀ x ∈ s, ∑ i : Fin #s, (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0
⊢ (degreeLTEquiv R #s) ⟨f, degree_f_lt⟩ = 0

Tactic:
exact
  Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero
    (Injective.comp (Embedding.subtype _).inj' (equivFinOfCardEq (card_coe _)).symm.injective)
    fun _ => eval_f _ (Finset.coe_mem _)

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem natCast_lt_cast {m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
m : ℕ
n : ℚ≥0
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
    ↑(⨆ i, f i) = (⨆ i, f i : WithTop α)

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Icc (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)

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

Tactic:
simp [← Ici_inter_Iic, h]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
@[simp] lemma mersenne_odd : ∀ {p : ℕ}, Odd (mersenne p) ↔ p ≠ 0
  | 0 => by simp
  | p + 1 => by
    simpa using Nat.Even.sub_odd (one_le_pow₀ one_le_two)
      (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

Proof state:
⊢ Odd (mersenne 0) ↔ 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
⊢ Odd (mersenne (p + 1)) ↔ p + 1 ≠ 0

Tactic:
simpa using Nat.Even.sub_odd (one_le_pow₀ one_le_two)
  (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableAt.sub_iff_right (hg : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 g x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hg : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 g x

Tactic:
simp only [sub_eq_add_neg, hg, add_iff_right, differentiableAt_neg_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_mul_inv_iff_mul_lt : c < a * b⁻¹ ↔ c * b < a :=
  (mul_lt_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ c * b < a * b⁻¹ * b ↔ c * b < a

Tactic:
rw [inv_mul_cancel_right]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem exists_reduced_word' (w : W) : ∃ ω : List B, cs.IsReduced ω ∧ w = π ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω

Tactic:
rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ ω_1, cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ ω_1, cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1

Tactic:
use ω

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.IsReduced ω ∧ cs.wordProd ω = cs.wordProd ω

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.IsReduced ω ∧ cs.wordProd ω = cs.wordProd ω

Tactic:
tauto

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph0_le_preAleph {o : Ordinal} : ℵ₀ ≤ preAleph o ↔ ω ≤ o

Proof state:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ preAleph o ↔ ω ≤ o

Tactic:
rw [← preAleph_omega0, preAleph_le_preAleph]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
/-- One can prove `QuotientMeasureEqMeasurePreimage` by checking behavior with respect to a single
fundamental domain. -/
@[to_additive]
lemma IsFundamentalDomain.quotientMeasureEqMeasurePreimage {μ : Measure (Quotient α_mod_G)}
    {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) (h : μ = (ν.restrict s).map π) :
    QuotientMeasureEqMeasurePreimage ν μ

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
μ : Measure (Quotient α_mod_G)
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
h : μ = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
simpa [h] using fund_dom_s.quotientMeasureEqMeasurePreimage_quotientMeasure

Result:
no goals
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem comul_tensorObj :
    Coalgebra.comul (R := R) (A := (CoalgebraCat.of R M ⊗ CoalgebraCat.of R N : CoalgebraCat R))
      = Coalgebra.comul (A := M ⊗[R] N)

Proof state:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom ↑(tensorTensorTensorComm R M M N N)) =
    ↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom
      ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N)).comul =
    CoalgebraStruct.comul

Tactic:
dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj,
  instCoalgebraStruct_comul]

Result:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N).toComonObj).comul =
    ↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul

Proof state:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N).toComonObj).comul =
    ↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X,
  toComonObj_comul, tensorμ_eq_tensorTensorTensorComm]

Result:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom ↑(tensorTensorTensorComm R M M N N)) =
    ↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul

Proof state:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
rw [ofComonObjCoalgebraStruct_comul]

Result:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom
      ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N)).comul =
    CoalgebraStruct.comul
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_single_zero_mul [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} :
    ((single 0 r : HahnSeries Γ R) * x).coeff a = r * x.coeff a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
⊢ ((single 0) r * x).coeff a = r * x.coeff a

Tactic:
rw [← add_zero a, coeff_single_mul_add, add_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_comap_uniformSpace {u : UniformSpace β} {α} {f : α → β} {l : Filter α} :
    Cauchy (uniformSpace := comap f u) l ↔ Cauchy (map f l)

Proof state:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun p => (f p.1, f p.2)) (𝓤 β)

Tactic:
rfl

Result:
no goals

Proof state:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ Cauchy l ↔ Cauchy (map f l)

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]

Result:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun p => (f p.1, f p.2)) (𝓤 β)
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite products, then `F.unop : C ⥤ D` preserves finite
    coproducts. -/
lemma preservesFiniteCoproducts_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesFiniteProducts F] :
    PreservesFiniteCoproducts F.unop where
  preserves _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_unop

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals