mathlib-initiative/mathlib-tactics huggingface dataset:
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.IsLE X n
i : EInt
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

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

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

Goal state before:
pp: case coe
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 : EInt
X : C
b : ℤ
h : a ≤ WithBotTop.coe b
⊢ IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))

Tactic:
| coe b =>

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

Goal state before:
pp: case coe.coe
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
X : C
a b : ℤ
h : WithBotTop.coe a ≤ WithBotTop.coe b
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι (WithBotTop.coe b)).app X))

Tactic:
| coe b =>

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
inst✝ : IsTriangulated C
a b : EInt
h : a ≤ b
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))

Tactic:
by
  induction a using WithBotTop.rec with
  | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
  | top =>
    obtain rfl : b = ⊤ := by simpa using h
    infer_instance

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
inst✝ : IsTriangulated C
a : EInt
X : C
⊢ IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))

Tactic:
by
  rw [← eTruncLT_obj_map_eTruncLTι_app]
  infer_instance

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
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #({u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}) ≤ 2 ^ (#F - 1)

Tactic:
refine (card_le_card h).trans (card_image_le.trans ?_)
    rw [card_powerset, card_erase_of_mem ht]

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

Goal state before:
pp: case coe
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
X : C
b : ℤ
⊢ IsIso ((t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)).app X)

Tactic:
| coe b =>

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

Goal state before:
pp: case coe.coe
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✝¹ b✝ : EInt
X✝ X : C
a b : ℤ
⊢ IsIso ((t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) (WithBotTop.coe b)).app X)

Tactic:
| coe b =>

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

Goal state before:

Tactic:
_ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
        mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
    _ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
    _ ≤ #A * (#A / #P.parts + 1) :=
        mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity)
    _ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]

Goal state after:
case inr.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A / #P.parts + 1) ≤ ↑(#A) / ↑(#P.parts) + 1

case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) ⊆ (increment hP G ε).parts.offDiag

Tactic:
by
  rintro ⟨Ui, Vj⟩
  simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
    mem_product, mem_attach, true_and, Subtype.exists, and_imp,
    mem_offDiag, forall_exists_index, Ne]
  refine fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, ?_⟩
  rintro rfl
  obtain ⟨i, hi⟩ := nonempty_of_mem_parts _ hUi
  exact hUV.2.2 (P.disjoint.elim_finset hUV.1 hUV.2.1 i (Finpartition.le _ hUi hi) <|
    Finpartition.le _ hVj hi)

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

Goal state before:
pp: case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ {B' | Nonempty (A ≃g B'.coe)} → H' ∈ Set.range toSubgraph

Tactic:
rintro ⟨e⟩
    refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
    simp [toSubgraph, Subgraph.map_comp]

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G'.Subgraph
⊢ ∀ ⦃b : G'.Subgraph⦄, H ≤ b → Subgraph.comap f H ≤ Subgraph.comap f b

Tactic:
H'

Goal state after:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
⊢ H ≤ H' → Subgraph.comap f H ≤ Subgraph.comap f H'
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) =
    ∑ x ∈ (equitabilise h).parts with #x = m, #x + ∑ x ∈ (equitabilise h).parts with #x = m + 1, #x

pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ Disjoint ({u ∈ (equitabilise h).parts | #u = m}) ({u ∈ (equitabilise h).parts | #u = m + 1})

Tactic:
sum_const_nat fun x hx => (mem_filter.1 hx).2,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) =
    #({x ∈ (equitabilise h).parts | #x = m}) * m + ∑ x ∈ (equitabilise h).parts with #x = m + 1, #x

α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ Disjoint ({u ∈ (equitabilise h).parts | #u = m}) ({u ∈ (equitabilise h).parts | #u = m + 1})
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) =
    #({x ∈ (equitabilise h).parts | #x = m}) * m + ∑ x ∈ (equitabilise h).parts with #x = m + 1, #x

pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ Disjoint ({u ∈ (equitabilise h).parts | #u = m}) ({u ∈ (equitabilise h).parts | #u = m + 1})

Tactic:
sum_const_nat fun x hx => (mem_filter.1 hx).2,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) =
    #({x ∈ (equitabilise h).parts | #x = m}) * m + #({x ∈ (equitabilise h).parts | #x = m + 1}) * (m + 1)

α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ Disjoint ({u ∈ (equitabilise h).parts | #u = m}) ({u ∈ (equitabilise h).parts | #u = m + 1})
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
by
  rcases eq_or_ne u v with rfl | h
  · simp [edge_self_eq_bot]
  simp [← disjoint_edgeSet, edgeSet_edge_of_ne h]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ¬n ≤ p.length
⊢ p.getVert n = p.support.getD n v

Tactic:
grind [getVert_of_length_le, length_support]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support
⊢ G.Adj u' v'

Tactic:
have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h
  have h₀ := Nat.zero_add _ ▸ h 0 Nat.zero_lt_two
  have h₁ := Nat.add_comm .. ▸ h 1 Nat.one_lt_two
  rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁
  exact h₀ ▸ h₁ ▸ p.adj_getVert_succ (i := k) <| by grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 / (↑m + 1) ≤ ε ^ 5 / (50 * 2)

Tactic:
one_div_le coe_m_add_one_pos,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 / (ε ^ 5 / (50 * 2)) ≤ ↑m + 1

α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 0 < ε ^ 5 / (50 * 2)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ
V : Type u_1
G : SimpleGraph V
u v : V
n k✝ : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
⊢ (p.take n).IsSubwalk (p.take (k + 1))

Tactic:
apply ih.trans

Goal state after:
case succ
V : Type u_1
G : SimpleGraph V
u v : V
n k✝ : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
⊢ (p.take k).IsSubwalk (p.take (k + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).edgeSet = insert s(v, w) p.edgeSet

Tactic:
ext; simp [or_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.dropLast.support = p.support.dropLast

Tactic:
simp [← support_dropLast_concat hp]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.dropLast.reverse = p.reverse.tail.copy ⋯ ⋯

Tactic:
by
  match p with
  | nil => simp
  | cons hadj p =>
    apply ext_support
    simp [-reverse_cons, List.dropLast_cons_of_ne_nil p.support_ne_nil]

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

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

Tactic:
by
  rw [isClique_map_iff, f.injective.subsingleton_image_iff]
  obtain (hs | hs) := s.subsingleton_or_nontrivial
  · simp [hs, IsClique.of_subsingleton]
  simp [or_iff_right hs.not_subsingleton, Set.image_eq_image f.injective]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ ⊥.IsNClique n s ↔ n ≤ 1 ∧ #s = n

Tactic:
rw [isNClique_iff, isClique_bot_iff]

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case zero
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
hs : G.IsNClique 0 s
⊢ G.IsNClique 0 (insert a (s.erase b))

Tactic:
exact False.elim <| notMem_empty _ (isNClique_zero.1 hs ▸ hb)

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
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤
    (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3 * ↑(Fintype.card α) ^ 3

Tactic:
gcongr; exact triangleRemovalBound_le hε₁

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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
· calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ False

Tactic:
Nat.floor_lt' (by positivity),

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : (triangleRemovalBound (ε / 9) * 27)⁻¹ < ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ False
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
have : A = Prod.map Fin.val Fin.val ''
      (Prod.map Nat.cast Nat.cast '' A : Set (Fin (2 * n).succ × Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Prod.map_apply, Fin.val_natCast, id_eq, Prod.forall,
      Prod.mk.injEq, Nat.mod_succ_eq_iff_lt]
    rintro a b hab
    have := hAn hab
    simp at this
    lia

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
⊢ False
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
Nat.lt_iff_add_one_le

Goal state after:
case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
hL : (a :: L).SortedLT
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise
  simp_rw [Nat.lt_iff_add_one_le] at haL
  have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = L₀.map (· + a + 1) := by
    refine ⟨L.map (· - (a+1)), ?_, ?_⟩
    · rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
    have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
    simp [List.map_congr_left h']
  obtain ⟨L₀, hL₀, rfl⟩ := h'
  have hrw : (2 ^ ·) ∘ (· + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i) := by
    ext x; simp only [Function.comp_apply, pow_add, pow_one]; ac_rfl
  simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]
  nth_rw 1 [← mul_one (a := 2 ^ a)]
  rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
    bitIndices_sum_map_two_pow hL₀]
  simp [add_comm (a := 1), add_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a

Tactic:
refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}
b : α
hb : b ∈ s
⊢ b ≠ a

case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : ∀ b ∈ s, b < a
⊢ ¬s = {a}
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (w.cross v).orthogonal w

Tactic:
exact cross_orthogonal_left h.symm

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

Goal state before:
pp: case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
| ind n hyp =>

Goal state after:
case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
by_contra h

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) = catalan (n + 1)

pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
catalan_succ'

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.nil
s : DyckStep
count_U_eq_count_D✝ : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

Tactic:
rename_i bal _

Goal state after:
case cons.nil
s : DyckStep
bal : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1 (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h']