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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
x✝ : Arrow (Sheaf J A)
⊢ IsLocallySurjective
    ((inv (sheafificationAdjunction J A).counit).app x✝.left ≫
      (presheafToSheaf J A).map
        ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom)))

Tactic:
rw [← isLocallySurjective_sheafToPresheaf_map_iff, Functor.map_comp,
      Presheaf.comp_isLocallySurjective_iff, isLocallySurjective_sheafToPresheaf_map_iff,
      Presheaf.isLocallySurjective_presheafToSheaf_map_iff]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
x✝ : Arrow (Sheaf J A)
⊢ Presheaf.IsLocallySurjective J
    ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom))
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
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F

Tactic:
and_iff_left (isSheaf_of_projective F),

Goal state after:
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
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F G : Sheaf J A
f : F ⟶ G
U : Cᵒᵖ
⊢ (Γ J A).map f ≫ G.ΓRes U = (ΓHomEquiv.symm (𝟙 ((Γ J A).obj F) ≫ (Γ J A).map f)).app U

Tactic:
exact (congr_app (ΓHomEquiv_naturality_left_symm ((Γ J A).map f) (𝟙 _)) U).symm.trans (by simp)

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

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ p = ⋯.lift f₁ f₂ ⋯

Tactic:
by
    apply (sq i₁ i₂).isPullback.hom_ext <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ Sieve.pullback
      (pullback.map ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst) ∈
    J (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))

Tactic:
exact J.pullback_stable _ (mem_sieve₁' E _ _)

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
s : (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))) := ⋯.amalgamate (familyOfElements w φ i) ⋯
⊢ (F.map q.op.toLoc).toFunctor.map (hom w hf' φ i) = mor w φ q a fac

Tactic:
have hs : (familyOfElements w φ i).IsAmalgamation s :=
    Presieve.IsSheafFor.isAmalgamation
      (((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)).isSheafFor _
        (by simpa using sieve_mem _ hf' i)) (compatible_familyOfElements w φ i)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
s : (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))) := ⋯.amalgamate (familyOfElements w φ i) ⋯
hs : (familyOfElements w φ i).IsAmalgamation s
⊢ (F.map q.op.toLoc).toFunctor.map (hom w hf' φ i) = mor w φ q a fac
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ S.arrows ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom)

Tactic:
simpa using hZ

Goal state after:
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f✝ (α j) = f' j ≫ p
X✝ Y✝ : ↑(F.obj { as := op S })
f : X✝ ⟶ Y✝
i : ι'
⊢ ((F.toDescentData f✝ ⋙ pullFunctor F w).map f ≫
          (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app Y✝) ⋯).hom).hom
      i =
    ((isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app X✝) ⋯).hom ≫
          ((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').map f).hom
      i

Tactic:
exact (F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc).inv.toNatTrans.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows (↾fun x_1 ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : (Sieve.pullback (↾fun x_1 ↦ x) S).arrows f
y : β
⊢ ((ConcreteCategory.hom (f ≫ ↾fun x ↦ { down := true })).toFun y).down =
    ((ConcreteCategory.hom (f ≫ ↾fun x ↦ { down := false })).toFun y).down

Tactic:
exact hsx.elim <| S.2 hf (↾fun _ => y)

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : G.obj X),
    {
          arrows := fun Y f ↦
            ∃ a, (ConcreteCategory.hom (G.map f.op)) x₂ = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
          downward_closed := ⋯ } =
        ⊤ →
      ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = x₂

Tactic:
intro p

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
p : G.obj X
⊢ { arrows := fun Y f ↦ ∃ a, (ConcreteCategory.hom (G.map f.op)) p = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
        downward_closed := ⋯ } =
      ⊤ →
    ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = p
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
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 ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
map_id,

Goal state after:
case e_a
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 ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    𝟙 ((shiftFunctor D n).obj ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
· exact hs hb hc hd h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map ?m.102 s).prod = (map f (map g t)).prod ↔ s.prod = t.prod

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ s, (f ∘ g) x = ?m.102 x

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ β → β

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A

Tactic:
map_id,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ s.prod = (map f (map g t)).prod ↔ s.prod = t.prod

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ s, (f ∘ g) x = id x

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : (map ?m.123 s).prod = (map g (map f t)).prod
⊢ s.prod = t.prod

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
⊢ α → α

pp: case g1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = ?m.123 x

Tactic:
map_id,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map g (map f t)).prod
⊢ s.prod = t.prod

case g1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
a : Fin n.succ → ℕ
⊢ (map d) a % d = a 0 % d

Tactic:
map_succ,

Goal state after:
n d : ℕ
a : Fin n.succ → ℕ
⊢ (a 0 + (∑ x, a x.succ * d ^ ↑x) * d) % d = a 0 % d
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 : (map d) x₁ = (map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
map_succ,

Goal state after:
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, x₁ x.succ * d ^ ↑x) * d = (map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
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, x₁ x.succ * d ^ ↑x) * d = (map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
map_succ,

Goal state after:
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, x₁ x.succ * d ^ ↑x) * d = x₂ 0 + (∑ x, x₂ x.succ * d ^ ↑x) * d
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}

Tactic:
rw [Set.add_subset_iff]

Goal state after:
n d k : ℕ
⊢ ∀ x ∈ ↑(sphere n d k), ∀ y ∈ ↑(sphere n d k), x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hxy
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
exact two_div_one_sub_two_div_e_le_eight

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

Goal state before:
pp: case hxy
N : ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N

Tactic:
exact mod_cast hN

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift A to Finset G using hA
  lift B to Finset G using hB
  classical
  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
  exact ⟨F, by norm_cast; simp [*]⟩

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

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
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))
⊢ rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n))

Tactic:
rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff₀, mul_div_assoc,
      div_sqrt, neg_mul, neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff₀ hn]
    · gcongr
      apply le_ceil
    refine Real.sqrt_pos.2 (log_pos ?_)
    rw [one_lt_cast]
    exact hN.trans_lt' (by norm_num1)

Goal state after:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(Nat.card ↥(zmultiples ↑(n / n.minFac))) ≤ ↑n.minFac

Tactic:
rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
      gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]

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

Goal state before:
pp: case inr.inr.inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
hS : ↑(zpowers g) ⊆ a⁻¹ • ↑s
⊢ Nat.card ↑↑(a⁻¹ • s) = #s

Tactic:
simp [-coe_smul_finset]

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

Goal state before:

Tactic:
(#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
classical
    rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
      card_neighborSet_eq_degree]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
⊢ G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}

Tactic:
ext ⟨⟨⟩⟩
  simp [mk'_mem_incidenceSet_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.maxDegree = 0 ↔ G = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ G = ⊥

case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ G.maxDegree = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.degree v = Fintype.card V - 1 ↔ G.IsUniversal v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ G.IsUniversal v

case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1

Tactic:
simp [← card_neighborFinset_eq_degree, (G.neighborFinset_eq_erase_univ v).mpr h]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ⊆ s.powerset

Tactic:
intro p

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
⊢ p ∈ P.parts → p ∈ s.powerset