mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).1 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1

pp: case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2

Tactic:
· rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_fst, Iso.inv_hom_id_apply]

Goal state after:
case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ ≫
      𝟙 (Precomp.obj (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (F.H' n₀ S.X₄) 3) =
    𝟙 (Precomp.obj (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (F.H' n₀ S.X₄) 2) ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
rw [comp_id, id_comp]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ =
    (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
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
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₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ adj.unit.app Z ≫ G.map h = 0
⊢ 0 ≫ G.map T.mor₃ = 0

Tactic:
zero_comp

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✝¹³ : 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₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ adj.unit.app Z ≫ G.map h = 0
⊢ 0 = 0
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 ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂
⊢ (shiftFunctor C 1).map (ι.map k) = 0

Tactic:
zero_comp

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
⊢ (shiftFunctor C 1).map (ι.map k) = 0
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 ≫ (Triangle.mk α β γ).mor₃
⊢ (shiftFunctor C 1).map (ι.map k) = 0

Tactic:
zero_comp

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
⊢ (shiftFunctor C 1).map (ι.map k) = 0
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
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
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
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
have : admissibleMorphism ι f₁ := by simp [hA]

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
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
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
this : admissibleMorphism ι f₁
⊢ Nonempty (Abelian.AbelianStruct f₁)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
⊢ ThreeGPFree (⇑f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ habc
  rw [h ha hb hc (hf (mul_mem_mul ha hc) (mul_mem_mul hb hb) <| by rwa [map_mul, map_mul])]

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

Goal state before:
pp: case inl.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c ∈ s
hd : d ∈ s
⊢ b = c

pp: case inr.inl.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

pp: case inr.inl.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c

pp: case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

pp: case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
· exact ha hc hd h

Goal state after:
case inr.inl.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

case inr.inl.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c

case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case refine_2
n d : ℕ
⊢ (n * (d - 1) ^ 2 + 1) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))

Tactic:
nsmul_eq_mul,

Goal state after:
case refine_2
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2 + 1) * (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 2 / rexp 1 < 1

Tactic:
div_lt_one

Goal state after:
⊢ 2 < rexp 1

⊢ 0 < rexp 1
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ F ⊆ A ∧ ↑(Nat.card ↥F) ≤ K ∧ A ⊆ F * (B / B) ∧ (↑F).Finite

Tactic:
simp [*]

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

Goal state before:
pp: ⊢ 4096 < rexp 16

Tactic:
← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp),

Goal state after:
⊢ log 4096 < 16
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(rothNumberNat N)

Tactic:
simpa using! rothNumberNat.monotone hN

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x

Tactic:
ext : 1 <;> dsimp
  · rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]
    exact inter_subset_union
  · rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
    exact inter_subset_union

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

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

Tactic:
inter_comm

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x y : G
⊢ Set.LeftInvOn (fun ab' ↦ x •> ab'.1) (fun z ↦ (x⁻¹ * z, z⁻¹ * y)) ↑(x •> A ∩ y •> B)

Tactic:
simp [Set.LeftInvOn]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ Set.LeftInvOn (fun ab ↦ (ab.1, ab.2⁻¹)) (fun ab ↦ (ab.1, ab.2⁻¹)) ↑({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x})

Tactic:
simp [Set.LeftInvOn]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ Set.RightInvOn (fun ab ↦ (ab.1, ab.2⁻¹)) (fun ab ↦ (ab.1, ab.2⁻¹)) ↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x})

Tactic:
simp [Set.LeftInvOn]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(x •> A ∩ B⁻¹) = #(B⁻¹ ∩ x •> A)

Tactic:
inter_comm

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(B⁻¹ ∩ x •> A) = #(B⁻¹ ∩ x •> A)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
rw [← card_smul_inter, ← card_inter_smul, inter_comm]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
u v : W
⊢ (SimpleGraph.map (⇑f) G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v

Tactic:
by
  dsimp [SimpleGraph.map, Relation.Map]
  grind [SimpleGraph.Adj.ne]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeSet

Tactic:
← mem_edgeFinset

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
s : Set V
t : Set W
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
hi : Set.InjOn (⇑φ) s
⊢ Injective ⇑(induceHom φ φst)

Tactic:
simpa [Set.MapsTo.restrict_inj]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
this : (P.parts.sup fun x ↦ x) = a
⊢ (P.parts.sup fun i ↦ i) ⊓ b = b

Tactic:
rw [this, inf_eq_right.mpr hb]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤ ((∑ x ∈ s, f x - #s • ((∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2

Tactic:
nsmul_eq_mul,

Goal state after:
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤
    ((∑ x ∈ s, f x - ↑(#s) * ((∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
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 → ℕ := 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 (fun a ↦ ⟨#P.parts * ↑(f a).snd + ↑(g (f a).fst), ⋯⟩) bij) a) % #P.parts =
      ↑((Equiv.ofBijective (fun a ↦ ⟨#P.parts * ↑(f a).snd + ↑(g (f a).fst), ⋯⟩) bij) b) % #P.parts

Tactic:
Equiv.ofBijective_apply,

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 ↔
    (#P.parts * ↑(f a).snd + ↑(g (f a).fst)) % #P.parts = (#P.parts * ↑(f b).snd + ↑(g (f b).fst)) % #P.parts
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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ IsIso (t.eTruncGEToGEGE a b)

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)