harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Rotate.lean
theorem zipWith_rotate_distrib {β γ : Type*} (f : α → β → γ) (l : List α) (l' : List β) (n : ℕ)
    (h : l.length = l'.length) :
    (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Proof state:
case h
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
rw [length_drop, length_drop, h]

Result:
no goals

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod,
  rotate_eq_drop_append_take_mod, h, zipWith_append, ← drop_zipWith, ←
  take_zipWith, List.length_zipWith, h, min_self]

Result:
case h
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIso.hom_snd :
    (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ snd i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
delta pullbackDiagonalMapIso

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ snd i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ snd i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
theorem ShortComplex.mapToComposableArrows_comp {S₁ S₂ S₃ : ShortComplex C} (φ : S₁ ⟶ S₂)
    (ψ : S₂ ⟶ S₃) : ShortComplex.mapToComposableArrows (φ ≫ ψ) =
      ShortComplex.mapToComposableArrows φ ≫ ShortComplex.mapToComposableArrows ψ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
ψ : S₂ ⟶ S₃
⊢ mapToComposableArrows (φ ≫ ψ) = mapToComposableArrows φ ≫ mapToComposableArrows ψ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem fst_apply {s : Set α} (hs : MeasurableSet s) : ρ.fst s = ρ (Prod.fst ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ ρ.fst s = ρ (Prod.fst ⁻¹' s)

Tactic:
rw [fst, Measure.map_apply measurable_fst hs]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem mem_vars_bind₁ (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) {j : τ}
    (h : j ∈ (bind₁ f φ).vars) : ∃ i : σ, i ∈ φ.vars ∧ j ∈ (f i).vars

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ ((bind₁ f) φ).vars
⊢ ∃ i ∈ φ.vars, j ∈ (f i).vars

Tactic:
classical
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ ((bind₁ f) φ).vars
⊢ ∃ i ∈ φ.vars, j ∈ (f i).vars

Tactic:
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_zero : m.degree (0 : MvPolynomial σ R) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.degree 0 = 0

Tactic:
simp [degree]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_mulVec [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) :
    (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
⊢ (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)

Tactic:
rw [← vecMul_vecMul, vecMul_transpose]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem cast_trans {α β γ : Type u} {r : α → α → Prop} {s : β → β → Prop}
    {t : γ → γ → Prop} (h₁ : α = β) (h₁' : β = γ) (h₂ : HEq r s) (h₂' : HEq s t) :
    (RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast (h₁.trans h₁') (h₂.trans h₂') :=
  ext fun x => by subst h₁; rfl

Proof state:
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : HEq r s
h₂' : HEq s t
x : α
⊢ ((RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
subst h₁

Result:
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Proof state:
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem comap_const (f : C(X, Y)) (y : Y) (h : ∀ x, f x = y) :
    (comap f : LocallyConstant Y Z → LocallyConstant X Z) = fun g => const X (g y)

Proof state:
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝

Tactic:
simp [h]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g => const X (g y)

Tactic:
ext

Result:
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_div_rev (a b : E) : ‖a / b‖ = ‖b / a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ = ‖b / a‖

Tactic:
simpa only [dist_eq_norm_div] using dist_comm a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_set_self {l : List α} {i : Nat} {a : α} (h : i < l.length) :
    (l.set i a)[i]? = some a

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ (l.set i a)[i]? = some a

Tactic:
simp_all [getElem?_eq_some_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
lemma tmul_single {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) :
    x ⊗ₜ[R] Pi.single i m j = (Pi.single i (x ⊗ₜ[R] m) : ∀ i, N ⊗[R] M i) j

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_11
inst✝² : DecidableEq ι
M : ι → Type u_12
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

Tactic:
by_cases h : i = j <;> aesop

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem mem_powersetCard {n : ℕ} {s t : Multiset α} : s ∈ powersetCard n t ↔ s ≤ t ∧ card s = n :=
  Quotient.inductionOn t fun l => by simp [powersetCard_coe']

Proof state:
α : Type u_1
n : ℕ
s t : Multiset α
l : List α
⊢ s ∈ powersetCard n ⟦l⟧ ↔ s ≤ ⟦l⟧ ∧ s.card = n

Tactic:
simp [powersetCard_coe']

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
/-- A characterisation of `Module.End.IsFinitelySemisimple` using only the lattice of submodules of
`M` (thus avoiding submodules of submodules). -/
lemma isFinitelySemisimple_iff :
    f.IsFinitelySemisimple ↔ ∀ p ∈ invtSubmodule f, Module.Finite R p → ∀ q ∈ invtSubmodule f,
      q ≤ p → ∃ r, r ≤ p ∧ r ∈ invtSubmodule f ∧ Disjoint q r ∧ q ⊔ r = p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ f.IsFinitelySemisimple ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
simp_rw [isFinitelySemisimple_iff', isSemisimple_restrict_iff]

Result:
no goals
-- Mathlib/Data/Finmap.lean
@[simp] lemma keysLookupEquiv_symm_apply_keys :
    ∀ f : {f : Finset α × (∀ a, Option (β a)) // ∀ i, (f.2 i).isSome ↔ i ∈ f.1},
      (keysLookupEquiv.symm f).keys = f.1.1 :=
  keysLookupEquiv.surjective.forall.2 fun _ => by
    simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : Finmap β
⊢ (keysLookupEquiv.symm (keysLookupEquiv x✝)).keys = (↑(keysLookupEquiv x✝)).1

Tactic:
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem connectedComponents_preimage_singleton {x : α} :
    (↑) ⁻¹' ({↑x} : Set (ConnectedComponents α)) = connectedComponent x

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x

Tactic:
rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x

Tactic:
ext y

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_push_eq_some {xs : Vector α n} :
    (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b))

Proof state:
case mk
α : Type
n : Nat
a : α
p : α → Bool
b : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) = some b ↔
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = some b ∨
      find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = none ∧ p a = true ∧ a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type
n : Nat
a : α
p : α → Bool
b : α
xs : Vector α n
⊢ find? p (xs.push a) = some b ↔ find? p xs = some b ∨ find? p xs = none ∧ p a = true ∧ a = b

Tactic:
cases xs

Result:
case mk
α : Type
n : Nat
a : α
p : α → Bool
b : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) = some b ↔
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = some b ∨
      find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = none ∧ p a = true ∧ a = b
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_ssubset_Icc_right (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) :
    Icc a₁ b₁ ⊂ Icc a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Result:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_right hI ha hb

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_convex : Convex ℝ (convexBodySum K B)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ Convex ℝ (convexBodySum K B)

Tactic:
refine Convex_subadditive_le (fun _ _ => convexBodySumFun_add_le _ _) (fun c x h => ?_) B

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ convexBodySumFun (c • x) ≤ c * convexBodySumFun x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ convexBodySumFun (c • x) ≤ c * convexBodySumFun x

Tactic:
convert le_of_eq (convexBodySumFun_smul c x)

Result:
case h.e'_4.h.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ c = |c|

Proof state:
case h.e'_4.h.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ c = |c|

Tactic:
exact (abs_eq_self.mpr h).symm

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem isGenericPoint_iff_specializes : IsGenericPoint x S ↔ ∀ y, x ⤳ y ↔ y ∈ S

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S

Tactic:
simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
/-- See `zero_lt_three'` for a version with the type explicit. -/
@[simp] lemma zero_lt_three : (0 : α) < 3

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3

Tactic:
rw [← two_add_one_eq_three]

Result:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 2 + 1

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 2 + 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.nonempty_minimalPrimes (h : I ≠ ⊤) : Nonempty I.minimalPrimes

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty ↑I.minimalPrimes

Tactic:
obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h

Result:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
⊢ Nonempty ↑I.minimalPrimes

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
⊢ Nonempty ↑I.minimalPrimes

Tactic:
obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ Nonempty ↑I.minimalPrimes

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ Nonempty ↑I.minimalPrimes

Tactic:
exact ⟨p, hp⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_antiperiodic : Function.Antiperiodic sin π

Proof state:
⊢ Function.Antiperiodic sin π

Tactic:
simp [sin_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_reverse [Monad m] (l : Array α) (f : α → β → m β) (b) :
    l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : α → β → m β
b : β
⊢ foldrM f b l.reverse = foldlM (fun x y => f y x) b l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b { toList := l }.reverse = foldlM (fun x y => f y x) b { toList := l }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b { toList := l }.reverse = foldlM (fun x y => f y x) b { toList := l }

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
lemma additive_of_comp_faithful
    (F : C ⥤ D) (G : D ⥤ E) [G.Additive] [(F ⋙ G).Additive] [Faithful G] :
    F.Additive where
  map_add {_ _ f₁ f₂} := G.map_injective (by
    rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map])

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Category.{u_6, u_3} E
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : Preadditive E
F : C ⥤ D
G : D ⥤ E
inst✝² : G.Additive
inst✝¹ : (F ⋙ G).Additive
inst✝ : G.Faithful
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)

Tactic:
rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_finite [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite) :
    count s = hs.toFinset.card

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Finite
⊢ count s = ↑hs.toFinset.card

Tactic:
rw [← count_apply_finset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_zero_add (x y : V) : midpoint R 0 (x + y) = midpoint R x y :=
  (midpoint_eq_midpoint_iff_vsub_eq_vsub R).2 <| by simp [sub_add_eq_sub_sub_swap]

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ 0 -ᵥ x = y -ᵥ (x + y)

Tactic:
simp [sub_add_eq_sub_sub_swap]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Cast.lean
theorem cast_factorial : (a ! : S) = (ascPochhammer S a).eval 1

Proof state:
S : Type u_1
inst✝ : Semiring S
a : ℕ
⊢ ↑a ! = Polynomial.eval 1 (ascPochhammer S a)

Tactic:
rw [← one_ascFactorial, cast_ascFactorial, cast_one]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_neg {n : ℤ} {x : AddCircle T} : fourier (-n) x = conj (fourier n x)

Proof state:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

Tactic:
induction x using QuotientAddGroup.induction_on

Result:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ (fourier (-n)) ↑z✝ = (starRingEnd ℂ) ((fourier n) ↑z✝)

Proof state:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))

Tactic:
rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]

Result:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift ↑(-n • z✝)) = (starRingEnd ℂ) ↑(⋯.lift ↑(n • z✝))

Proof state:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift ↑(-n • z✝)) = (starRingEnd ℂ) ↑(⋯.lift ↑(n • z✝))

Tactic:
simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
  neg_smul, mul_neg]

Result:
no goals

Proof state:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ (fourier (-n)) ↑z✝ = (starRingEnd ℂ) ((fourier n) ↑z✝)

Tactic:
simp_rw [fourier_apply, toCircle]

Result:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem exists_superset_of_isCompact {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ s ⊆ ⋃ i, (interior ∘ ⇑K) i

Tactic:
intro x _

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
a✝ : x ∈ s
⊢ x ∈ ⋃ i, (interior ∘ ⇑K) i

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 => x1 ⊆ x2) (interior ∘ ⇑K)

Tactic:
exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

Result:
no goals

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
a✝ : x ∈ s
⊢ x ∈ ⋃ i, (interior ∘ ⇑K) i

Tactic:
rcases K.exists_mem x with ⟨k, hk⟩

Result:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
a✝ : x ∈ s
k : ℕ
hk : x ∈ K k
⊢ x ∈ ⋃ i, (interior ∘ ⇑K) i

Proof state:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
a✝ : x ∈ s
k : ℕ
hk : x ∈ K k
⊢ x ∈ ⋃ i, (interior ∘ ⇑K) i

Tactic:
exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ ∃ n, s ⊆ interior (K n)

Tactic:
refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ s ⊆ ⋃ i, (interior ∘ ⇑K) i

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 => x1 ⊆ x2) (interior ∘ ⇑K)
-- Mathlib/Logic/Basic.lean
theorem forall_apply_eq_imp_iff' {f : α → β} {p : β → Prop} :
    (∀ a b, f a = b → p b) ↔ ∀ a, p (f a)

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem eqOn_sup {φ ψ : F} {S T : Subalgebra R A} (hS : Set.EqOn φ ψ S) (hT : Set.EqOn φ ψ T) :
    Set.EqOn φ ψ ↑(S ⊔ T)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn ⇑φ ⇑ψ ↑S
hT : Set.EqOn ⇑φ ⇑ψ ↑T
⊢ Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)

Tactic:
rw [← le_equalizer] at hS hT ⊢

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ equalizer φ ψ
hT : T ≤ equalizer φ ψ
⊢ S ⊔ T ≤ equalizer φ ψ

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ equalizer φ ψ
hT : T ≤ equalizer φ ψ
⊢ S ⊔ T ≤ equalizer φ ψ

Tactic:
exact sup_le hS hT

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem JacobiSym.mod_left (a : ℤ) (b ab' : ℕ) (ab r b' : ℤ) (hb' : (b : ℤ) = b')
    (hab : a % b' = ab) (h : (ab' : ℤ) = ab) (hr : jacobiSymNat ab' b = r) : jacobiSym a b = r

Proof state:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
@[simp]
lemma comp_id (κ : Kernel α β) : κ ∘ₖ Kernel.id = κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ ∘ₖ Kernel.id = κ

Tactic:
rw [Kernel.id, comp_deterministic_eq_comap, comap_id]

Result:
no goals