awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
w :
  ∀ (x : Cᵒᵖ)
    (x_1 : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).obj X).obj x),
    Eq (α := obj (obj uliftYoneda.{v₂, v₁, u₁} Y) x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).map f ≫
              Iso.hom ((fun (X : C) ↦ hF.homNatIso X) Y))
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Iso.hom ((fun (X : C) ↦ hF.homNatIso X) X) ≫ map uliftYoneda.{v₂, v₁, u₁} f) x))
        x_1)
⊢ Eq (α :=
    (F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).obj X ⟶
      obj uliftYoneda.{v₂, v₁, u₁} Y)
    ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).map f ≫
      Iso.hom ((fun (X : C) ↦ hF.homNatIso X) Y))
    (Iso.hom ((fun (X : C) ↦ hF.homNatIso X) X) ≫ map uliftYoneda.{v₂, v₁, u₁} f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
x : Cᵒᵖ
x_1 : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).obj X).obj x
⊢ Eq (α := F.obj (unop x) ⟶ F.obj Y)
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj Y).obj x)) → (yoneda.obj Y).obj x)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).map f ≫
                Iso.hom ((fun (X : C) ↦ hF.homNatIso X) Y))
              x))
          x_1)))
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj Y).obj x)) → (yoneda.obj Y).obj x)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Iso.hom ((fun (X : C) ↦ hF.homNatIso X) X) ≫ map uliftYoneda.{v₂, v₁, u₁} f) x))
          x_1)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
x : Cᵒᵖ
x_1 : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).obj X).obj x
⊢ Eq (α := obj (obj uliftYoneda.{v₂, v₁, u₁} Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))) F.op).map f ≫
            Iso.hom ((fun (X : C) ↦ hF.homNatIso X) Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (Iso.hom ((fun (X : C) ↦ hF.homNatIso X) X) ≫ map uliftYoneda.{v₂, v₁, u₁} f) x))
      x_1)

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, Equiv.ulift, Equiv.injective
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X X_1 Y : C
f : X_1 ⟶ Y
h :
  ∀ (x : (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj X_1),
    Eq (α := obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).map f ≫
            Iso.hom
              ((fun (Y : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                    (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                      obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (Y : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                    (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                      obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
                X_1) ≫
            map (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) f))
        x)
⊢ Eq (α := (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj X_1 ⟶ obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y)
    ((F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).map f ≫
      Iso.hom
        ((fun (Y : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
              (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
          Y))
    (Iso.hom
        ((fun (Y : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
              (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
          X_1) ≫
      map (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X X_1 Y : C
f : X_1 ⟶ Y
x : (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj X_1
⊢ Eq (α := F.obj (unop (op X)) ⟶ F.obj Y)
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj Y).obj (op X))) → (yoneda.obj Y).obj (op X))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).map f ≫
              Iso.hom
                ((fun (Y : C) ↦
                    (Equiv.toIso
                        (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                      (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                        obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
                  Y)))
          x)))
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj Y).obj (op X))) → (yoneda.obj Y).obj (op X))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
                ((fun (Y : C) ↦
                    (Equiv.toIso
                        (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                      (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                        obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
                  X_1) ≫
              map (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) f))
          x)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X X_1 Y : C
f : X_1 ⟶ Y
x : (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj X_1
⊢ Eq (α := obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).map f ≫
          Iso.hom
            ((fun (Y : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                  (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                    obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                  (F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj X))).obj Y ≅
                    obj (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) Y))
              X_1) ≫
          map (obj uliftCoyoneda.{v₂, v₁, u₁} (op X)) f))
      x)

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, Equiv.ulift, Equiv.injective
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : Cᵒᵖ
f : X ⟶ Y
w :
  ∀ (x : C) (x_1 : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).obj X).obj x),
    Eq (α := obj (obj uliftCoyoneda.{v₂, v₁, u₁} Y) x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).map f ≫
              Iso.hom
                ((fun (X : Cᵒᵖ) ↦
                    (hF.homNatIso' (unop X) :
                      F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                        obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                  Y))
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : Cᵒᵖ) ↦
                    (hF.homNatIso' (unop X) :
                      F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                        obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                  X) ≫
              map uliftCoyoneda.{v₂, v₁, u₁} f)
            x))
        x_1)
⊢ Eq (α :=
    (F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).obj X ⟶
      obj uliftCoyoneda.{v₂, v₁, u₁} Y)
    ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).map f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (hF.homNatIso' (unop X) :
              F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅ obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
          Y))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (hF.homNatIso' (unop X) :
              F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅ obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
          X) ≫
      map uliftCoyoneda.{v₂, v₁, u₁} f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : Cᵒᵖ
f : X ⟶ Y
x : C
x_1 : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).obj X).obj x
⊢ Eq (α := F.obj (unop Y) ⟶ F.obj x)
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj x).obj Y)) → (yoneda.obj x).obj Y)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).map f ≫
                Iso.hom
                  ((fun (X : Cᵒᵖ) ↦
                      (hF.homNatIso' (unop X) :
                        F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                          obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                    Y))
              x))
          x_1)))
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj x).obj Y)) → (yoneda.obj x).obj Y)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Iso.hom
                  ((fun (X : Cᵒᵖ) ↦
                      (hF.homNatIso' (unop X) :
                        F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                          obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                    X) ≫
                map uliftCoyoneda.{v₂, v₁, u₁} f)
              x))
          x_1)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : Cᵒᵖ
f : X ⟶ Y
x : C
x_1 : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).obj X).obj x
⊢ Eq (α := obj (obj uliftCoyoneda.{v₂, v₁, u₁} Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ obj (whiskeringLeft C D (Type (max v₁ v₂))) F).map f ≫
            Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (hF.homNatIso' (unop X) :
                    F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                      obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (hF.homNatIso' (unop X) :
                    F ⋙ obj uliftCoyoneda.{v₁, v₂, u₂} (op (F.obj (unop X))) ≅
                      obj uliftCoyoneda.{v₂, v₁, u₁} (op (unop X))))
                X) ≫
            map uliftCoyoneda.{v₂, v₁, u₁} f)
          x))
      x_1)

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, Equiv.ulift, Equiv.injective
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : 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
⊢ Ne.{u_1 + 1} (α := 𝕜) 2 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : 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
rwa : (1 / 2) • (a + c) = b
rwa₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ (a + c) = b
rwa₂ : a + c = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 b
rwa₃ rwa₄ rwa₅ rwa₆ : a + c = b + b
⊢ (1 / 2) • a + (1 / 2) • c = b

Tactic:
rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]

Premises used: two_smul, inv_smul_eq_iff₀, one_div, smul_add
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : 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
obtain :
  ∀ (hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s)
    (habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)), a = (1 / 2) • a + (1 / 2) • c
⊢ a = b

Tactic:
obtain rfl : (1 / 2 : 𝕜) • a + (1 / 2 : 𝕜) • c = b := by
    rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]

Premises used: HDiv.hDiv, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
c : E
hc : c ∈ frontier s
hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s
habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)
⊢ a = c

Tactic:
have :=
    hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hc) one_half_pos one_half_pos
      (add_halves _) hb.2
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
c : E
hc : c ∈ frontier s
hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s
habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)
this : a = c
simp : c = HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • c
⊢ a = (1 / 2) • a + (1 / 2) • c

Tactic:
simp [this, ← add_smul]

Premises used: add_smul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
c : E
hc : c ∈ frontier s
hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s
habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)
this : a = c
ring_nf : c = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 c
⊢ c = HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • c

Tactic:
ring_nf
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
c : E
hc : c ∈ frontier s
hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s
habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)
this : a = c
⊢ c = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 c

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
inl : ThreeAPFree (sphere x 0)
inr : ∀ (hr : r ≠ 0), ThreeAPFree (sphere x r)
⊢ ThreeAPFree (sphere x r)

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
inl : ThreeAPFree (α := E) {x}
⊢ ThreeAPFree (sphere x 0)

Tactic:
rw [sphere_zero]

Premises used: Metric.sphere_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (α := E) {x}

Tactic:
threeAPFree_singleton _

Premises used: threeAPFree_singleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (α := E) {x}

Tactic:
exact threeAPFree_singleton _

Premises used: threeAPFree_singleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (frontier (closedBall x r))

Tactic:
threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)

Premises used: Real, Metric.isClosed_closedBall, strictConvex_closedBall, threeAPFree_frontier
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
h : sphere x r = frontier (closedBall x r)
⊢ ThreeAPFree (sphere x r)

Tactic:
convert! threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)

Premises used: Real, Metric.isClosed_closedBall, strictConvex_closedBall, threeAPFree_frontier
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)

Tactic:
(frontier_closedBall _ hr).symm

Premises used: frontier_closedBall, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)

Tactic:
exact (frontier_closedBall _ hr).symm

Premises used: frontier_closedBall, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
⊢ x ∈ box n d ↔ ∀ (i : Fin n), x i < d

Tactic:
simp only [box, Fintype.mem_piFinset, mem_range]

Premises used: Fintype.mem_piFinset, Behrend.box, Finset.mem_range
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ #(box n d) = d ^ n

Tactic:
simp [box]

Premises used: Behrend.box
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin (n + 1) → ℕ)) (box (n + 1) 0) ∅

Tactic:
simp [box]

Premises used: Behrend.box
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
⊢ x ∈ sphere n d 0 → Membership.mem (γ := Finset (Fin n → ℕ)) 0 x

Tactic:
simp [sphere, funext_iff]

Premises used: Behrend.sphere, funext_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n k : ℕ
⊢ Eq (α := Finset (Fin (n + 1) → ℕ)) (sphere (n + 1) 0 k) ∅

Tactic:
simp [sphere]

Premises used: Behrend.sphere
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
⊢ sphere n d k ⊆ box n d

Tactic:
filter_subset _ _

Premises used: Set.Mem, setOf, Finset.filter_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
rw :
  √(∑ i : Fin n,
        HPow.hPow (β := ℕ)
          (Norm.norm (E := (fun (x : Fin n) ↦ ℝ) i) (ofLp (p := 2) (toLp 2 (Nat.cast ∘ x)) i : (fun (x : Fin n) ↦ ℝ) i))
          2) =
    √(↑k : ℝ)
⊢ Norm.norm (E := WithLp 2 (Fin n → ℝ)) (toLp 2 (Nat.cast ∘ x)) = √(↑k : ℝ)

Tactic:
rw [EuclideanSpace.norm_eq]

Premises used: EuclideanSpace.norm_eq
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
simp_rw : √(∑ x_1 : Fin n, HPow.hPow (α := ℝ) (β := ℕ) (↑(x x_1) : ℝ) 2) = √(↑k : ℝ)
simp_rw₁ : √(∑ x_1 : Fin n, (↑(HPow.hPow (β := ℕ) (x x_1) 2) : ℝ)) = √(↑k : ℝ)
simp_rw₂ : √(↑(∑ x_1 : Fin n, HPow.hPow (β := ℕ) (x x_1) 2) : ℝ) = √(↑k : ℝ)
⊢ √(∑ i : Fin n, HPow.hPow (α := ℝ) (β := ℕ) |(↑(x i) : ℝ)| 2) = √(↑k : ℝ)

Tactic:
simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]

Premises used: Nat.abs_cast, Nat.cast_sum, And.right, Iff.mp, Finset.mem_filter, Nat.cast_pow
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
rw : Membership.mem (γ := Set (WithLp 2 (Fin n → ℝ))) (Metric.sphere 0 √(↑k : ℝ)) (toLp 2 (Nat.cast ∘ x))
rw₁ : Norm.norm (E := WithLp 2 (Fin n → ℝ)) (toLp 2 (Nat.cast ∘ x)) = √(↑k : ℝ)
rw₂ rw₃ : √(↑k : ℝ) = √(↑k : ℝ)
⊢ Membership.mem (γ := Set (Fin n → ℕ))
    (Set.preimage (β := WithLp 2 (Fin n → ℝ)) (fun (x : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ x)) (Metric.sphere 0 √(↑k : ℝ)))
    x

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]

Premises used: Behrend.norm_of_mem_sphere, mem_sphere_zero_iff_norm, Set.mem_preimage
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d_1 k N : ℕ
x : Fin n → ℕ
d : ℕ
simp_rw : Eq (α := ℕ) (∑ x : Fin n, 0 * d ^ (↑x : ℕ)) 0
simp_rw₁ : Eq (α := ℕ) (∑ x : Fin n, 0) 0
⊢ Eq (α := ℕ) (∑ i : Fin n, 0 i * d ^ (↑i : ℕ)) 0

Tactic:
simp_rw [Pi.zero_apply, zero_mul, sum_const_zero]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Finset.sum_const_zero