mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N

Tactic:
by
  have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
  rw [dValue, floor_pos, ← log_le_log_iff zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀,
    inv_mul_eq_div, sub_nonneg, le_div_iff₀]
  · have : (nValue N : ℝ) ≤ 2 * √(log N) := by
      apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
      rw [two_mul, add_le_add_iff_left]
      apply le_sqrt_of_sq_le
      rw [one_pow, le_log_iff_exp_le hN₀]
      exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
    apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _
    rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
    · apply log_two_mul_two_le_sqrt_log_eight.trans
      apply Real.sqrt_le_sqrt
      exact log_le_log (by simp) (mod_cast hN₃)
    exact hN₃.trans_lt' (by simp)
  · exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by simp)
  · exact (rpow_pos_of_pos hN₀ _).ne'
  · exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two

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

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

case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:

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

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

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

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty
  · simp
  induction n with
  | zero => simp
  | succ n ih =>
    refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)
    calc
      ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
        = #(B ^ n * A * B) * #A := by rw [pow_succ, mul_left_comm, mul_assoc]
      _ ≤ #(A * B) * #(B ^ n * A) := mod_cast pluennecke_petridis_inequality_mul _ hAB
      _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by rw [mul_comm _ A]; gcongr
      _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by simp [field, pow_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2

Tactic:
by
  refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)
  rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x.1 = s ∧ x.2 = t
⊢ min (minOrder α) ↑(#s + #t - 1) ≤ ↑(#(s * t))

Tactic:
obtain ⟨rfl, rfl⟩ := hx

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
x : Finset α × Finset α
hs : x.1.Nonempty
ht : x.2.Nonempty
⊢ min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ ↑(#(x.1 * 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 : G
⊢ A.convolution B x ≠ 0 ↔ x ∈ A * B

Tactic:
suffices A.convolution B x ≠ 0 ↔ 0 < A.convolution B x by simp [this]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≠ 0 ↔ 0 < A.convolution B x
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap f G'

Tactic:
intro v w

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
s : Set V
⊢ induce s ⊥ = ⊥

Tactic:
by
  dsimp

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

Goal state before:
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:
· apply le_minDegree_of_forall_le_degree
    exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

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

Goal state before:
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
w✝ : V
hv : G.maxDegree = G.degree w✝
⊢ G.maxDegree ≤ k

Tactic:
exact hv ▸ h _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ Disjoint b a

Tactic:
have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
⊢ Disjoint b a
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
y : α
hy : (∃ x ∈ ↑P.parts, x ⊓ b = y) ∧ ¬y = ⊥
px : α
hpx : px ∈ ↑P.parts
hxy : px ⊓ b ≠ y
right✝ : ¬px ⊓ b = ⊥
⊢ (Disjoint on id) (px ⊓ b) y

Tactic:
obtain ⟨⟨py, hpy, rfl⟩, _⟩ := hy

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
px : α
hpx : px ∈ ↑P.parts
right✝¹ : ¬px ⊓ b = ⊥
py : α
hpy : py ∈ ↑P.parts
hxy : px ⊓ b ≠ py ⊓ b
right✝ : ¬py ⊓ b = ⊥
⊢ (Disjoint on id) (px ⊓ b) (py ⊓ b)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q ↑a_2 ⋯).parts

Tactic:
rintro ⟨A, hA, h⟩

Goal state after:
case mpr
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
⊢ (↑parts).PairwiseDisjoint id

Tactic:
intro a ha b hb hab

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ (Disjoint on id) a b
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
X : C
n : ℤ
inst✝ : t.IsGE X n
i : EInt
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
by
  induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isGE_of_isZero _ (by simp) _

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
X : C
n : ℤ
inst✝ : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
⊢ j ≤ n

Tactic:
by simpa using hj

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

Goal state before:
pp: ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a✝ : α × β
⊢ a✝ ∈ interedges r (s.biUnion f) t ↔ a✝ ∈ s.biUnion fun a ↦ interedges r (f a) t

Tactic:
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Tactic:
by
  rw [← card_product, interedges_def, interedges_def]
  have : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2} := by
    refine filter_congr fun x hx ↦ ?_
    rw [mem_product] at hx
    rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
  rw [this, ← card_union_of_disjoint, filter_union_filter_not_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ↑(#((P.sparsePairs G ε).biUnion fun x ↦
          match x with
          | (U, V) => G.interedges U V)) ≤
    ε * (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
calc
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, (#(G.interedges UV.1 UV.2) : 𝕜) := mod_cast card_biUnion_le
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (#UV.1 * #UV.2) := ?_
    _ ≤ ∑ UV ∈ P.parts.offDiag, ε * (#UV.1 * #UV.2) := by gcongr; apply filter_subset
    _ = ε * ∑ UV ∈ P.parts.offDiag, (#UV.1 * #UV.2 : 𝕜) := (mul_sum _ _ _).symm
    _ ≤ _ := ?_
  · gcongr with ⟨U, V⟩ hUV
    simp only [mk_mem_sparsePairs, ne_eq, ← card_interedges_div_card, Rat.cast_div,
      Rat.cast_natCast, Rat.cast_mul] at hUV
    refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le
    exact mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
      (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)
  norm_cast
  gcongr
  calc
    (_ : ℕ) ≤ _ := sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2)
            ((#A / #P.parts + 1) ^ 2 : ℕ) ?_
    _ ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 := ?_
    _ ≤ _ := by gcongr; apply Nat.mul_div_le
  · simp only [Prod.forall, and_imp, mem_offDiag, sq]
    rintro U V hU hV -
    exact_mod_cast Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)
  · rw [smul_eq_mul, offDiag_card, Nat.mul_sub_right_distrib, ← sq, ← mul_pow, mul_add_one (α := ℕ)]
    exact Nat.sub_le _ _

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x x✝ : V
⊢ x✝ ∈ (G.deleteIncidenceSet x).support → x✝ ∈ G.support \ {x}

Tactic:
simp_rw [mem_support, deleteIncidenceSet_adj]

Goal state after:
V : Type u_1
G : SimpleGraph V
x x✝ : V
⊢ (∃ w, G.Adj x✝ w ∧ x✝ ≠ x ∧ w ≠ x) → x✝ ∈ G.support \ {x}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
ext e; induction e using Sym2.ind; simp

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

Goal state before:
pp: case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w

Tactic:
intro v w

Goal state after:
case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
v w : V
⊢ (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ G.edgeSet ∧
    ∀ (x : G.Subgraph) (x_1 : Nonempty (H ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map
      (Subtype.val ∘
        ⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm)
      e =
    Sym2.map Subtype.val e

Tactic:
congr 1 with x

Goal state after:
case e_f
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ G.edgeSet ∧
    ∀ (x : G.Subgraph) (x_1 : Nonempty (H ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
x : ↑(Subgraph.map (Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).toHom G').verts
⊢ (Subtype.val ∘
        ⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm)
      x =
    ↑x
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)
⊢ G'.spanningCoe.degree v = G'.degree v

Tactic:
rw [← card_neighborSet_eq_degree, Subgraph.degree]
  congr!

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe ≤ G'.coe

Tactic:
intro v w

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : ↑(G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
by_cases x = v <;> aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (⇑f.toEmbedding '' ↑univ) ∧ Fintype.card β = Fintype.card β

Tactic:
coe_univ,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (⇑f.toEmbedding '' Set.univ) ∧ Fintype.card β = Fintype.card β
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
⊢ p = Path.nil

Tactic:
obtain ⟨_ | _, h⟩ := p
  · rfl
  · simp at h

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

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : t ∈ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G

pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : t ∉ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G

Tactic:
· obtain ⟨x, hx⟩ := mt
    by_cases ms : s ∈ Set.range φ
    · obtain ⟨y, hy⟩ := ms
      have e := @hφ x y
      simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e
      rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
    · unfold replaceVertex at hφ
      refine Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩
      simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]
      rw [apply_ite (G.Adj · _), apply_ite (G.Adj _ ·), apply_ite (G.Adj _ ·)]
      convert! @hφ a b <;> simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : t ∉ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)

Tactic:
exact ⟨(edge_comm .. ▸ hc).erase_of_sup_edge_of_mem h2, hc.erase_of_sup_edge_of_mem h1⟩

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ ∃ s, G.IsNClique G.cliqueNum s

Tactic:
by_cases h : BddAbove {n | ∃ s, G.IsNClique n s}
  · exact Nat.sSup_mem ⟨0, by simp⟩ h
  · simp [cliqueNum, h]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ⊆ t
hc : ¬t ⊆ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
⊢ False

Tactic:
have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ⊆ t
hc : ¬t ⊆ ↑s
fint : Fintype ↑t
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b c : α
hbc : G.Adj b c
e : α
hde : G.Adj e e
hab : G.Adj e b
hac : G.Adj e c
⊢ s(e, e) = s(e, b) ∨ s(e, e) = s(e, c) ∨ s(e, e) = s(b, c)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hac : G.Adj d c
hbc : G.Adj e c
hab : G.Adj d e
⊢ s(d, e) = s(d, e) ∨ s(d, e) = s(d, c) ∨ s(d, e) = s(e, c)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hab : G.Adj d b
hbc : G.Adj b e
hac : G.Adj d e
⊢ s(d, e) = s(d, b) ∨ s(d, e) = s(d, e) ∨ s(d, e) = s(b, e)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hbc : G.Adj d c
hac : G.Adj e c
hab : G.Adj e d
⊢ s(d, e) = s(e, d) ∨ s(d, e) = s(e, c) ∨ s(d, e) = s(d, c)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a c : α
hac : G.Adj a c
e : α
hde : G.Adj e e
hab : G.Adj a e
hbc : G.Adj e c
⊢ s(e, e) = s(a, e) ∨ s(e, e) = s(a, c) ∨ s(e, e) = s(e, c)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hab : G.Adj a d
hac : G.Adj a e
hbc : G.Adj d e
⊢ s(d, e) = s(a, d) ∨ s(d, e) = s(a, e) ∨ s(d, e) = s(d, e)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hbc : G.Adj b d
hab : G.Adj e b
hac : G.Adj e d
⊢ s(d, e) = s(e, b) ∨ s(d, e) = s(e, d) ∨ s(d, e) = s(b, d)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hac : G.Adj a d
hab : G.Adj a e
hbc : G.Adj e d
⊢ s(d, e) = s(a, e) ∨ s(d, e) = s(a, d) ∨ s(d, e) = s(e, d)

Tactic:
simp [*] at *

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

Goal state before:
pp: case refine_2.inr.inr.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b : α
hab : G.Adj a b
e : α
hde : G.Adj e e
hac : G.Adj a e
hbc : G.Adj b e
⊢ s(e, e) = s(a, b) ∨ s(e, e) = s(a, e) ∨ s(e, e) = s(b, e)

Tactic:
simp [*] at *

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : G.IsIndepSet ↑t
⊢ #t ≤ G.indepNum

Tactic:
← isClique_compl

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ G.indepNum
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (G.badVertices ε s t) t)) ≤ ↑(#(G.badVertices ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
exact G.card_interedges_badVertices_le

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
⊢ ∃ G' ≤ G, ∃ x, ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3

Tactic:
by_contra! h
  refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset
  intro G' _ hG hG'
  exact le_of_not_gt fun i ↦ h G' hG _ i hG'

Goal state after: