harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toMonoidHom_injective : Injective (toMonoidHom : _ → α →* β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.setLIntegral_kernel {f : β → ℝ≥0∞} (hf : Measurable f) {s : Set β}
    (hs : MeasurableSet s) : Measurable fun a => ∫⁻ b in s, f b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (uncurry fun a => f)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β) in s, f b ∂κ a

Tactic:
refine Measurable.setLIntegral_kernel_prod_right ?_ hs

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (uncurry fun a => f)
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_log_mul_rpow_nhds_zero {r : ℝ} (hr : 0 < r) :
    Tendsto (fun x => log x * x ^ r) (𝓝[>] 0) (𝓝 0) :=
  (tendsto_log_div_rpow_nhds_zero <| neg_lt_zero.2 hr).congr' <|
    eventually_mem_nhdsWithin.mono fun x hx => by rw [rpow_neg hx.out.le, div_inv_eq_mul]

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ log x / x ^ (-r) = (fun x => log x * x ^ r) x

Tactic:
rw [rpow_neg hx.out.le, div_inv_eq_mul]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem isRoot_root (f : R[X]) : IsRoot (f.map (of f)) (root f)

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
⊢ (Polynomial.map (of f) f).IsRoot (root f)

Tactic:
rw [IsRoot, eval_map, eval₂_root]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem invOf_fromBlocks₁₁_eq (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
    (D : Matrix n n α) [Invertible A] [Invertible (D - C * ⅟ A * B)]
    [Invertible (fromBlocks A B C D)] :
    ⅟ (fromBlocks A B C D) =
      fromBlocks (⅟ A + ⅟ A * B * ⅟ (D - C * ⅟ A * B) * C * ⅟ A) (-(⅟ A * B * ⅟ (D - C * ⅟ A * B)))
        (-(⅟ (D - C * ⅟ A * B) * C * ⅟ A)) (⅟ (D - C * ⅟ A * B))

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₁₁Invertible B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)

Tactic:
convert (rfl : ⅟ (fromBlocks A B C D) = _)

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)

Tactic:
letI := fromBlocks₁₁Invertible A B C D

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₁₁Invertible B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_exact_iff_lTensor_exact :
    FaithfullyFlat R M ↔
    (∀ {N1 : Type max u v} [AddCommGroup N1] [Module R N1]
      {N2 : Type max u v} [AddCommGroup N2] [Module R N2]
      {N3 : Type max u v} [AddCommGroup N3] [Module R N3]
      (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
        Function.Exact l12 l23 ↔ Function.Exact (l12.lTensor M) (l23.lTensor M))

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
      [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
      [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)

Tactic:
simp only [iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact]

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_of_not_measurable (κ : Kernel α β) [IsSFiniteKernel κ]
    (hf : ¬Measurable (Function.uncurry f)) : withDensity κ f = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
exact dif_neg hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
classical exact dif_neg hf

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem head_ofSeq (s : Seq α) : head (ofSeq s) = Computation.pure s.head

Proof state:
α : Type u
s : Seq α
⊢ (↑s).head = Computation.pure s.head

Tactic:
simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]

Result:
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a => (a, ↑s.tail)) s.head) = Computation.pure s.head

Proof state:
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a => (a, ↑s.tail)) s.head) = Computation.pure s.head

Tactic:
cases Seq.head s <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem of_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃]
    (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (hF : W.IsInvertedBy F) (G : C₂ ⥤ C₃) :
    W.IsInvertedBy (F ⋙ G) := fun X Y f hf => by
  haveI := hF f hf
  dsimp
  infer_instance

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))

Tactic:
infer_instance

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)

Tactic:
dsimp

Result:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso ((F ⋙ G).map f)

Tactic:
haveI := hF f hf

Result:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.smul_even [Ring β] [AddCommGroup γ] [Module β γ] (hf : f.Odd) (hg : g.Even) :
    (f • g).Odd

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = -(f • g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = -(f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, neg_smul]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
lemma sum_pow_eq_sum_piAntidiag (s : Finset α) (f : α → R) (n : ℕ) :
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ piAntidiag s n, multinomial s k * ∏ i ∈ s, f i ^ k i

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * ∏ i ∈ s, f i ^ k i

Tactic:
simp_rw [← noncommProd_eq_prod]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ x ∈ s.piAntidiag n, ↑(multinomial s x) * s.noncommProd (fun i => f i ^ x i) ⋯

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ x ∈ s.piAntidiag n, ↑(multinomial s x) * s.noncommProd (fun i => f i ^ x i) ⋯

Tactic:
rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem factorThruKernelSubobject_comp_kernelSubobjectIso {W : C} (h : W ⟶ X) (w : h ≫ f = 0) :
    factorThruKernelSubobject f h w ≫ (kernelSubobjectIso f).hom = kernel.lift f h w :=
  (cancel_mono (kernel.ι f)).1 <| by simp

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (factorThruKernelSubobject f h w ≫ (kernelSubobjectIso f).hom) ≫ kernel.ι f = kernel.lift f h w ≫ kernel.ι f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift_inf {f : Filter α} {g h : Set α → Filter β} :
    (f.lift fun x => g x ⊓ h x) = f.lift g ⊓ f.lift h

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g h : Set α → Filter β
⊢ (f.lift fun x => g x ⊓ h x) = f.lift g ⊓ f.lift h

Tactic:
simp only [Filter.lift, iInf_inf_eq]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem StructureGroupoid.id_mem_maximalAtlas : PartialHomeomorph.refl H ∈ G.maximalAtlas H :=
  G.subset_maximalAtlas <| by simp

Proof state:
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ PartialHomeomorph.refl H ∈ atlas H H

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem strictMono_map_iff {f : α → β} :
    StrictMono (WithBot.map f) ↔ StrictMono f :=
  strictMono_iff.trans <| by simp [StrictMono, bot_lt_coe]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f

Tactic:
simp [StrictMono, bot_lt_coe]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.clm_apply (hc : HasDerivAt c c' x) (hu : HasDerivAt u u' x) :
    HasDerivAt (fun y => (c y) (u y)) (c' (u x) + c x u') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
this : HasDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x
⊢ HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
have := (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).hasDerivAt

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
this : HasDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x
⊢ HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_lt_top [Nontrivial M] [IsCoatomic (Submodule R M)] : jacobson R M < ⊤

Proof state:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsCoatomic (Submodule R M)
⊢ jacobson R M < ⊤

Tactic:
obtain ⟨m, hm, -⟩ := (eq_top_or_exists_le_coatom (⊥ : Submodule R M)).resolve_left bot_ne_top

Result:
case intro.intro
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsCoatomic (Submodule R M)
m : Submodule R M
hm : IsCoatom m
⊢ jacobson R M < ⊤

Proof state:
case intro.intro
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsCoatomic (Submodule R M)
m : Submodule R M
hm : IsCoatom m
⊢ jacobson R M < ⊤

Tactic:
exact (sInf_le <| Set.mem_setOf.mpr hm).trans_lt hm.1.lt_top

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse

Proof state:
α : Type ?u.56979
β : Type ?u.57027
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs.reverse → P a
⊢ pmap f xs.reverse H = (pmap f xs ⋯).reverse

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Invariant.lean
theorem smul_charpoly (b : B) (g : G) : g • (charpoly G b) = charpoly G b

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
g : G
⊢ g • charpoly G b = charpoly G b

Tactic:
rw [charpoly_eq_prod_smul, Finset.smul_prod_perm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_union {self : UnionFind} {x y : Fin self.size} :
    Equiv (union self x y) a b ↔
    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b

Proof state:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.parent ↑⟨self.rootD ↑x, ⋯⟩ = ↑⟨self.rootD ↑x, ⋯⟩

Tactic:
simp [← rootD_eq_self, rootD_rootD]

Result:
no goals

Proof state:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ (((self.find x).fst.find ⟨↑y, ⋯⟩).fst.link ⟨self.rootD ↑x, ⋯⟩ ((self.find x).fst.find ⟨↑y, ⋯⟩).2.val ⋯).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Tactic:
rw [equiv_link (by simp [← rootD_eq_self, rootD_rootD])]

Result:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a b ∨
      ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a ↑⟨self.rootD ↑x, ⋯⟩ ∧
          ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv (↑((self.find x).fst.find ⟨↑y, ⋯⟩).2.val) b ∨
        ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a ↑((self.find x).fst.find ⟨↑y, ⋯⟩).2.val ∧
          ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv (↑⟨self.rootD ↑x, ⋯⟩) b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Proof state:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a b ∨
      ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a ↑⟨self.rootD ↑x, ⋯⟩ ∧
          ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv (↑((self.find x).fst.find ⟨↑y, ⋯⟩).2.val) b ∨
        ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv a ↑((self.find x).fst.find ⟨↑y, ⋯⟩).2.val ∧
          ((self.find x).fst.find ⟨↑y, ⋯⟩).fst.Equiv (↑⟨self.rootD ↑x, ⋯⟩) b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Tactic:
simp [equiv_find]

Result:
no goals

Proof state:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ (self.union x y).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Tactic:
simp [union]

Result:
a b : Nat
self : UnionFind
x y : Fin self.size
⊢ (((self.find x).fst.find ⟨↑y, ⋯⟩).fst.link ⟨self.rootD ↑x, ⋯⟩ ((self.find x).fst.find ⟨↑y, ⋯⟩).2.val ⋯).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccAboveEquiv_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
    (finSuccAboveEquiv (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2)

Proof state:
n : ℕ
x : { x // x ≠ Fin.last n }
⊢ (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯

Tactic:
rw [← Option.some_inj]

Result:
n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some ((finSuccAboveEquiv (Fin.last n)).symm x) = some ((↑x).castLT ⋯)

Proof state:
n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some ((finSuccAboveEquiv (Fin.last n)).symm x) = some ((↑x).castLT ⋯)

Tactic:
simp [finSuccAboveEquiv]

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem addBottom_head_fst (L : ListBlank (∀ k, Option (Γ k))) : (addBottom L).head.1 = true

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom L).head.1 = true

Tactic:
rw [addBottom, ListBlank.head_cons]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.sub_le_dist (x y : ℝ) : x - y ≤ dist x y

Proof state:
x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)

Tactic:
exact Or.inl (le_refl _)

Result:
no goals

Proof state:
x y : ℝ
⊢ x - y ≤ dist x y

Tactic:
rw [Real.dist_eq, le_abs]

Result:
x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)
-- Mathlib/Data/Finset/Powerset.lean
theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
    (s.powersetCard i).val.map Finset.val = s.1.powersetCard i

Proof state:
α : Type u_1
s : Finset α
i : ℕ
⊢ Multiset.map val (powersetCard i s).val = Multiset.powersetCard i s.val

Tactic:
simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem Iso.symm_apply_reachable {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V}
    {v : V'} : G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)

Tactic:
rw [← Iso.reachable_iff, RelIso.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem τ_symm_apply_fromCoset :
    Equiv.symm τ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = ∞

Proof state:
A B : Grp
f : A ⟶ B
⊢ (Equiv.symm τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = ∞

Tactic:
rw [tau, Equiv.symm_swap, Equiv.swap_apply_left]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[simp] protected lemma zero_smul (s : AddSubgroup M) : (0 : R) • s = ⊥

Proof state:
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : AddSubgroup M
⊢ 0 • s = ⊥

Tactic:
simp [eq_bot_iff_forall, pointwise_smul_def]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pdiv [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : IsMultiplicative f)
    (hg : IsMultiplicative g) : IsMultiplicative (pdiv f g) :=
  ⟨ by simp [hf, hg], fun {m n} cop => by
    simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop,
      div_eq_mul_inv, mul_inv]
    apply mul_mul_mul_comm ⟩

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f.pdiv g) 1 = 1

Tactic:
simp [hf, hg]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ (f.pdiv g) (m * n) = (f.pdiv g) m * (f.pdiv g) n

Tactic:
simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop,
  div_eq_mul_inv, mul_inv]

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ f m * f n * ((g m)⁻¹ * (g n)⁻¹) = f m * (g m)⁻¹ * (f n * (g n)⁻¹)

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ f m * f n * ((g m)⁻¹ * (g n)⁻¹) = f m * (g m)⁻¹ * (f n * (g n)⁻¹)

Tactic:
apply mul_mul_mul_comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
    m * n / (m * k) = n / k

Proof state:
m n k : Nat
H : 0 < m
⊢ m * n / (m * k) = n / k

Tactic:
rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_C (r : R) : contract p (C r) = C r

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
r : R
⊢ contract p (C r) = C r

Tactic:
simp [contract]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_map_iff {f g : α → β} {l : Vector α n} :
    map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f g : α → β
l : Vector α n
⊢ map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem add_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) :
    (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x + y) ᵥ* A) x✝ = (x ᵥ* A + y ᵥ* A) x✝

Tactic:
apply add_dotProduct

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
⊢ (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x + y) ᵥ* A) x✝ = (x ᵥ* A + y ᵥ* A) x✝
-- Mathlib/Data/Matroid/Dual.lean
theorem base_iff_dual_isBase_compl (hB : B ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.IsBase B ↔ M✶.IsBase (M.E \ B)

Tactic:
rw [dual_isBase_iff, diff_diff_cancel_left hB]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_eq_empty_iff : Ico a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]

Result:
no goals