mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
A' : Type u_2
inst✝¹ : Category.{v_2, u_2} A'
B : Type u
inst✝ : Category.{v, u} B
F G : A ⊕ A' ⥤ B
η₁ : inl_ A A' ⋙ F ≅ inl_ A A' ⋙ G
η₂ : inr_ A A' ⋙ F ≅ inr_ A A' ⋙ G
⊢ natIsoOfWhiskerLeftInlInr η₁ η₂ =
    (functorEquiv A A' B).unitIso.app F ≪≫
      (functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫ (functorEquiv A A' B).unitIso.symm.app G

Tactic:
cat_disch

Goal state after:
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 : ℕ
x : ↑(F.H' n S.X₄)
⊢ Ext.biprodAddEquiv
      (Ext.biprodAddEquiv.symm
        ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
          ((ConcreteCategory.hom (S.toBiprod F n)) x))) =
    Ext.biprodAddEquiv ((Ext.mk₀ S.shortComplex.g).comp x ⋯)

Tactic:
cat_disch

Goal state after:
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 : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      ((Ext.mk₀ biprod.fst).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).1
          ⋯ +
        (Ext.mk₀ biprod.snd).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).2
          ⋯)
      ⋯ =
    (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₂.op)) x₂ -
      (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₃.op)) x₃

Tactic:
cat_disch

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))
J : GrothendieckTopology C
X : Cᵒᵖ
x : (sieves C).obj X
⊢ x ∈ (Subfunctor.range (Presheaf.truth C)).obj X → x ∈ (closedSieves J).obj X

Tactic:
cat_disch

Goal state after:
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
⊢ φ ≫ g = 0

Tactic:
rw [← cancel_mono ((G.commShiftIso (1 : ℤ)).inv.app T.obj₁), assoc, h₂', zero_comp,
          homEquiv_unit, assoc, reassoc_of% hφ, zero_comp]

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
x₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
x₃ : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₃
hx₃ : (shiftFunctor C 1).map (ι.map x₁) = x₃ ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₃
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk α β γ).obj₁
hk' : x₃ = k' ≫ (Triangle.mk α β γ).mor₁
⊢ (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃

Tactic:
cat_disch

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
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
k : (Triangle.mk α β γ).obj₃ ⟶ ι.obj B
hk : x₁ = (Triangle.mk α β γ).mor₂ ≫ k
⊢ ι.map (πQ f₂ β ≫ ι.preimage k) = ι.map x₂

Tactic:
cat_disch

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
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
this : ι.map f₁ ≫ ι.map f₂ = 0
⊢ ι.map (f₁ ≫ f₂) = ι.map 0

Tactic:
cat_disch

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

Goal state before:
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

Tactic:
exact mul_right_cancel h

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

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

Tactic:
rw [card_range, nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀, card_box]

Goal state after:
case refine_2.ha
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
rw [sub_pos, div_lt_one] <;> exact exp_one_gt_d9.trans' (by norm_num)

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ⌊↑N ^ (↑(nValue N))⁻¹ / 2⌋₊

Tactic:
floor_pos,

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ ↑N ^ (↑(nValue N))⁻¹ / 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
obtain rfl | hN := Nat.eq_zero_or_pos N
  · simp
  obtain h₁ | h₁ := le_or_gt 4096 N
  · exact (roth_lower_bound_explicit h₁).le
  · apply (lower_bound_le_one hN h₁.le).trans
    simpa using! rothNumberNat.monotone hN

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ m ∩ B ^ n ⊆ ↑F₁ ^ (m - 1) * A ∩ (↑F₂ ^ (n - 1) * B)

Tactic:
gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul

Goal state after:
case h₁.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ 2 ⊆ ↑F₁ * A

case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ m ≠ 0

case h₂.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ B ^ 2 ⊆ ↑F₂ * B

case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ n ≠ 0
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
rw [div_eq_mul_inv, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
← card_inv,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B ^ m / B ^ n)⁻¹) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂

Tactic:
disjoint_edgeSet

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ #⊤.edgeFinset

Tactic:
exact card_le_card (edgeFinset_mono le_top)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ G.minDegree = 0 ↔ ∃ v, G.IsIsolated v

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨v, hv⟩ ↦ ?_⟩
  · grind [G.exists_minimal_degree_vertex, degree_eq_zero]
  · grind [G.minDegree_le_degree v, degree_eq_zero]

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

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

Tactic:
cases isEmpty_or_nonempty V
  · simp
  exact IsRegularOfDegree.top.minDegree_eq

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
⊢ ⊤.parts ⊆ {a}

Tactic:
by
  intro b hb
  have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
  split_ifs at hb
  · simp only [copy_parts, empty_parts, notMem_empty] at hb
  · exact hb

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    ∀ x_1 ∈ x,
      ∀ x_2 ⊆ F,
        {i ∈ s | ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u} = x →
          x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
rintro P' i hi P PQ rfl hy₂ j _hj

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
hy₂ : {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u} ⊆ t
j : α
_hj : j ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
⊢ ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp.Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x✝¹ x✝ : V
⊢ M'.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
exact ⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 2 ^ (#(P.nonuniformWitnesses G ε U) - 1) * m ≤ 2 ^ (#P.parts - 1) * m

Tactic:
Finpartition.card_nonuniformWitnesses_le,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 2 ^ (#({t ∈ P.parts | U ≠ t ∧ ¬G.IsUniform ε U t}) - 1) * m ≤ 2 ^ (#P.parts - 1) * m

case ha
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 1 ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert 0 = u

Tactic:
cases w

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.getVert 0 = u

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).getVert 0 = u
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support ≠ []

Tactic:
by cases p <;> simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.head ⋯ = a

Tactic:
by cases p <;> simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support

Tactic:
by cases p <;> simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
by cases p <;> simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support[0] = u

Tactic:
by cases p <;> simp

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
⊢ Walk.map f p = nil ↔ p = nil

Tactic:
by cases p <;> simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
n k✝ : ℕ
p : G.Walk u v
k : ℕ
⊢ (p.drop (k + 1)).IsSubwalk (p.drop k)

Tactic:
induction k generalizing p u with

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

Tactic:
by
  refine p.support_reverse ▸ p.support.nodup_tail_reverse ?_
  rw [← getVert_eq_support_getElem? _ (by lia), List.getLast?_eq_getElem?,
    ← getVert_eq_support_getElem? _ (by rw [Walk.length_support]; lia)]
  simp

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 ≤ ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
exact_mod_cast _root_.zero_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
⊢ (SimpleGraph.map (⇑f) G).Adj (f a) (f b)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ p.support[k]? = q.support[k]?

Tactic:
| inl hk =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i - 1 ∈ {i | i ≤ p.length - 1}

Tactic:
simp only [Set.mem_ofPred_eq, Nat.sub_le_iff_le_add]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i ≤ p.length - 1 + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
intro h'
  have hl := hpc.three_le_length
  by_cases hi' : i ≥ p.length - 1
  · rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'
    lia
  have := hpc.getVert_injOn' (by simp only [Set.mem_ofPred_eq, Nat.sub_le_iff_le_add]; lia)
    (by simp only [Set.mem_ofPred_eq]; lia) h'
  lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ¬G.CliqueFree n
⊢ completeGraph (Fin n) ↪g G

Tactic:
unfold CliqueFree at h

Goal state after:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ¬∀ (t : Finset α), ¬G.IsNClique n t
⊢ completeGraph (Fin n) ↪g G
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
p : G.Path v v
⊢ e ∉ (↑p).edges

Tactic:
by simp [p.loop_eq]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {d, e, f}.sym2

Tactic:
simpa using And.intro hg₂ hh₂

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 ≤ ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
exact_mod_cast _root_.zero_le

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 2
a b : α
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
by simpa [hab.ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
by simpa [hab.ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
⊢ (∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)) ↔ G.CliqueFreeOn s n

Tactic:
refine ⟨fun h t ht ↦ ?_, (· <| map_subtype_subset ·)⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
h : ∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)
t : Finset α
ht : ↑t ⊆ s
⊢ ¬G.IsNClique n t