harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem iSup_mem_measurableLE' (f : ℕ → α → ℝ≥0∞) (hf : ∀ n, f n ∈ measurableLE μ ν) (n : ℕ) :
    (⨆ (k) (_ : k ≤ n), f k) ∈ measurableLE μ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n), f k ∈ measurableLE μ ν

Tactic:
convert iSup_mem_measurableLE f hf n

Result:
case h.e'_5.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
⊢ (⨆ k, ⨆ (_ : k ≤ n), f k) x✝ = ⨆ k, ⨆ (_ : k ≤ n), f k x✝

Proof state:
case h.e'_5.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
⊢ (⨆ k, ⨆ (_ : k ≤ n), f k) x✝ = ⨆ k, ⨆ (_ : k ≤ n), f k x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_eq_pow_card (s : Multiset α) (comm) (m : α) (h : ∀ x ∈ s, x = m) :
    s.noncommProd comm = m ^ Multiset.card s

Proof state:
α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
m : α
h : ∀ x ∈ s, x = m
⊢ s.noncommProd comm = m ^ s.card

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, x = m
⊢ noncommProd ⟦a✝⟧ comm = m ^ card ⟦a✝⟧

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, x = m
⊢ noncommProd ⟦a✝⟧ comm = m ^ card ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *

Result:
case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ a✝, x = m
⊢ a✝.prod = m ^ a✝.length

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ a✝, x = m
⊢ a✝.prod = m ^ a✝.length

Tactic:
exact List.prod_eq_pow_card _ m h

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem coeff_p_pow [CharP R p] (i : ℕ) : ((p : 𝕎 R) ^ i).coeff i = 1

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ (↑p ^ 0).coeff 0 = 1

Tactic:
simp only [one_coeff_zero, Ne, pow_zero]

Result:
no goals

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ (i + 1)).coeff (i + 1) = 1

Tactic:
rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
  verschiebung_coeff_succ, h, one_pow]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ (↑p ^ i).coeff i = 1

Tactic:
induction' i with i h

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ (↑p ^ 0).coeff 0 = 1

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ (i + 1)).coeff (i + 1) = 1
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal (H1 : IsRelPrime x z) (H2 : x ∣ y * z)
    (h : IsPrimal x) : x ∣ y

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := h H2

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommMonoid α
y z a b : α
ha : a ∣ y
hb : b ∣ z
H1 : IsRelPrime (a * b) z
H2 : a * b ∣ y * z
h : IsPrimal (a * b)
⊢ a * b ∣ y

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommMonoid α
y z a b : α
ha : a ∣ y
hb : b ∣ z
H1 : IsRelPrime (a * b) z
H2 : a * b ∣ y * z
h : IsPrimal (a * b)
⊢ a * b ∣ y

Tactic:
exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem roots_C_mul_X_add_C (b : R) (ha : a ≠ 0) : (C a * X + C b).roots = {-(a⁻¹ * b)}

Proof state:
R : Type u
a : R
inst✝ : Field R
b : R
ha : a ≠ 0
⊢ (C a * X + C b).roots = {-(a⁻¹ * b)}

Tactic:
simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsPath.tail {p : G.Walk u v} (hp : p.IsPath) : p.tail.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.tail.IsPath

Tactic:
cases p with
| nil => simp
| cons hadj p =>
  simp_all [Walk.isPath_def]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
hp : (cons hadj p).IsPath
⊢ (cons hadj p).tail.IsPath

Tactic:
simp_all [Walk.isPath_def]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u : V
hp : Walk.nil.IsPath
⊢ Walk.nil.tail.IsPath

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem IsInitial.hasInitial {X : C} (h : IsInitial X) : HasInitial C where
  has_colimit F :=
    HasColimit.mk ⟨⟨X, by aesop_cat, by simp⟩, isColimitChangeEmptyCocone _ h _ (Iso.refl _)⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty.{1} ⥤ C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as => ⋯.elim) =
      id (Discrete.casesOn X_1 fun as => ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_concat (s n : Nat) : range' s (n + 1) step = range' s n step ++ #v[s + step * n]

Proof state:
step s n : Nat
⊢ range' s (n + 1) step = range' s n step ++ { toArray := #[s + step * n], size_toArray := ⋯ }

Tactic:
exact (range'_append s n 1 step).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : Array α) (f : α → β → β) (init : β) :
    forIn l init (fun a b => pure (.yield (f a b))) =
      pure (f := m) (l.foldl (fun b a => f a b) init)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => pure (ForInStep.yield (f a b))) =
    pure (foldl (fun b a => f a b) init { toList := toList✝ })

Tactic:
simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : α → β → β
init : β
⊢ (forIn l init fun a b => pure (ForInStep.yield (f a b))) = pure (foldl (fun b a => f a b) init l)

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => pure (ForInStep.yield (f a b))) =
    pure (foldl (fun b a => f a b) init { toList := toList✝ })
-- Mathlib/Data/DFinsupp/Submonoid.lean
theorem dfinsupp_sumAddHom_mem [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] {S : Type*}
    [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ i, β i) (g : ∀ i, β i →+ γ)
    (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : DFinsupp.sumAddHom g f ∈ s

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
rw [DFinsupp.sumAddHom_apply]

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (f.sum fun x => ⇑(g x)) ∈ s
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@[simp] lemma num_nonpos {a : ℚ} : a.num ≤ 0 ↔ a ≤ 0

Proof state:
a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0

Tactic:
simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem compl_mem_coprodᵢ {s : Set (∀ i, α i)} :
    sᶜ ∈ Filter.coprodᵢ f ↔ ∀ i, (eval i '' s)ᶜ ∈ f i

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (eval i '' s)ᶜ ∈ f i

Tactic:
simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a

Proof state:
case intro.intro
α : Type u_1
a : α
l : List α
h✝ : a ∈ l
n : Nat
h : n < l.length
e : l[n] = a
⊢ ∃ n, l.get n = a

Tactic:
exact ⟨⟨n, h⟩, e⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ ∃ n, l.get n = a

Tactic:
obtain ⟨n, h, e⟩ := getElem_of_mem h

Result:
case intro.intro
α : Type u_1
a : α
l : List α
h✝ : a ∈ l
n : Nat
h : n < l.length
e : l[n] = a
⊢ ∃ n, l.get n = a
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma oddKernel_def (a x : ℝ) : ↑(oddKernel a x) = jacobiTheta₂'' a (I * x)

Proof state:
a x : ℝ
⊢ ↑(oddKernel (↑a) x) = jacobiTheta₂'' (↑a) (I * ↑x)

Tactic:
simp [oddKernel, ← conj_eq_iff_re, jacobiTheta₂''_conj]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma compProd_toKernel [IsFiniteKernel κ] [IsSFiniteKernel ν] (hf : IsCondKernelCDF f κ ν) :
    ν ⊗ₖ hf.toKernel f = κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ ((ν ⊗ₖ IsCondKernelCDF.toKernel f hf) a) s = (κ a) s

Tactic:
rw [Kernel.compProd_apply hs, lintegral_toKernel_mem hf a hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
⊢ ν ⊗ₖ IsCondKernelCDF.toKernel f hf = κ

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ ((ν ⊗ₖ IsCondKernelCDF.toKernel f hf) a) s = (κ a) s
-- Mathlib/Order/Bounds/Basic.lean
theorem isGreatest_univ_iff : IsGreatest univ a ↔ IsTop a

Proof state:
α : Type u
inst✝ : Preorder α
a : α
⊢ IsGreatest univ a ↔ IsTop a

Tactic:
simp [IsGreatest, mem_upperBounds, IsTop]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma latticeClosure_empty : latticeClosure (∅ : Set α) = ∅

Proof state:
α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure ∅ = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nat_mul_two_pi_sub_pi (n : ℕ) : cos (n * (2 * π) - π) = -1

Proof state:
n : ℕ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.clm_comp (hc : HasFDerivWithinAt c c' s x)
    (hd : HasFDerivWithinAt d d' s x) :
    HasFDerivWithinAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s 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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    s x

Tactic:
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp_hasFDerivWithinAt x <| hc.prod hd

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_neg (x : 𝕎 R) : truncateFun n (-x) = -truncateFun n x

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ truncateFun n (-x) = -truncateFun n x

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
theorem hexagon_forward (X Y Z : ModuleCat.{u} R) :
    (α_ X Y Z).hom ≫ (braiding X _).hom ≫ (α_ Y Z X).hom =
      (braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom

Proof state:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)

Proof state:
case hf
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)

Tactic:
apply TensorProduct.ext_threefold

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
intro x y z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_neg₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (y : F) : f (-x) y = -f x y

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : SeminormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x : M
y : F
⊢ (f (-x)) y = -(f x) y

Tactic:
rw [f.map_neg, neg_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) :
    l.head h = l.reverse.getLast (by simp_all)

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ l.head h = l.reverse.getLast ⋯

Tactic:
rw [← getLast_reverse]

Result:
no goals

Proof state:
α : Type ?u.313160
l : List α
h : l ≠ []
⊢ l.reverse ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_int_one_mod_four {n : ℤ} (hn : n % 4 = 1) : χ₄ n = 1

Proof state:
n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
rw [χ₄_int_mod_four, hn]

Result:
n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1

Proof state:
n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem principal_opow_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : Principal (· ^ ·) c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ Principal (fun x1 x2 => x1 ^ x2) c.ord

Tactic:
apply (isInitial_ord c).principal_opow

Result:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
rwa [omega0_le_ord]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem fundamentalDomain_stdBasis :
    fundamentalDomain (stdBasis K) =
        (Set.univ.pi fun _ => Set.Ico 0 1) ×ˢ
        (Set.univ.pi fun _ => Complex.measurableEquivPi⁻¹' (Set.univ.pi fun _ => Set.Ico 0 1))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ fundamentalDomain (stdBasis K) =
    (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ Set.univ.pi fun x => ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : mixedSpace K
⊢ x✝ ∈ fundamentalDomain (stdBasis K) ↔
    x✝ ∈
      (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ Set.univ.pi fun x => ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : mixedSpace K
⊢ x✝ ∈ fundamentalDomain (stdBasis K) ↔
    x✝ ∈
      (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ Set.univ.pi fun x => ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1

Tactic:
simp [stdBasis, mem_fundamentalDomain, Complex.measurableEquivPi]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_X_pow_mul : ∀ (n : ℕ), (X^n * p).smeval x = x^n * p.smeval x
  | 0 => by
    simp [npow_zero, one_mul]
  | n + 1 => by
    rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add,
      smeval_X_pow_assoc, npow_one]

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
⊢ (X ^ 0 * p).smeval x = x ^ 0 * p.smeval x

Tactic:
simp [npow_zero, one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x

Tactic:
rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add,
  smeval_X_pow_assoc, npow_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_subset_iUnion_closedBall_of_lt {α : Type*} [PseudoMetricSpace α] (E : Set α)
    {δ δ' : ℝ} (hδ₀ : 0 < δ') (hδδ' : δ < δ') : cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ'

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx

Result:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
y : α
hy₁ : y ∈ E
hy₂ : dist x y < δ'
⊢ x ∈ ⋃ x ∈ E, closedBall x δ'

Proof state:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
y : α
hy₁ : y ∈ E
hy₂ : dist x y < δ'
⊢ x ∈ ⋃ x ∈ E, closedBall x δ'

Tactic:
exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ'
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_eq_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succ a = succ b ↔ a = b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a = succ b ↔ a = b

Tactic:
rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
  succ_lt_succ_iff_of_not_isMax ha hb]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_multiset_prod_le : t.prod.degree ≤ (t.map Polynomial.degree).sum :=
  Quotient.inductionOn t (by simpa using degree_list_prod_le)

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum

Tactic:
simpa using degree_list_prod_le

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
/-- Any two `IsKleinFour` groups are isomorphic. -/
@[to_additive "Any two `IsAddKleinFour` groups are isomorphic."]
lemma nonempty_mulEquiv [IsKleinFour G₂] : Nonempty (G₁ ≃* G₂)

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
let _inst₁ := Fintype.ofFinite G₂

Result:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Nonempty (G₁ ≃* G₂)

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Fintype.card G₁ = Fintype.card G₂

Tactic:
simp

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ ((Fintype.equivOfCardEq ⋯).setValue 1 1) 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
classical
let _inst₁ := Fintype.ofFinite G₁
let _inst₁ := Fintype.ofFinite G₂
exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
let _inst₁ := Fintype.ofFinite G₁

Result:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
⊢ Nonempty (G₁ ≃* G₂)