harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma LFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
    LFunction Φ s = N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ LFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Tactic:
simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ↑N ^ (-s) *
      (∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s) =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ↑N ^ (-s) *
      (∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s) =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Tactic:
congr 1

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s =
    ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s =
    ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s

Tactic:
simp only [add_right_eq_self, ← neg_eq_self ℂ, ← sum_neg_distrib]

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ x : ZMod N, -(Φ x * hurwitzZetaOdd (toAddCircle x) s) = ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ x : ZMod N, -(Φ x * hurwitzZetaOdd (toAddCircle x) s) = ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s

Tactic:
refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
i : ZMod N
⊢ -(Φ i * hurwitzZetaOdd (toAddCircle i) s) =
    Φ ((Equiv.neg (ZMod N)) i) * hurwitzZetaOdd (toAddCircle ((Equiv.neg (ZMod N)) i)) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
i : ZMod N
⊢ -(Φ i * hurwitzZetaOdd (toAddCircle i) s) =
    Φ ((Equiv.neg (ZMod N)) i) * hurwitzZetaOdd (toAddCircle ((Equiv.neg (ZMod N)) i)) s

Tactic:
simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaOdd_neg, mul_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
lemma isSheaf_iff_of_nat_equiv :
    Presieve.IsSheaf J P₁ ↔ Presieve.IsSheaf J P₂ :=
  ⟨fun hP₁ ↦ isSheaf_of_nat_equiv e he hP₁,
    fun hP₂ ↦
      isSheaf_of_nat_equiv (fun _ ↦ (@e _).symm) (fun X Y f x ↦ by
        obtain ⟨y, rfl⟩ := e.surjective x
        refine e.injective ?_
        simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, he]) hP₂⟩

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)
hP₂ : IsSheaf J P₂
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ ((fun x => e.symm) X) (P₂.map f.op (e y)) = P₁.map f.op (((fun x => e.symm) Y) (e y))

Tactic:
refine e.injective ?_

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)
hP₂ : IsSheaf J P₂
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ e (((fun x => e.symm) X) (P₂.map f.op (e y))) = e (P₁.map f.op (((fun x => e.symm) Y) (e y)))

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)
hP₂ : IsSheaf J P₂
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ e (((fun x => e.symm) X) (P₂.map f.op (e y))) = e (P₁.map f.op (((fun x => e.symm) Y) (e y)))

Tactic:
simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, he]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)
hP₂ : IsSheaf J P₂
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ ((fun x => e.symm) X) (P₂.map f.op x) = P₁.map f.op (((fun x => e.symm) Y) x)

Tactic:
obtain ⟨y, rfl⟩ := e.surjective x

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)
hP₂ : IsSheaf J P₂
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ ((fun x => e.symm) X) (P₂.map f.op (e y)) = P₁.map f.op (((fun x => e.symm) Y) (e y))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem map_attach {l : Array α} (f : { x // x ∈ l } → β) :
    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id)

Proof state:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : { x // x ∈ { toList := toList✝ } } → β
⊢ map f { toList := toList✝ }.attach = pmap (fun a h => f ⟨a, h⟩) { toList := toList✝ } ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : { x // x ∈ l } → β
⊢ map f l.attach = pmap (fun a h => f ⟨a, h⟩) l ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : { x // x ∈ { toList := toList✝ } } → β
⊢ map f { toList := toList✝ }.attach = pmap (fun a h => f ⟨a, h⟩) { toList := toList✝ } ⋯
-- Mathlib/Algebra/Group/End.lean
theorem mem_iff_ofSubtype_apply_mem (f : Perm (Subtype p)) (x : α) :
    p x ↔ p ((ofSubtype f : α → α) x) :=
  if h : p x then by
    simpa only [h, true_iff, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2
  else by simp [h, ofSubtype_apply_of_not_mem f h]

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p x ↔ p ((ofSubtype f) x)

Tactic:
simpa only [h, true_iff, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p x ↔ p ((ofSubtype f) x)

Tactic:
simp [h, ofSubtype_apply_of_not_mem f h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblZ_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
    (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) : W'.dblZ P = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_cancel_left (m : M) (s₁ s₂ : S) : mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₂)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₂)

Tactic:
rw [LocalizedModule.mk_cancel_common_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_filterMap (xs : Array α) (f : α → Option β) (p : β → Bool) :
    (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f

Proof state:
α : Type u_1
β : Type u_2
xs : Array α
f : α → Option β
p : β → Bool
⊢ find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f

Tactic:
cases xs

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
toList✝ : List α
⊢ find? p (filterMap f { toList := toList✝ }) = (find? (fun a => Option.any p (f a)) { toList := toList✝ }).bind f

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
toList✝ : List α
⊢ find? p (filterMap f { toList := toList✝ }) = (find? (fun a => Option.any p (f a)) { toList := toList✝ }).bind f

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isOpen_empty : IsOpen (∅ : Set X)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen ∅

Tactic:
rw [← sUnion_empty]

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen (⋃₀ ∅)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen (⋃₀ ∅)

Tactic:
exact isOpen_sUnion fun a => False.elim

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma Complex.coe_selfAdjointEquiv (z : selfAdjoint ℂ) :
    (selfAdjointEquiv z : ℂ) = z

Proof state:
z : ↥(selfAdjoint ℂ)
⊢ ↑(selfAdjointEquiv z) = ↑z

Tactic:
simpa [selfAdjointEquiv_symm_apply]
  using (congr_arg Subtype.val <| Complex.selfAdjointEquiv.left_inv z)

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem qRight_one_right (t : I) : qRight (t, 1) = t :=
  Eq.trans (by rw [qRight]; norm_num) <| Set.projIcc_val zero_le_one _

Proof state:
t : ↑I
⊢ Set.projIcc 0 1 qRight.proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t

Tactic:
norm_num

Result:
no goals

Proof state:
t : ↑I
⊢ qRight (t, 1) = Set.projIcc 0 1 ⋯ ↑t

Tactic:
rw [qRight]

Result:
t : ↑I
⊢ Set.projIcc 0 1 qRight.proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t
-- Mathlib/Data/Multiset/Count.lean
theorem count_pos {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 0 < count a s ↔ a ∈ s

Tactic:
simp [count, countP_pos]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_eval (p : ℕ) (P : R[X]) (r : R) : eval r (expand R p P) = eval (r ^ p) P

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
⊢ eval r ((expand R p) P) = eval (r ^ p) P

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)

Tactic:
rw [map_add, eval_add, eval_add, hf, hg]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r ((expand R p) (C a * X ^ n)) = eval (r ^ p) (C a * X ^ n)
⊢ eval r ((expand R p) (C a * X ^ (n + 1))) = eval (r ^ p) (C a * X ^ (n + 1))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r a : R
⊢ eval r ((expand R p) (C a)) = eval (r ^ p) (C a)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@[reassoc (attr := simp)]
lemma pOpcycles_comp_fromLeftDerivedZero' {C} [Category C] [Abelian C] {X : C}
    (P : ProjectiveResolution X) (F : C ⥤ D) [F.Additive] :
    HomologicalComplex.pOpcycles _ _ ≫ P.fromLeftDerivedZero' F = F.map (P.π.f 0)

Proof state:
D : Type u_1
inst✝⁴ : Category.{u_4, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Abelian C
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0 ≫ P.fromLeftDerivedZero' F =
    F.map (P.π.f 0)

Tactic:
simp [fromLeftDerivedZero']

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
lemma trace_mul_cycle' (f g h : M →ₗ[R] M) :
    trace R M (f * (g * h)) = trace R M (h * (f * g))

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) = (trace R M) (h * (f * g))

Tactic:
rw [← mul_assoc, LinearMap.trace_mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_insert (l : List α) (a : α) (w) :
    (l.insert a).head w = if h : a ∈ l then l.head (ne_nil_of_mem h) else a

Proof state:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
w : List.insert a l ≠ []
⊢ some ((List.insert a l).head w) = some (if h : a ∈ l then l.head ⋯ else a)

Tactic:
rw [← head?_eq_head, head?_insert]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
w : List.insert a l ≠ []
⊢ (List.insert a l).head w = if h : a ∈ l then l.head ⋯ else a

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
w : List.insert a l ≠ []
⊢ some ((List.insert a l).head w) = some (if h : a ∈ l then l.head ⋯ else a)
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem map (f : R →+* S) (n ν : ℕ) :
    (bernsteinPolynomial R n ν).map f = bernsteinPolynomial S n ν

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n ν : ℕ
⊢ Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν

Tactic:
simp [bernsteinPolynomial]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Restriction.isBase_iff_of_spanning {N : Matroid α} (hR : N ≤r M) (hN : M.Spanning N.E) :
    N.IsBase B ↔ (M.IsBase B ∧ B ⊆ N.E)

Proof state:
α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E

Tactic:
obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR

Result:
case intro.intro
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E

Tactic:
rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false

Proof state:
bs : List Bool
i : Nat
⊢ (ofBoolListLE bs).getLsbD i = bs.getD i false

Tactic:
induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem bind_smallSets_gc :
    GaloisConnection (fun L : Filter (Set α) ↦ L.bind principal) smallSets

Proof state:
α : Type u_1
⊢ GaloisConnection (fun L => L.bind 𝓟) smallSets

Tactic:
intro L l

Result:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ (fun L => L.bind 𝓟) L ≤ l ↔ L ≤ l.smallSets

Proof state:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ (fun L => L.bind 𝓟) L ≤ l ↔ L ≤ l.smallSets

Tactic:
simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]

Result:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem isCycle_cycleOf (f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) :
    IsCycle (cycleOf f x) :=
  have : cycleOf f x x ≠ x

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
⊢ (f.cycleOf x) x ≠ x

Tactic:
rwa [SameCycle.rfl.cycleOf_apply]

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f.cycleOf x ^ i) x = y

Tactic:
rw [cycleOf_zpow_apply_self, hi]

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
exact (h rfl).elim

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hxy] at h

Result:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y
-- Mathlib/LinearAlgebra/SModEq.lean
theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ x ≡ y [SMOD ⊥] ↔ x = y

Tactic:
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivAt.unique (h₀ : HasFDerivAt f f₀' x) (h₁ : HasFDerivAt f f₁' x) : f₀' = f₁'

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h₀ : HasFDerivWithinAt f f₀' univ x
h₁ : HasFDerivWithinAt f f₁' univ x
⊢ f₀' = f₁'

Tactic:
exact uniqueDiffWithinAt_univ.eq h₀ h₁

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h₀ : HasFDerivAt f f₀' x
h₁ : HasFDerivAt f f₁' x
⊢ f₀' = f₁'

Tactic:
rw [← hasFDerivWithinAt_univ] at h₀ h₁

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h₀ : HasFDerivWithinAt f f₀' univ x
h₁ : HasFDerivWithinAt f f₁' univ x
⊢ f₀' = f₁'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none

Proof state:
α : Type u_1
a : Array α
i : Nat
h : a.size ≤ i
⊢ a[i]? = none

Tactic:
simp [getElem?_neg, h]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem mono_iff_injective {n m : SimplexCategory} {f : n ⟶ m} :
    Mono f ↔ Function.Injective f.toOrderHom

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]

Result:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
  NonemptyFinLinOrd.mono_iff_injective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

Result:
no goals

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor]

Result:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)
-- Mathlib/Algebra/Homology/HomotopyCategory.lean
theorem NatTrans.mapHomotopyCategory_comp (c : ComplexShape ι) {F G H : V ⥤ W} [F.Additive]
    [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) :
    NatTrans.mapHomotopyCategory (α ≫ β) c =
      NatTrans.mapHomotopyCategory α c ≫ NatTrans.mapHomotopyCategory β c

Proof state:
ι : Type u_2
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
W : Type u_3
inst✝⁴ : Category.{u_4, u_3} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
⊢ mapHomotopyCategory (α ≫ β) c = mapHomotopyCategory α c ≫ mapHomotopyCategory β c

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/EpiMono.lean
lemma prop_X₁_of_shortExact [HasZeroMorphisms C] {S : ShortComplex C} (hS : S.ShortExact)
    (h₂ : P S.X₂) : P S.X₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Mono S.f
⊢ P S.X₁

Tactic:
exact P.prop_of_mono S.f h₂

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₁

Tactic:
have := hS.mono_f

Result:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Mono S.f
⊢ P S.X₁
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Tactic:
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]

Result:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c

Tactic:
exact himp_inf_le.trans le_himp_himp

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem IsOrtho.zero_right (x : M) : IsOrtho Q x (0 : M)

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q.IsOrtho x 0

Tactic:
simp [isOrtho_def]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setAverage_eq (f : α → E) (s : Set α) :
    ⨍ x in s, f x ∂μ = (μ s).toReal⁻¹ • ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
⊢ ⨍ (x : α) in s, f x ∂μ = (μ s).toReal⁻¹ • ∫ (x : α) in s, f x ∂μ

Tactic:
rw [average_eq, restrict_apply_univ]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_equiv_neg_iff {x y : PGame} : -x ≈ -y ↔ x ≈ y

Proof state:
x y : PGame
⊢ (-x).Equiv (-y) ↔ x.Equiv y

Tactic:
rw [Equiv, Equiv, neg_le_neg_iff, neg_le_neg_iff, and_comm]

Result:
no goals

Proof state:
x y : PGame
⊢ -x ≈ -y ↔ x ≈ y

Tactic:
show Equiv (-x) (-y) ↔ Equiv x y

Result:
x y : PGame
⊢ (-x).Equiv (-y) ↔ x.Equiv y
-- Mathlib/Data/List/Map2.lean
theorem zipWith_nil (f : α → β → γ) (l : List α) : zipWith f l [] = []

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_zmod (n : ℕ) : Nat.card (ZMod n) = n

Proof state:
case zero

⊢ Nat.card (ZMod 0) = 0

Tactic:
exact @Nat.card_eq_zero_of_infinite _ Int.infinite

Result:
no goals

Proof state:
n : ℕ
⊢ Nat.card (ZMod n) = n

Tactic:
cases n

Result:
case zero

⊢ Nat.card (ZMod 0) = 0

case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1

Proof state:
case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1

Tactic:
rw [Nat.card_eq_fintype_card, ZMod.card]

Result:
no goals