harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem biproduct_ι_comp_rightDistributor_inv {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
    biproduct.ι _ j ≫ (rightDistributor f X).inv = biproduct.ι _ j ▷ X

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j => f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X

Tactic:
simp [rightDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc,
  dite_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j => f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X

Tactic:
classical
simp [rightDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc,
  dite_comp]

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_mod_two (b n) : bit b n % 2 = b.toNat

Proof state:
b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat

Tactic:
cases b <;> simp [bit_val, mul_add_mod]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_dvd_prod_of_subset {ι M : Type*} [CommMonoid M] (s t : Finset ι) (f : ι → M)
    (h : s ⊆ t) : (∏ i ∈ s, f i) ∣ ∏ i ∈ t, f i :=
  Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| by simpa

Proof state:
ι : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s t : Finset ι
f : ι → M
h : s ⊆ t
⊢ s.val ≤ t.val

Tactic:
simpa

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem isClosed_iff_zeroLocus (Z : Set (ProjectiveSpectrum 𝒜)) :
    IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem ACF_zero_realize_iff_infinite_ACF_prime_realize {φ : Language.ring.Sentence} :
    Theory.ACF 0 ⊨ᵇ φ ↔ Set.Infinite { p : Nat.Primes | Theory.ACF p ⊨ᵇ φ }

Proof state:
φ : Language.ring.Sentence
⊢ ¬Theory.ACF 0 ⊨ᵇ φ → ¬{p | Theory.ACF ↑p ⊨ᵇ φ}.Infinite

Tactic:
simpa [(ACF_isComplete (Or.inr rfl)).models_not_iff,
    fun p : Nat.Primes => (ACF_isComplete (Or.inl p.2)).models_not_iff] using
  finite_ACF_prime_not_realize_of_ACF_zero_realize φ.not

Result:
no goals

Proof state:
φ : Language.ring.Sentence
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ {p | Theory.ACF ↑p ⊨ᵇ φ}.Infinite

Tactic:
refine ⟨fun h => Set.infinite_of_finite_compl
    (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h),
  not_imp_not.1 ?_⟩

Result:
φ : Language.ring.Sentence
⊢ ¬Theory.ACF 0 ⊨ᵇ φ → ¬{p | Theory.ACF ↑p ⊨ᵇ φ}.Infinite
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma eq_C_of_isEmpty [IsEmpty σ] (p : MvPolynomial σ R) :
    p = C (p.coeff 0)

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ p = C (coeff 0 p)

Tactic:
obtain ⟨x, rfl⟩ := C_surjective σ p

Result:
case intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x : R
⊢ C x = C (coeff 0 (C x))

Proof state:
case intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x : R
⊢ C x = C (coeff 0 (C x))

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndepOn_sUnion_of_directed {s : Set (Set ι)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃ i, ↑i)

Tactic:
exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ (i : ↑s), LinearIndepOn R v ↑i

Tactic:
simpa using h

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃₀ s)

Tactic:
rw [sUnion_eq_iUnion]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃ i, ↑i)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma fin3_def (P : Fin 3 → R) : ![P x, P y, P z] = P

Proof state:
case h
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n

Tactic:
fin_cases n <;> rfl

Result:
no goals

Proof state:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P

Tactic:
ext n

Result:
case h
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma reflection_perm_sq :
    P.reflection_perm i ^ 2 = 1

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ P.reflection_perm i ^ 2 = 1

Tactic:
ext j

Result:
case H
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflection_perm i ^ 2) j = 1 j

Proof state:
case H.a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root ((P.reflection_perm i ^ 2) j) = P.root (1 j)

Tactic:
simp only [sq, Equiv.Perm.mul_apply, root_reflection_perm, reflection_same, Equiv.Perm.one_apply]

Result:
no goals

Proof state:
case H
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflection_perm i ^ 2) j = 1 j

Tactic:
apply P.root.injective

Result:
case H.a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root ((P.reflection_perm i ^ 2) j) = P.root (1 j)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
@[simp]
lemma singularPart_singularPart (μ ν : Measure α) :
    (μ.singularPart ν).singularPart ν = μ.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact Measure.mutuallySingular_singularPart _ _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).singularPart ν = μ.singularPart ν

Tactic:
rw [Measure.singularPart_eq_self]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_uIcc (ha : a ≠ 0) (b c : α) :
    (· * a) ⁻¹' [[b, c]] = [[b / a, c / a]] :=
  (lt_or_gt_of_ne ha).elim
    (fun h => by
      simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos])
    fun ha : 0 < a => by simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha✝ : a ≠ 0
b c : α
ha : 0 < a
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]

Tactic:
simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]

Result:
no goals

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

Tactic:
simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem max_eq_left {a b : Int} (h : b ≤ a) : max a b = a

Proof state:
a b : Int
h : b ≤ a
⊢ max b a = a

Tactic:
exact Int.max_eq_right h

Result:
no goals

Proof state:
a b : Int
h : b ≤ a
⊢ max a b = a

Tactic:
rw [← Int.max_comm b a]

Result:
a b : Int
h : b ≤ a
⊢ max b a = a
-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem comp (hg : IsLocalHomeomorphOn g t) (hf : IsLocalHomeomorphOn f s)
    (h : Set.MapsTo f s t) : IsLocalHomeomorphOn (g ∘ f) s

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
⊢ IsLocalHomeomorphOn (g ∘ f) s

Tactic:
intro x hx

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : PartialHomeomorph Y Z
hg : IsLocalHomeomorphOn (↑eg) t
ef : PartialHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocalHomeomorphOn (↑ef) s
h : Set.MapsTo (↑ef) s t
hxg : ↑ef x ∈ eg.source
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ ↑ef = ↑e

Tactic:
exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : PartialHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocalHomeomorphOn (↑eg) t
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ f = ↑e

Tactic:
obtain ⟨ef, hxf, rfl⟩ := hf x hx

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : PartialHomeomorph Y Z
hg : IsLocalHomeomorphOn (↑eg) t
ef : PartialHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocalHomeomorphOn (↑ef) s
h : Set.MapsTo (↑ef) s t
hxg : ↑ef x ∈ eg.source
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ ↑ef = ↑e

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e

Tactic:
obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)

Result:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : PartialHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocalHomeomorphOn (↑eg) t
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ f = ↑e
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_take : ∀ {s}, Valid s → ∀ n, (s.take n).toString.1 = s.toString.1.take n
  | _, h, _ => let ⟨_, _, _, h⟩ := h.validFor; by simp [(h.take _).toString, h.toString]

Proof state:
x✝¹ : Substring
h✝ : x✝¹.Valid
x✝ : Nat
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝¹
⊢ (x✝¹.take x✝).toString.data = List.take x✝ x✝¹.toString.data

Tactic:
simp [(h.take _).toString, h.toString]

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
@[simp] lemma dirSupInacc_compl : DirSupInacc sᶜ ↔ DirSupClosed s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ DirSupInacc sᶜ ↔ DirSupClosed s

Tactic:
simp [DirSupInacc, DirSupClosed, ← not_disjoint_iff_nonempty_inter, not_imp_not,
  disjoint_compl_right_iff]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem card {R : Type*} [Fintype R] :
    Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n

Proof state:
p n : ℕ
R : Type u_2
inst✝ : Fintype R
⊢ Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n

Tactic:
simp only [TruncatedWittVector, Fintype.card_fin, Fintype.card_fun]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem filter_card_add_filter_neg_card_eq_card
    (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
    #(s.filter p) + #(s.filter fun a ↦ ¬ p a) = #s

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #(filter (fun a => ¬p a) s) = #s

Tactic:
rw [← card_union_of_disjoint (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #(filter (fun a => ¬p a) s) = #s

Tactic:
classical
rw [← card_union_of_disjoint (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem exists_measurableSet_indicator (hf : UnifTight f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε :=
  let ⟨s, hμs, hsm, hfs⟩ := (hf.eventually_cofinite_indicator hε).exists_measurable_mem_of_smallSets
  ⟨sᶜ, hsm.compl, hμs, by rwa [compl_compl s]⟩

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
s : Set α
hμs : s ∈ μ.cofinite
hsm : MeasurableSet s
hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
⊢ ∀ (i : ι), eLpNorm (sᶜᶜ.indicator (f i)) p μ ≤ ε

Tactic:
rwa [compl_compl s]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem rel_reverse : (Forall₂ R ⇒ Forall₂ R) reverse reverse
  | [], [], Forall₂.nil => Forall₂.nil
  | _, _, Forall₂.cons h₁ h₂ => by
    simp only [reverse_cons]
    exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (a✝ :: l₁✝).reverse (b✝ :: l₂✝).reverse

Tactic:
simp only [reverse_cons]

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (l₁✝.reverse ++ [a✝]) (l₂✝.reverse ++ [b✝])

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (l₁✝.reverse ++ [a✝]) (l₂✝.reverse ++ [b✝])

Tactic:
exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

Result:
no goals
-- Mathlib/NumberTheory/Wilson.lean
theorem prime_iff_fac_equiv_neg_one (h : n ≠ 1) : Prime n ↔ ((n - 1)! : ZMod n) = -1

Proof state:
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ ↑(n - 1)! = -1

Tactic:
haveI := Fact.mk h1

Result:
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ ↑(n - 1)! = -1

Proof state:
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ ↑(n - 1)! = -1

Tactic:
exact ZMod.wilsons_lemma n

Result:
no goals

Proof state:
n : ℕ
h : n ≠ 1
⊢ Prime n ↔ ↑(n - 1)! = -1

Tactic:
refine ⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩

Result:
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ ↑(n - 1)! = -1
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem isometry_iff_nndist_eq [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
    Isometry f ↔ ∀ x y, nndist (f x) (f y) = nndist x y

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y

Tactic:
simp only [Isometry, edist_nndist, ENNReal.coe_inj]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
theorem norm_indicator_le_norm_self : ‖indicator s f a‖ ≤ ‖f a‖

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖f a‖

Tactic:
rw [norm_indicator_eq_indicator_norm]

Result:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖) a ≤ ‖f a‖

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖) a ≤ ‖f a‖

Tactic:
apply indicator_norm_le_norm_self

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem spanPoints_nonempty (s : Set P) : (spanPoints k s).Nonempty ↔ s.Nonempty

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ (spanPoints k s).Nonempty ↔ s.Nonempty

Tactic:
constructor

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ (spanPoints k s).Nonempty → s.Nonempty

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ s.Nonempty → (spanPoints k s).Nonempty

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ (spanPoints k s).Nonempty → s.Nonempty

Tactic:
contrapose

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ¬s.Nonempty → ¬(spanPoints k s).Nonempty

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : s = ∅
⊢ spanPoints k s = ∅

Tactic:
simp [h, spanPoints]

Result:
no goals

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ s = ∅ → spanPoints k s = ∅

Tactic:
intro h

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : s = ∅
⊢ spanPoints k s = ∅

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ¬s.Nonempty → ¬(spanPoints k s).Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ s = ∅ → spanPoints k s = ∅

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ s.Nonempty → (spanPoints k s).Nonempty

Tactic:
exact fun h => h.mono (subset_spanPoints _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem unitOfList_singleton {k : α} :
    unitOfList [k] = (∅ : Raw α (fun _ => Unit)).insertIfNew k ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty [k]).val.val = (Raw₀.insertIfNew ⟨Raw₀.empty.val, ⋯⟩ k ()).val

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
⊢ unitOfList [k] = ∅.insertIfNew k ()

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty [k]).val.val = (Raw₀.insertIfNew ⟨Raw₀.empty.val, ⋯⟩ k ()).val
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma integrable (f : 𝓢(D, V)) : Integrable f μ :=
  (f.integrable_pow_mul μ 0).mono f.continuous.aestronglyMeasurable
    (Eventually.of_forall (fun _ ↦ by simp))

Proof state:
D : Type u_3
V : Type u_7
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
x✝ : D
⊢ ‖f x✝‖ ≤ ‖‖x✝‖ ^ 0 * ‖f x✝‖‖

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem BinaryBiconeMorphism.ext {P Q : C} {c c' : BinaryBicone P Q}
    (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Result:
case mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w : { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom = g.hom
⊢ { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ } = g

Proof state:
case mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w : { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom = g.hom
⊢ { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ } = g

Tactic:
cases g

Result:
case mk.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
hom✝¹ : c.pt ⟶ c'.pt
wfst✝¹ : hom✝¹ ≫ c'.fst = c.fst
wsnd✝¹ : hom✝¹ ≫ c'.snd = c.snd
winl✝¹ : c.inl ≫ hom✝¹ = c'.inl
winr✝¹ : c.inr ≫ hom✝¹ = c'.inr
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w :
  { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ }.hom =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom
⊢ { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ } =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }

Proof state:
case mk.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
hom✝¹ : c.pt ⟶ c'.pt
wfst✝¹ : hom✝¹ ≫ c'.fst = c.fst
wsnd✝¹ : hom✝¹ ≫ c'.snd = c.snd
winl✝¹ : c.inl ≫ hom✝¹ = c'.inl
winr✝¹ : c.inr ≫ hom✝¹ = c'.inr
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w :
  { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ }.hom =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom
⊢ { hom := hom✝¹, wfst := wfst✝¹, wsnd := wsnd✝¹, winl := winl✝¹, winr := winr✝¹ } =
    { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem mem_support_seq_iff : b ∈ (seq q p).support ↔ ∃ f ∈ q.support, b ∈ f '' p.support

Proof state:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ b ∈ (q.seq p).support ↔ ∃ f ∈ q.support, b ∈ f '' p.support

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem countP_eq_card {s} : countP p s = card s ↔ ∀ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_length]

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = card (Quot.mk (⇑(isSetoid α)) _l) ↔ ∀ a ∈ Quot.mk (⇑(isSetoid α)) _l, p a

Tactic:
simp [List.countP_eq_length]

Result:
no goals