mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
← effectiveEpi_iff_effectiveEpiFamily

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpi (F.effectiveEpiOver B)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact and_congr (isSheaf_iff_preservesFiniteProducts _)
    (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ SingleEqualizerCondition P π ↔ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op))

Tactic:
by
  constructor
  · intro h
    exact ⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩
  · intro ⟨h⟩
    exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
q' : Z ⟶ S
a' : Z ⟶ X (α j)
hq' : q ≫ f i = q'
ha' : a ≫ p' j = a'
⊢ mor w φ q a fac = D₁.hom q' q a' ⋯ ⋯ ≫ pullHom (φ.hom j) a a' a' ⋯ ⋯ ≫ D₂.hom q' a' q ⋯ ⋯

Tactic:
subst hq' ha'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
⊢ mor w φ q a fac =
    D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
inst✝ : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
this : Mono (S.shortComplex.f ≫ biprod.snd)
⊢ Mono S.shortComplex.f

Tactic:
exact mono_of_mono _ biprod.snd

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
⊢ (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y → x = y

Tactic:
hxy

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
have h₁ (i' : ι') : ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i' := by
    obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk
    exact ⟨i, _, fac⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R)) ≤
    (Sieve.overEquiv (Over.mk a)).symm R

Tactic:
rintro X b ⟨Y, c, d, h, fac⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h✝ :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
X : Over S₀
b : X ⟶ Over.mk a
Y : Over S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h : ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows c
fac : b ≫ (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv = d ≫ (Over.map a).map c
⊢ ((Sieve.overEquiv (Over.mk a)).symm R).arrows b
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
⊢ adj.op.CommShift ℤ

Tactic:
have eq : adj.op = PullbackShift.adjunction
    (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; lia))
      (OppositeShift.adjunction ℤ adj) := by
    ext
    dsimp [PullbackShift.adjunction, NatTrans.PullbackShift.natIsoId,
      NatTrans.PullbackShift.natIsoComp, PullbackShift.functor, PullbackShift.natTrans,
      OppositeShift.adjunction, OppositeShift.natTrans, NatTrans.OppositeShift.natIsoId,
      NatTrans.OppositeShift.natIsoComp, OppositeShift.functor]
    simp only [Category.comp_id, Category.id_comp]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
⊢ adj.op.CommShift ℤ
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c

Tactic:
rintro a ha b hb c hc habc

Goal state after:
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : a * c = b * b
⊢ b = c
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (shiftFunctor (Triangle C) 1).obj (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ∈ distinguishedTriangles

Tactic:
refine isomorphic_distinguished _ H.mem _ ?_

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (shiftFunctor (Triangle C) 1).obj (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ≅
    Triangle.mk H.m₁ H.m₃
      ((-(shiftFunctor C 1).map (Triangle.mk α β γ).mor₁) ≫ (shiftFunctor C 1).map (Triangle.mk (ι.map f₁) f₂ f₃).mor₃)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map (fun x ↦ f₁ x) s).prod = (map (fun x ↦ f₁ x) t).prod ↔ s.prod = t.prod

Tactic:
hf₁.map_prod_eq_map_prod hsA htA hs ht

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ s.prod = t.prod ↔ s.prod = t.prod
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b

Tactic:
← two_mul

Goal state after:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : 2 * a = 2 * b
⊢ a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
⊢ ThreeAPFree (frontier s)

Tactic:
intro a ha b hb c hc habc

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
c : E
hc : c ∈ frontier s
habc : a + c = b + b
⊢ a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
a b : Fin n → ℕ
⊢ ∑ x, (a x + b x) * d ^ ↑x = ∑ i, a i * d ^ ↑i + ∑ i, b i * d ^ ↑i

Tactic:
add_mul,

Goal state after:
n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
a b : Fin n → ℕ
⊢ ∑ x, (a x * d ^ ↑x + b x * d ^ ↑x) = ∑ i, a i * d ^ ↑i + ∑ i, b i * d ^ ↑i
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
⊢ (map d) x₁ = (map d) x₂

Tactic:
rw [map_succ', map_succ', h.1, h.2]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
⊢ ∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
  refine ⟨k, ?_⟩
  obtain rfl | hn := n.eq_zero_or_pos
  · simp
  obtain rfl | hd := d.eq_zero_or_pos
  · simp
  refine (div_le_div_of_nonneg_left (by positivity) (by positivity) ?_).trans hk
  simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow,
    cast_one, mul_one, sub_add, sub_sub_self]
  apply one_le_mul_of_one_le_of_one_le
  · rwa [one_le_cast]
  rw [_root_.le_sub_iff_add_le]
  norm_num
  exact one_le_cast.2 hd

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

pp: case hxy
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ 2 ^ 3

Tactic:
· field_simp
        simp (disch := positivity) [exp_one_gt_two]

Goal state after:
case hxy
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ 2 ^ 3
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑⌈√(log ↑N)⌉₊

Tactic:
grw [ceil_lt_mul]
    · rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
      · norm_num [le_sqrt_log hN]
      · norm_num1
    · rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
      refine log_pos ?_
      rw [one_lt_cast]
      exact hN.trans_lt' (by norm_num1)
    apply le_sqrt_of_sq_le
    have : (12 : ℕ) * log 2 ≤ log N := by
      rw [← log_rpow zero_lt_two, rpow_natCast]
      exact log_le_log (by positivity) (mod_cast hN)
    refine le_trans ?_ this
    rw [← div_le_iff₀']
    · exact log_two_gt_d9.le.trans' (by norm_num1)
    · norm_num1

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Tactic:
refine Real.sqrt_pos.2 (log_pos ?_)

Goal state after:
case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(mulDysonETransform e x).1 + #(mulDysonETransform e x).2 = #x.1 + #x.2

Tactic:
dsimp
  rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]

Goal state after:
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
      ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
simp only [hc]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #{w | Odd (G.degree w) ∧ w ≠ v}
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
h : G.minDegree = 0
⊢ ∃ v, G.IsIsolated v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
x✝ : ∃ v, G.IsIsolated v
v : V
hv : G.IsIsolated v
⊢ G.minDegree = 0

Tactic:
· grind [G.exists_minimal_degree_vertex, degree_eq_zero]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
x✝ : ∃ v, G.IsIsolated v
v : V
hv : G.IsIsolated v
⊢ G.minDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ insert v (G.neighborFinset v) = univ ↔ G.IsUniversal v

Tactic:
simp only [Finset.ext_iff, mem_insert, mem_neighborFinset, IsUniversal]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ (∀ (a : V), a = v ∨ G.Adj v a ↔ a ∈ univ) ↔ ∀ ⦃w : V⦄, v ≠ w → G.Adj v w
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
y✝ : α
hy : y✝ ∈ ↑P.parts
⊢ x✝ ≠ y✝ → (Disjoint on f) x✝ y✝

Tactic:
hxy

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
y✝ : α
hy : y✝ ∈ ↑P.parts
hxy : x✝ ≠ y✝
⊢ (Disjoint on f) x✝ y✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
simp_rw [← P.sup_parts]
  refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩
  · rw [h]
    exact Finset.sup_empty
  · rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ (a : Finset α),
    a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1 ↔
      (Equiv.refl (Finset α)) a ∈ P.parts ∧ #((Equiv.refl (Finset α)) a) = #s / #P.parts

Tactic:
simp only [Equiv.refl_apply, and_congr_right_iff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ (((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) * x ^ 2 / ↑(#t)) * ↑(#t) ≤ ∑ i ∈ t, f i ^ 2

Tactic:
add_mul,

Goal state after:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ↑(#s) * x ^ 2 / ↑(#t) * ↑(#t) ≤ ∑ i ∈ t, f i ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2

Tactic:
apply (Nat.mul_lt_mul_of_pos_right this <| pow_pos Nat.succ_pos' _).trans_le

Goal state after:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j ^ 2 * (i / j).succ ^ 2 ≤ (i + j) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬H.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Tactic:
· grind [subgraphOfAdj_adj, h.symm]

Goal state after: