mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
⊢ b ∉ g ⁻¹' {h c} →
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0

Tactic:
nm

Goal state after:
case w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : b ∉ g ⁻¹' {h c}
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a ↦ s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b) ≫ w) ≫ biproduct.π (fun b ↦ s (h b)) c =
    0
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ ∀ (w : X ⟶ Y), ∃ c, c • f = w

Tactic:
intro g

Goal state after:
case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
⊢ ∃ c, c • f = g
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)

Tactic:
← not_nonempty_iff,

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬Nonempty (X ≅ Y)
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
let (a : α) : PartialOrder a.1 := a.2.1

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a' ≫ d'))) y₁ = (ConcreteCategory.hom (F.map (a ≫ d))) y₁

Tactic:
by rw [h₅]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
⊢ ∃ g', f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)

Tactic:
simp only [iteration_map_succ]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
⊢ ∃ g', f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j) ≫ (iterationObjSuccIso W Z κ j).inv
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ CreatesColimit G (sheafToPresheaf (extensiveTopology C) A)

Tactic:
refine createsColimitOfIsSheaf _ (fun c hc ↦ ?_)

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
⊢ Presheaf.IsSheaf (extensiveTopology C) c.pt
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
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
this : PreservesFiniteProducts F
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι ((F ⋙ s).map π.op) ⋯)

Tactic:
exact isLimitForkMapOfIsLimit s _ (hF.2 π c hc).some

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

Goal state before:
pp: case h₂.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ op i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ (ObjectProperty.homMk (Over.homMk ij ⋯)).op

Tactic:
congr; aesop

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

Goal state before:
pp: case h₂.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ op j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ (ObjectProperty.homMk (Over.homMk ij ⋯)).op

Tactic:
congr; aesop

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

Goal state before:
pp: case _i
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
φ φ' : D₁ ⟶ D₂
i : ι
this✝¹ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
this✝ : Over.Hom.left g = Z.hom
this :
  ∀ (ψ : D₁ ⟶ D₂),
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (ψ.hom i)) =
      D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
        pullHom ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯
hφ : (F.map (p' j).op.toLoc).toFunctor.map (φ.hom (α j)) = (F.map (p' j).op.toLoc).toFunctor.map (φ'.hom (α j))
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ.hom i)) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ'.hom i))

Tactic:
simp only [this, hφ]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ IsLimit (F.multifork G)

Tactic:
refine Multifork.IsLimit.mk _ ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ (E : Multifork (F.multicospanIndex G)) → E.pt ⟶ (F.multifork G).pt

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ ∀ (E : Multifork (F.multicospanIndex G)) (i : F.multicospanShape.L), ?refine_1 E ≫ (F.multifork G).ι i = E.ι i

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ ∀ (E : Multifork (F.multicospanIndex G)) (m : E.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E.ι i) → m = ?refine_1 E
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
hf' : Sieve.ofArrows X' f' ∈ J S
i : ι
⊢ sieve f f' i ∈ (J.over (X i)) (Over.mk (𝟙 (X i)))

Tactic:
by
  simpa only [J.mem_over_iff, OrderIso.apply_symm_apply] using! J.pullback_stable (f i) hf'

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 : E.I₀
⊢ Sieve.generate (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows ∈ J (E.X i)

Tactic:
rw [Sieve.generate_sieve]

Goal state after:
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 : E.I₀
⊢ Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i)) ∈ J (E.X i)
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)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
⊢ ∀ ⦃i j : WalkingPair⦄ (a : W ⟶ pairFunction sq.X₂ sq.X₃ i) (b : W ⟶ pairFunction sq.X₂ sq.X₃ j),
    a ≫ WalkingPair.casesOn i sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn j sq.f₂₄ sq.f₃₄ →
      WalkingPair.casesOn i s.fst s.snd ≫ F.obj.map a.op = WalkingPair.casesOn j s.fst s.snd ≫ F.obj.map b.op

Tactic:
by
          rintro (_ | _) (_ | _) a b fac
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
            rfl
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
            simpa using s.condition =≫ F.obj.map φ.op
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
            simpa using s.condition.symm =≫ F.obj.map φ.op
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
            rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ P.triangEnvelopeIter n

Tactic:
rw [← triangEnvelopeIter_zero]
      exact P.monotone'_triangEnvelopeIter (Nat.zero_le n)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case left
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ₁ : Y ⟶ Z
⊢ ∀ ⦃a₂ : Y ⟶ Z⦄, (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₁ = (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) a₂ → φ₁ = a₂

Tactic:
φ₂

Goal state after:
case left
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ₁ φ₂ : Y ⟶ Z
⊢ (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₁ = (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₂ → φ₁ = φ₂
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree s ↔ ThreeGPFree t

Tactic:
← threeGPFree_image hf subset_rfl,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree (f '' s) ↔ ThreeGPFree t
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 * d ^ ↑x + b x * d ^ ↑x) = ∑ i, a i * d ^ ↑i + ∑ i, b i * d ^ ↑i

Tactic:
sum_add_distrib

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

Goal state before:
pp: n d : ℕ
⊢ Set.InjOn ⇑(map d) {x | ∀ (i : Fin n), x i < d}

Tactic:
intro x₁ hx₁ x₂ hx₂ h

Goal state after:
n d : ℕ
x₁ : Fin n → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin n), x i < d}
x₂ : Fin n → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin n), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Tactic:
refine (hFmax.not_gt ?_ <| ssubset_insert hau).elim

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ insert a F ⊆ A ∧ (↑(insert a F)).PairwiseDisjoint fun x ↦ x • B
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ log ↑N / √(log ↑N)

pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N

Tactic:
div_sqrt

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ √(log ↑N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
have : exp (-4 * √(log N)) = exp (-2 * √(log N)) * exp (-2 * √(log N)) := by
    rw [← exp_add, ← add_mul]
    norm_num

Goal state after:
case hbc
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))
⊢ rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inr.succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) ≤ (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A) * ↑(#A)

Tactic:
calc
      ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
        = #(B ^ n * A * B) * #A := by rw [pow_succ, mul_left_comm, mul_assoc]
      _ ≤ #(A * B) * #(B ^ n * A) := mod_cast pluennecke_petridis_inequality_mul _ hAB
      _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by rw [mul_comm _ A]; gcongr
      _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by simp [field, pow_add]

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

Goal state before:
pp: case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1

Tactic:
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]

Goal state after:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case «0»
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨0, ⋯⟩)| = 1

Tactic:
simp [hε]

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

Goal state before:
pp: case «1»
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨1, ⋯⟩)| = 1

Tactic:
simp [hε]

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

Goal state before:
pp: case «2»
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨2, ⋯⟩)| = 1

Tactic:
simp [hε]

Goal state after: