mathlib-initiative/mathlib-tactics huggingface dataset:
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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f' i₂).op.toLoc ≫ f₂.op.toLoc = q.op.toLoc

Tactic:
by grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (p.op.toLoc ≫ (f' i₂).op.toLoc) ≫ f₂.op.toLoc = p.op.toLoc ≫ q.op.toLoc

Tactic:
by grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₁)).op.toLoc ≫ (p' i₁).op.toLoc = p.op.toLoc ≫ (f' i₁).op.toLoc

Tactic:
by grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₂)).op.toLoc ≫ (p' i₂).op.toLoc = p.op.toLoc ≫ (f' i₂).op.toLoc

Tactic:
by grind

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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
x✝ : ι''
⊢ (p' (β x✝)).op.toLoc ≫ (q' x✝).op.toLoc = (r' x✝).op.toLoc

Tactic:
by grind

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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (p' (β k₁)).op.toLoc ≫ (q' k₁).op.toLoc = (r' k₁).op.toLoc

Tactic:
by grind

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsColimit (Cofork.ofπ ((presheafToSheaf J D).map p) ⋯)

Tactic:
by
        have := IsRegularEpiCategory.regularEpiOfEpi p
        exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f f)))))

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : MonoOver F
f : X ⟶ Y
⊢ range X.arrow ≤ range Y.arrow

Tactic:
rw [← MonoOver.w f]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : MonoOver F
f : X ⟶ Y
⊢ range (Over.Hom.left f.hom ≫ Y.arrow) ≤ range Y.arrow
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

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

Tactic:
exact ⟨fun _ ↦ inferInstance,
    fun _ ↦ Functor.isEquivalence_of_comp_right _ e.functor⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case commfst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ (Iso.refl X).hom =
    ((MonoOver.forget X ⋙ Over.forget X).mapIso (h.iso m)).symm.hom ≫ m

pp: case commsnd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ pullbackπ (h.χ m) h.Ω₀ ≫ (Iso.refl (underlying.obj h.Ω₀)).hom =
    ((MonoOver.forget X ⋙ Over.forget X).mapIso (h.iso m)).symm.hom ≫ h.π m

pp: case commf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ h.χ m ≫ (Iso.refl Ω).hom = (Iso.refl X).hom ≫ h.χ m

pp: case commg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ h.Ω₀.arrow ≫ (Iso.refl Ω).hom = (Iso.refl (underlying.obj h.Ω₀)).hom ≫ h.Ω₀.arrow

Tactic:
all_goals simp [MonoOver.forget]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) (χ m) (truth J)

Tactic:
by
  apply IsPullback.of_map (sheafToPresheaf J _)
  · ext : 1
    simp only [Ω_obj, ObjectProperty.FullSubcategory.comp_hom, χ_hom, terminal_obj, truth_hom,
      ← cancel_mono (closedSieves J).ι, Category.assoc, Subfunctor.lift_ι]
    exact Presheaf.comp_χ_eq m.hom
  · simp only [ObjectProperty.ι_obj, terminal_obj, Ω_obj, ObjectProperty.ι_map, χ_hom, truth_hom]
    apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)
    · simp only [Category.comp_id]
      exact Presheaf.isPullback_χ_truth m.hom
    · simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ F.op.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

Tactic:
mem_distTriang_op_iff

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj (F.op.mapTriangle.obj T)) ∈ Pretriangulated.distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case succ.zero
k n✝ : ℕ
⊢ #(sphere (n✝ + 1) 0 k) ≤ rothNumberNat ((2 * 0 - 1) ^ (n✝ + 1))

pp: case succ.succ
k n✝¹ n✝ : ℕ
⊢ #(sphere (n✝¹ + 1) (n✝ + 1) k) ≤ rothNumberNat ((2 * (n✝ + 1) - 1) ^ (n✝¹ + 1))

Tactic:
· simp

Goal state after:
case succ.succ
k n✝¹ n✝ : ℕ
⊢ #(sphere (n✝¹ + 1) (n✝ + 1) k) ≤ rothNumberNat ((2 * (n✝ + 1) - 1) ^ (n✝¹ + 1))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: k n✝¹ n✝ : ℕ
⊢ ∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Tactic:
simp only [mem_image, and_imp, forall_exists_index,
      sphere, mem_filter]
    rintro _ x hx _ rfl
    exact (map_le_of_mem_box hx).trans_lt sum_lt

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

Goal state before:
pp: case inl
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere 0 d k))
⊢ ↑(d ^ 0) / ↑(0 * d ^ 2) ≤ ↑(#(sphere 0 d k))

pp: case inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
· simp

Goal state after:
case inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inr.inl
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(#(sphere n 0 k))
⊢ ↑(0 ^ n) / ↑(n * 0 ^ 2) ≤ ↑(#(sphere n 0 k))

pp: case inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
· simp

Goal state after:
case inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case zero
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso m (Iio ↑0) (Iio 0) val

pp: case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Tactic:
· simp

Goal state after:
case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ log 2 * 2 ≤ √(log (2 ^ 3))

Tactic:
Real.log_pow,

Goal state after:
⊢ log 2 * 2 ≤ √(↑3 * log 2)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 < ↑⌊x / 2⌋₊

Tactic:
by
  apply lt_of_le_of_lt _ (sub_one_lt_floor _)
  have : 0 < 1 - 2 / exp 1 := by
    rw [sub_pos, div_lt_one (exp_pos _)]
    exact exp_one_gt_two
  rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
    div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff₀ this]
  · exact zero_lt_two
  · exact two_ne_zero

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B * A⁻¹) * #(B * C)

Tactic:
by
  simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_mul_div_mul A B C

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

Goal state before:
pp: ⊢ 0 < ↑6

Tactic:
· simp

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

Goal state before:
pp: case inl
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * rexp (-4 * √(log ↑1)) ≤ 1

pp: case inr
N : ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
· simp

Goal state after:
case inr
N : ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inl
⊢ ↑0 * rexp (-4 * √(log ↑0)) ≤ ↑(rothNumberNat 0)

pp: case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
· simp

Goal state after:
case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
⊢ (t.eTruncLT.obj i).Additive

Tactic:
by
  induction i using WithBotTop.rec
  all_goals dsimp; infer_instance

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
hAA' : ∅ ⊆ A
⊢ #(A * C) * #∅ ≤ #(∅ * C) * #A

pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A C : Finset G
⊢ #(A * C) * #∅ ≤ #(A * ∅) * #(∅ * C)

pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
B : Finset G
n : ℕ
hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * #∅
⊢ ↑(#(∅ * B ^ n)) ≤ (↑(#(∅ * B)) / ↑(#∅)) ^ n * ↑(#∅)

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

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅⁻¹ * ∅ * ∅)) ≤ K ^ 2 * ↑(#∅)

pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A⁻¹ * A * A)) ≤ K ^ 2 * ↑(#A)

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A⁻¹ * A * A)) ≤ K ^ 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅ * ∅⁻¹ * ∅)) ≤ K ^ 3 * ↑(#∅)

pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case inl
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding v) ↔ G.Adj v v

pp: case inr
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

pp: case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : IsEmpty V
⊢ G.maxDegree ≤ k

pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : Nonempty V
⊢ G.maxDegree ≤ k

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
h✝ : Nonempty V
⊢ G.maxDegree ≤ k
Module: Mathlib.Combinatorics.SimpleGraph.Finite

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

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

Tactic:
· rw [eq_bot_iff_isIsolated]
    intro v
    grind [degree_eq_zero, G.degree_le_maxDegree v]

Goal state after:
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: case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.maxDegree = Fintype.card V - 1

pp: case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.maxDegree = Fintype.card V - 1

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.maxDegree = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : IsEmpty V
⊢ G.minDegree ≤ G.maxDegree

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree

Tactic:
· simp

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
he : Nonempty V
⊢ G.minDegree ≤ G.maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : IsEmpty V
⊢ ⊤.minDegree = Fintype.card V - 1

pp: case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.minDegree = Fintype.card V - 1

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
h✝ : Nonempty V
⊢ ⊤.minDegree = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inl
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : IsEmpty V
⊢ G.minDegree ≤ (induce s G).minDegree

pp: case inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
⊢ G.minDegree ≤ (induce s G).minDegree
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
by
  have z := P.sum_card_parts
  rw [← sum_filter_add_sum_filter_not (s := P.parts) (p := fun x ↦ #x = #s / #P.parts + 1),
    hP.filter_ne_average_add_one_eq_average, sum_const_nat (m := #s / #P.parts + 1) (by simp),
    sum_const_nat (m := #s / #P.parts) (by simp), ← hP.filter_ne_average_add_one_eq_average,
    mul_add, add_comm, ← add_assoc, ← add_mul, mul_one, add_comm #_,
    card_filter_add_card_filter_not, add_comm] at z
  rw [← add_left_inj, Nat.mod_add_div, z]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
⊢ (t.eTruncGE.obj i).Additive

Tactic:
by
  induction i using WithBotTop.rec
  all_goals dsimp; infer_instance

Goal state after: