awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
s : (↑F.sections : Type (max u₁ u₂))
x x_1 : C
x_2 : x ⟶ x_1
⊢ Eq (α := obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x ⟶ F.obj x_1)
    (map (obj (const C) X) x_2 ≫
      ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1) ↦ (↑s : (j : C) → F.obj j) x_1)
    ((↾fun (x_3 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x) ↦ (↑s : (j : C) → F.obj j) x) ≫ F.map x_2)
have h : ∀ (x_3 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj (const C) X) x_2 ≫
          ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1) ↦ (↑s : (j : C) → F.obj j) x_1))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x) ↦ (↑s : (j : C) → F.obj j) x) ≫ F.map x_2))
      x_3
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
⊢ (↑F.sections : Type (max u₁ u₂))
have refine : ∀ {j j' : C} (φ : j ⟶ j'),
  Eq (α := (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) :
          (a : (fun (X : Type u₂) ↦ X) (F.obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j'))
        ((fun (j : C) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                  (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                default :
              (fun (X : Type u₂) ↦ X) (F.obj j)))
          j) :
      (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((fun (j : C) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
              default :
            (fun (X : Type u₂) ↦ X) (F.obj j)))
        j' :
      (fun (X : Type u₂) ↦ X) (F.obj j'))
Tactic: refine ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
j j' : C
φ : j ⟶ j'
⊢ Eq (α := (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) :
          (a : (fun (X : Type u₂) ↦ X) (F.obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j'))
        ((fun (j : C) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                  (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                default :
              (fun (X : Type u₂) ↦ X) (F.obj j)))
          j) :
      (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((fun (j : C) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
              default :
            (fun (X : Type u₂) ↦ X) (F.obj j)))
        j' :
      (fun (X : Type u₂) ↦ X) (F.obj j'))
have simp : Eq (α := F.obj j')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ τ.app j') : (a : ((const C).obj X).obj j) → F.obj j') default :
    F.obj j')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j') : (a : ((const C).obj X).obj j') → F.obj j') default : F.obj j')
Tactic: simp [-const_obj_obj, ← comp_apply, -types_comp_apply, ← NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
⊢ (fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
        ({ app := fun (j : C) ↦ ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
            naturality := ⋯ } :
          NatTrans (obj (const C) X) F))
      ((fun (τ : obj (const C) X ⟶ F) ↦
          (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
              (fun (j : C) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                    (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                  default)
              ⋯ :
            { x : (j : C) → F.obj j // x ∈ F.sections }))
        τ) =
    τ
have w : ∀ (x : C) (x_1 : X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
              ({
                  app := fun (j : C) ↦
                    ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                  naturality := sorry } :
                NatTrans (obj (const C) X) F))
            ((fun (τ : obj (const C) X ⟶ F) ↦
                (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : C) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                          (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                        default)
                    sorry :
                  { x : (j : C) → F.obj j // x ∈ F.sections }))
              τ))
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x)).toFun x_1
Tactic: ext _ (x : X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
x_1 : C
x : X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
              ({
                  app := fun (j : C) ↦
                    ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                  naturality := ⋯ } :
                NatTrans (obj (const C) X) F))
            ((fun (τ : obj (const C) X ⟶ F) ↦
                (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : C) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                          (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                        default)
                    ⋯ :
                  { x : (j : C) → F.obj j // x ∈ F.sections }))
              τ))
          x_1))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x_1)).toFun x
have w : TypeCat.Fun.toFun (X := obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1)
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (NatTrans.app
        ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
            ({
                app := fun (j : C) ↦
                  ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                naturality := sorry } :
              NatTrans (obj (const C) X) F))
          ((fun (τ : obj (const C) X ⟶ F) ↦
              (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                  (fun (j : C) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                        (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                      default)
                  sorry :
                { x : (j : C) → F.obj j // x ∈ F.sections }))
            τ))
        x_1))
    default =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x_1)).toFun default
Tactic: rw [Unique.eq_default x]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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 : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
⊢ Eq (α := (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1 ⟶ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y)
    ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (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.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} 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.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
          X_1) ≫
      map (obj uliftYoneda.{v₂, v₁, u₁} X) f)
have h : ∀ (x : (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1),
  Eq (α := obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (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.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} 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.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
              X_1) ≫
          map (obj uliftYoneda.{v₂, v₁, u₁} X) f))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (1 / 2) • a + (1 / 2) • c = b
have rwa : (1 / 2) • (a + c) = b
Tactic: rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (1 / 2) • a + (1 / 2) • c = b
have rwa₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ (a + c) = b
Tactic: rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (1 / 2) • a + (1 / 2) • c = b
have rwa₂ : a + c = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 b
Tactic: rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ a = b
have 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
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]
Cleared hypotheses: b, hb, habc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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 = (1 / 2) • a + (1 / 2) • c
have this : a = c
Tactic: have :=
    hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hc) one_half_pos one_half_pos
      (add_halves _) hb.2
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ a = (1 / 2) • a + (1 / 2) • c
have simp : c = HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • c
Tactic: simp [this, ← add_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 = HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • c
have ring_nf : c = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 c
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
⊢ ThreeAPFree (sphere x r)
have inl : ThreeAPFree (sphere x 0)
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
inl : ThreeAPFree (sphere x 0)
⊢ ThreeAPFree (sphere x r)
have inr : ∀ (hr : r ≠ 0), ThreeAPFree (sphere x r)
Tactic: obtain rfl | hr := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (sphere x 0)
have inl : ThreeAPFree (α := E) {x}
Tactic: rw [sphere_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)
have h : sphere x r = frontier (closedBall x r)
Tactic: convert! threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Norm.norm (E := WithLp 2 (Fin n → ℝ)) (toLp 2 (Nat.cast ∘ x)) = √(↑k : ℝ)
have 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 : ℝ)
Tactic: rw [EuclideanSpace.norm_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i : Fin n, HPow.hPow (α := ℝ) (β := ℕ) |(↑(x i) : ℝ)| 2) = √(↑k : ℝ)
have simp_rw : √(∑ x_1 : Fin n, HPow.hPow (α := ℝ) (β := ℕ) (↑(x x_1) : ℝ) 2) = √(↑k : ℝ)
Tactic: simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)
⊢ √(∑ i : Fin n, HPow.hPow (α := ℝ) (β := ℕ) |(↑(x i) : ℝ)| 2) = √(↑k : ℝ)
have simp_rw₁ : √(∑ x_1 : Fin n, (↑(HPow.hPow (β := ℕ) (x x_1) 2) : ℝ)) = √(↑k : ℝ)
Tactic: simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)
⊢ √(∑ i : Fin n, HPow.hPow (α := ℝ) (β := ℕ) |(↑(x i) : ℝ)| 2) = √(↑k : ℝ)
have simp_rw₂ : √(↑(∑ x_1 : Fin n, HPow.hPow (β := ℕ) (x x_1) 2) : ℝ) = √(↑k : ℝ)
Tactic: simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
⊢ 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
have rw : Membership.mem (γ := Set (WithLp 2 (Fin n → ℝ))) (Metric.sphere 0 √(↑k : ℝ)) (toLp 2 (Nat.cast ∘ x))
Tactic: rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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))
⊢ 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
have rw₁ : Norm.norm (E := WithLp 2 (Fin n → ℝ)) (toLp 2 (Nat.cast ∘ x)) = √(↑k : ℝ)
Tactic: rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]