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
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
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₁)))) ≫
      (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj ((α ∘ β) k₁)) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ r' k₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj ((α ∘ β) k₂)) =
    pullFunctorObjHom w' (pullFunctorObj w D) (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₂))))

Tactic:
pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)

Goal state after:
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
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₁)))) ≫
      (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj ((α ∘ β) k₁)) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ r' k₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj ((α ∘ β) k₂)) =
    ((F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ q' k₁).op.toLoc ⋯).inv.toNatTrans.app
          ((pullFunctorObj w D).obj (β k₁)) ≫
        (pullFunctorObj w D).hom (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂) ⋯ ⋯ ≫
          (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ q' k₂).op.toLoc ⋯).hom.toNatTrans.app
            ((pullFunctorObj w D).obj (β k₂))) ≫
      (F.map f₂.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₂))))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom (eval S α (typesGlue S hs α f))) = f

Tactic:
funext x

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : (fun X ↦ X) α
⊢ (ConcreteCategory.hom (eval S α (typesGlue S hs α f))) x = f x
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤

Tactic:
· rintro ⟨a, h⟩
    rw [h]
    simpa using congr($(h₁ (.op Y)) a)

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = 0
⊢ 0 = (shiftFunctor C 1).map 0

Tactic:
Functor.map_zero

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝²³ : 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
E : C ≌ D
inst✝¹³ : E.functor.CommShift ℤ
inst✝¹² : E.inverse.CommShift ℤ
inst✝¹¹ : E.CommShift ℤ
D' : Type u_3
inst✝¹⁰ : Category.{v_3, u_3} D'
inst✝⁹ : HasZeroObject D'
inst✝⁸ : Preadditive D'
inst✝⁷ : HasShift D' ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D' n).Additive
inst✝⁵ : Pretriangulated D'
E' : D ≌ D'
inst✝⁴ : E'.functor.CommShift ℤ
inst✝³ : E'.inverse.CommShift ℤ
inst✝² : E'.CommShift ℤ
inst✝¹ : E.IsTriangulated
inst✝ : E'.IsTriangulated
⊢ (E.trans E').IsTriangulated

Tactic:
dsimp [Equivalence.IsTriangulated]
  rw [trans_toAdjunction]
  infer_instance

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

Goal state before:
pp: case refine_1
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ (shiftFunctor C 1).map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
case refine_1
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_2
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ (shiftFunctor C (-1)).map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
case refine_2
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ 0 = 0
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
B : α → Finset β
s : Finset α
⊢ ∑ j ∈ s, #(B j) = ∑ x ∈ s.biUnion B, #{j | j ∈ s ∧ x ∈ B j}

Tactic:
convert sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow (fun j x => x ∈ B j)
  · grind [bipartiteAbove]
  · grind [bipartiteBelow]

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

Goal state before:
pp: n d : ℕ
x₁ : Fin n → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin n), x i < d}
⊢ ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂

Tactic:
x₂

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

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

Tactic:
have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn

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

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)

Tactic:
rw [log_rpow zero_lt_two, ← div_lt_iff₀']

Goal state after:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2

N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6
Module: Mathlib.Combinatorics.Additive.ETransform

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

Tactic:
smul_finset_inter,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
Module: Mathlib.Combinatorics.Additive.ETransform

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

Tactic:
smul_finset_inter,

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

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

Tactic:
smul_finset_inter,

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
ht : t.Nonempty
a : α
hs : {a}.Nonempty
ih :
  ∀ (a_1 b : Finset α),
    a_1.Nonempty → b.Nonempty → DevosMulRel (a_1, b) ({a}, t) → minOrder α ≤ ↑(#(a_1 * b)) ∨ #a_1 + #b ≤ #(a_1 * b) + 1
hst : #{a} ≤ #t
⊢ minOrder α ≤ ↑(#({a} * t)) ∨ #{a} + #t ≤ #({a} * t) + 1

pp: case inr.inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
· simp [add_comm]

Goal state after:
case inr.inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ ↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) ≤ K ^ 3 * ↑(#A)

Tactic:
have : K ^ 2 ≤ K ^ 3 := by gcongr; simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
this : K ^ 2 ≤ K ^ 3
⊢ ↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inr.inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
⊢ ↑(#(A⁻¹ * A⁻¹ * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
· simp [*, pow_succ', ← mul_inv_rev] at hA ⊢
    nlinarith

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
⊢ v₁✝ ∈ u ↓∩ s → ∀ ⦃v₂ : ↑u⦄, v₂ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂

Tactic:
hs

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
⊢ ∀ ⦃v₂ : ↑u⦄, v₂ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
h : v ≠ w
⊢ f v ≠ f w

Tactic:
exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : {v | Odd (G.degree v)}.Nonempty
⊢ 0 < k

Tactic:
← card_pos,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < #{v | Odd (G.degree v)}
⊢ 0 < k
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2

Tactic:
by
  simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h]

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborFinset ↑v ∩ s.toFinset = G.neighborFinset ↑v
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v

Tactic:
← map_neighborFinset_induce v

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #p = #s / #P.parts + 1 ↔ ↑((f.trans (finCongr ⋯)) ⟨p, property✝⟩) < #s % #P.parts

Tactic:
f,

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #p = #s / #P.parts + 1 ↔
    ↑((((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)).trans
            (finCongr ⋯))
          ⟨p, property✝⟩) <
      #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ (i, i').1 ⊓ (i, i').2) = P.parts.sup id ⊓ Q.parts.sup id

pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a

Tactic:
· simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]
          rfl

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ a ⊓ Q.parts.sup id = a

Tactic:
Q.sup_parts,

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ a ⊓ a = a
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∀ (y : Finset α), (fun t ↦ t ∈ P.parts ∧ a ∈ t) y → y = t

Tactic:
rintro u ⟨hu, hu'⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
u : Finset α
hu : u ∈ P.parts
hu' : a ∈ u
⊢ u = t
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
⊢ a = b

Tactic:
have : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
this : NeZero #P.parts
⊢ a = b
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := ⋯
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := ⋯
bij : Function.Bijective z'
⊢ ∀ (a b : ↥s),
    P.part ↑a = P.part ↑b ↔ ↑((Equiv.ofBijective z' bij) a) % #P.parts = ↑((Equiv.ofBijective z' bij) b) % #P.parts

Tactic:
intro a b

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
bij : Function.Bijective z'
a b : ↥s
⊢ P.part ↑a = P.part ↑b ↔ ↑((Equiv.ofBijective z' bij) a) % #P.parts = ↑((Equiv.ofBijective z' bij) b) % #P.parts