harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMinOn.fderivWithin_eq_zero (h : IsLocalMinOn f s a)
    (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) :
    (fderivWithin ℝ f s a : E → ℝ) y = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
exact if hf : DifferentiableWithinAt ℝ f s a then
  h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
classical
exact if hf : DifferentiableWithinAt ℝ f s a then
  h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem preimage_comp (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :
    F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g :=
  F.map_injective (by simp)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.isRight = false ↔ x.isLeft = true

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasFDerivAt_apply (i : ι) (f : ∀ i, F' i) :
    HasFDerivAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) f

Proof state:
case hf
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Tactic:
apply hasStrictFDerivAt_apply

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ HasFDerivAt (fun f => f i) (proj i) f

Tactic:
apply HasStrictFDerivAt.hasFDerivAt

Result:
case hf
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f
-- Mathlib/Data/Rat/Lemmas.lean
theorem mul_den_dvd (q₁ q₂ : ℚ) : (q₁ * q₂).den ∣ q₁.den * q₂.den

Proof state:
case h
q₁ q₂ : ℚ
⊢ (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den

Tactic:
apply Nat.gcd_dvd_right

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣
    q₁.den * q₂.den

Tactic:
apply Nat.div_dvd_of_dvd

Result:
case h
q₁ q₂ : ℚ
⊢ (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den

Proof state:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
rw [mul_def, normalize_eq]

Result:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣
    q₁.den * q₂.den
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_le_nmul_right (h : a ≤ b) (c) : a ⨳ c ≤ b ⨳ c

Proof state:
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
⊢ a ⨳ c ≤ b ⨳ c

Tactic:
rw [nmul_comm, nmul_comm b]

Result:
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
⊢ c ⨳ a ≤ c ⨳ b

Proof state:
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
⊢ c ⨳ a ≤ c ⨳ b

Tactic:
exact nmul_le_nmul_left h c

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp] lemma inter_univ (s : Finset α) : s ∩ univ = s

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ s ∩ univ = s

Tactic:
rw [inter_comm, univ_inter]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_polynomialY : (W'.map f).toAffine.polynomialY = W'.polynomialY.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ (map W' f).toAffine.polynomialY = Polynomial.map (mapRingHom f) W'.polynomialY

Tactic:
simp only [polynomialY]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ C (C 2) * Y + C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) =
    Polynomial.map (mapRingHom f) (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃))

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ C (C 2) * Y + C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) =
    Polynomial.map (mapRingHom f) (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃))

Tactic:
map_simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_inf : (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet

Proof state:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet

Tactic:
ext ⟨x, y⟩

Result:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet

Proof state:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_basis_right' {ι : Type*} (n : Basis ι R N)
    (H : Function.Injective (mulRightMap M n)) : M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : Function.Injective ⇑(M.mulRightMap ⇑n)
⊢ M.LinearDisjoint N

Tactic:
simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : Function.Injective ⇑(M.mulMap N)
⊢ M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : Function.Injective ⇑(M.mulRightMap ⇑n)
⊢ M.LinearDisjoint N

Tactic:
classical simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
  ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
  LinearEquiv.coe_coe, EquivLike.injective_comp] at H

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : Function.Injective ⇑(M.mulMap N)
⊢ M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : Function.Injective ⇑(M.mulMap N)
⊢ M.LinearDisjoint N

Tactic:
exact ⟨H⟩

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma map_hom_inv_id_eval_app (e : X ≅ Y) (F : C ⥤ D ⥤ E) (j : J) (Y : D) :
    (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{u_5, u_1} C
inst✝¹ : Category.{u_7, u_2} D
inst✝ : Category.{u_6, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)

Tactic:
rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
  Functor.map_id, NatTrans.id_app]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_insert {α : Type u} {s : Set α} {a : α} (h : a ∉ s) :
    #(insert a s : Set α) = #s + 1

Proof state:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) = #↑s + 1

Tactic:
rw [← union_singleton, mk_union_of_disjoint, mk_singleton]

Result:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}

Proof state:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
lemma trace_blockDiagonal' [DecidableEq p] {m : p → Type*} [∀ i, Fintype (m i)]
    (M : ∀ i, Matrix (m i) (m i) R) :
    trace (blockDiagonal' M) = ∑ i, trace (M i)

Proof state:
p : Type u_4
R : Type u_6
inst✝³ : Fintype p
inst✝² : AddCommMonoid R
inst✝¹ : DecidableEq p
m : p → Type u_8
inst✝ : (i : p) → Fintype (m i)
M : (i : p) → Matrix (m i) (m i) R
⊢ (blockDiagonal' M).trace = ∑ i : p, (M i).trace

Tactic:
simp [blockDiagonal', trace, Finset.sum_sigma']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_C (r : R) : (C r).smeval x = r • 1

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ (C r).smeval x = r • 1

Tactic:
rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
theorem aux_ι (m₁ m₂ : M) : aux f ((even.ι Q).bilin m₁ m₂) = f.bilin m₁ m₂ :=
  (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans
    (by
      rw [foldr_ι, foldr_ι]
      exact mul_one _)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯)
          (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ((CliffordAlgebra.ι Q) m₂)))
        ((CliffordAlgebra.ι Q) m₁)).1 =
    (f.bilin m₁) m₂

Tactic:
rw [foldr_ι, foldr_ι]

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (((CliffordAlgebra.even.lift.fFold f) m₁) (((CliffordAlgebra.even.lift.fFold f) m₂) (1, 0))).1 = (f.bilin m₁) m₂

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (((CliffordAlgebra.even.lift.fFold f) m₁) (((CliffordAlgebra.even.lift.fFold f) m₂) (1, 0))).1 = (f.bilin m₁) m₂

Tactic:
exact mul_one _

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma le_pullbacks : P ≤ P.pullbacks

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
A B : C
q : A ⟶ B
hq : P q
⊢ P.pullbacks q

Tactic:
exact P.pullbacks_mk IsPullback.of_id_fst hq

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pullbacks

Tactic:
intro A B q hq

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
A B : C
q : A ⟶ B
hq : P q
⊢ P.pullbacks q
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem union_ae_eq_left_of_ae_eq_empty (h : t =ᵐ[μ] (∅ : Set α)) : (s ∪ t : Set α) =ᵐ[μ] s

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s = s ∪ ∅

Tactic:
rw [union_empty]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] s

Tactic:
convert ae_eq_set_union (ae_eq_refl s) h

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s = s ∪ ∅
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem norm_injOn_ray_right (hy : y ≠ 0) : { x | SameRay ℝ x y }.InjOn norm

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
hy : y ≠ 0
⊢ Set.InjOn Norm.norm {x | SameRay ℝ x y}

Tactic:
simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem eq_reflection_of_eq_subspace {s s' : AffineSubspace ℝ P} [Nonempty s] [Nonempty s']
    [HasOrthogonalProjection s.direction] [HasOrthogonalProjection s'.direction] (h : s = s')
    (p : P) : (reflection s p : P) = (reflection s' p : P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : HasOrthogonalProjection s.direction
p : P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ (reflection s) p = (reflection s) p

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s s' : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : HasOrthogonalProjection s.direction
inst✝ : HasOrthogonalProjection s'.direction
h : s = s'
p : P
⊢ (reflection s) p = (reflection s') p

Tactic:
subst h

Result:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : HasOrthogonalProjection s.direction
p : P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ (reflection s) p = (reflection s) p
-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem rel_eq_eqvGen_quot_rel :
    FilteredColimit.Rel.{v, u} F = Relation.EqvGen (Quot.Rel F)

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
⊢ FilteredColimit.Rel F = Relation.EqvGen (Quot.Rel F)

Tactic:
ext ⟨j, x⟩ ⟨j', y⟩

Result:
case h.mk.h.mk.a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ ↔ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩

Proof state:
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩

Tactic:
rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]

Result:
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (FilteredColimit.Rel F) ⟨j, x⟩ ⟨j', y⟩

Proof state:
case h.mk.h.mk.a.mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩

Tactic:
apply eqvGen_quot_rel_of_rel

Result:
no goals

Proof state:
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (FilteredColimit.Rel F) ⟨j, x⟩ ⟨j', y⟩

Tactic:
exact Relation.EqvGen.mono (rel_of_quot_rel F)

Result:
no goals

Proof state:
case h.mk.h.mk.a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ ↔ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩

Tactic:
constructor

Result:
case h.mk.h.mk.a.mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩

case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
private lemma card_edgeFinset (hs : ThreeAPFree (s : Set α)) [DecidableEq α] :
    #(graph <| triangleIndices s).edgeFinset = 3 * card α * #s

Proof state:
α : Type u_1
inst✝³ : Fintype α
inst✝² : CommRing α
s : Finset α
inst✝¹ : Fact (IsUnit 2)
hs : ThreeAPFree ↑s
inst✝ : DecidableEq α
this : NoAccidental (triangleIndices s)
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s

Tactic:
rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Fintype α
inst✝² : CommRing α
s : Finset α
inst✝¹ : Fact (IsUnit 2)
hs : ThreeAPFree ↑s
inst✝ : DecidableEq α
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s

Tactic:
haveI := noAccidental hs

Result:
α : Type u_1
inst✝³ : Fintype α
inst✝² : CommRing α
s : Finset α
inst✝¹ : Fact (IsUnit 2)
hs : ThreeAPFree ↑s
inst✝ : DecidableEq α
this : NoAccidental (triangleIndices s)
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_node {y c a x b} :
    y ∈ (.node c a x b : RBNode α) ↔ y = x ∨ y ∈ a ∨ y ∈ b

Proof state:
α : Type u_1
y : α
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ y ∈ node c a x b ↔ y = x ∨ y ∈ a ∨ y ∈ b

Tactic:
simp [Membership.mem, EMem]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.neg_iff {a b : α} :
    FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Proof state:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Tactic:
unfold FiniteMultiplicity

Result:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ (∃ n, ¬a ^ (n + 1) ∣ -b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b

Proof state:
case a.h.e'_2.h.h.e'_1.a
α : Type u_1
inst✝ : Ring α
a b : α
x✝ : ℕ
⊢ a ^ (x✝ + 1) ∣ -b ↔ a ^ (x✝ + 1) ∣ b

Tactic:
simp only [dvd_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ (∃ n, ¬a ^ (n + 1) ∣ -b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b

Tactic:
congr! 3

Result:
case a.h.e'_2.h.h.e'_1.a
α : Type u_1
inst✝ : Ring α
a b : α
x✝ : ℕ
⊢ a ^ (x✝ + 1) ∣ -b ↔ a ^ (x✝ + 1) ∣ b
-- Mathlib/Computability/DFA.lean
theorem evalFrom_comap (f : α' → α) (s : σ) (x : List α') :
    (M.comap f).evalFrom s x = M.evalFrom s (x.map f)

Proof state:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
⊢ (comap f M).evalFrom s x = M.evalFrom s (List.map f x)

Tactic:
induction x using List.reverseRecOn with
| nil => simp
| append_singleton x a ih => simp [ih]

Result:
no goals

Proof state:
case append_singleton
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
a : α'
ih : (comap f M).evalFrom s x = M.evalFrom s (List.map f x)
⊢ (comap f M).evalFrom s (x ++ [a]) = M.evalFrom s (List.map f (x ++ [a]))

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
⊢ (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem degree_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
    (G.induce s).degree v = G.degree v

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ (induce s G).degree v = G.degree ↑v

Tactic:
simp_rw [← card_neighborFinset_eq_degree,
  ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_lt_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y < ∞ ↔ x < ∞

Proof state:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y < ⊤ ↔ x < ⊤

Tactic:
simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x

Proof state:
w : Nat
x y : BitVec w
⊢ x.ule y = !y.ult x

Tactic:
simp [BitVec.ule, BitVec.ult, ← decide_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ ≤ l₃) :
    l₁ ++ l₂ ≤ l₁ ++ l₃

Proof state:
α : Type u_1
n m : Nat
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ : Vector α n
l₂ l₃ : Vector α m
h : l₂ ≤ l₃
⊢ l₁ ++ l₂ ≤ l₁ ++ l₃

Tactic:
simpa using Array.append_left_le h

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem neg_eq_self
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : -v = v ↔ v = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
⊢ -v = v ↔ v = 0

Tactic:
rw [eq_comm, self_eq_neg R M]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : getKey k (insertEntry k v l) containsKey_insertEntry_self = k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getKey k (insertEntry k v l) ⋯ = k

Tactic:
simp [getKey_insertEntry]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma HasAffineProperty.affineAnd_eq_of_propertyIsLocal {P P' : MorphismProperty Scheme.{u}}
    (hP : HasAffineProperty P (affineAnd Q)) [HasRingHomProperty P' Q] :
    P = (@IsAffineHom ⊓ P' : MorphismProperty Scheme.{u})

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q

Tactic:
exact HasRingHomProperty.isLocal_ringHomProperty P'

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q
⊢ P = @IsAffineHom ⊓ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
  targetAffineLocally_affineAnd_eq_affineLocally,
  HasRingHomProperty.eq_affineLocally (P := P')]

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q