mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

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

Tactic:
and_comm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥

Tactic:
by
  rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ G = ⊥

Tactic:
rw [eq_bot_iff_isIsolated]
    intro v
    grind [degree_eq_zero, G.degree_le_maxDegree v]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ P.parts.sup id = ⊥

Tactic:
rw [h]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ ∅.sup id = ⊥
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition a)

Tactic:
rw [h]

Goal state after:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition ⊥)
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
a b : EInt
hab : a ⟶ b
⊢ t.eTruncGE.map hab ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 a ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab

Tactic:
by
    replace hab := leOfHom hab
    induction a using WithBotTop.rec; rotate_right
    · apply (isZero_zero _).eq_of_src
    all_goals
      induction b using WithBotTop.rec <;> simp at hab <;>
        dsimp [eTruncGE, eTruncLT] <;>
        simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
rw [h]

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ t ⊂ ⊥,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
P : Finpartition ⊥
⊢ ∀ x ∈ P.parts, #(x \ {y ∈ (Finpartition.empty (Finset α)).parts | y ⊆ x}.biUnion id) ≤ m

Tactic:
by simp [Unique.eq_default P, -bot_eq_empty]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#(interedges r s t)) + ↑(#(interedges (fun x y ↦ ¬r x y) s t)) = ↑(#s) * ↑(#t)

Tactic:
exact mod_cast card_interedges_add_card_interedges_compl r s t

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 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε'

Tactic:
by
  refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h <;> gcongr

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:
interedges_def,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #(Gᶜ.interedges s t) = #(s ×ˢ t)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H.verts H'.verts → Disjoint H H'

Tactic:
rintro hdisj M' ⟨hsub₀, _⟩ ⟨hsub₁, _⟩
    rw [le_bot_iff]
    ext
    · grind [verts_bot]
    · exact ⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩

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

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

Tactic:
by
  ext; rw [edge_adj]; simp_all

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
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m ≤ 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V))

Tactic:
rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]

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
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))

α : 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
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'
    exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ (p.takeUntil w h).support = ((p.take (List.idxOf w p.support)).copy ⋯ ⋯).support

Tactic:
induction p with
  | nil =>
    simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]
    grind [mem_support_nil_iff, support_nil]
  | cons hadj p ih =>
    grind [takeUntil, support, copy_rfl_rfl, support_take]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ (p.takeUntil w h).snd = p.snd

Tactic:
apply p.getVert_takeUntil h
  contrapose hsu
  symm
  simpa [length_eq_zero_iff] using hsu

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x y : V
hyv : y ≠ v
hx : x ∈ p.support
hy : y ∈ q.support
⊢ x ≠ y

Tactic:
by
  rintro rfl
  have hq : ¬q.Nil := by
    intro hq
    simp [nil_iff_support_eq.mp hq, hyv] at hy
  have hx' : x ∈ q.tail.support := by
    rw [support_tail_of_not_nil q hq]
    rw [mem_support_iff] at hy
    exact hy.resolve_left hyv
  exact IsPath.disjoint_support_of_append hpq hq hx hx'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet
  let s := {n | ∃ (u v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
  have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset
  obtain ⟨x⟩ := N
  obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
  refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
  have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
  lia

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

Goal state before:
pp: 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
this : ∀ (k : ℕ), p.support[k]? = q.support[k]?
⊢ p = q

Tactic:
exact ext_support <| List.ext_getElem?_iff.mpr this

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ G.IsClique s

Tactic:
rw [isClique_iff]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos.inl
α : 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
hx : x ∈ s \ {v}
hy : y ∈ s \ {v}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact hv.mono le_sup_left hx hy hxy

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

Goal state before:
pp: case pos
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
⊢ False

Tactic:
rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : i - 1 = 0 ∨ i - 1 = p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n

Tactic:
by
  simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3431, in₁ ?m.3434, in₂ ?m.3437} ↔ a✝ ∈ {in₀ a✝⁵, in₁ b✝¹, in₂ c✝}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3431 ∨ a✝ = in₁ ?m.3434 ∨ a✝ = in₂ ?m.3437 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3588, in₁ ?m.3591, in₂ ?m.3594} ↔ a✝ ∈ {in₁ b✝¹, in₀ a✝⁵, in₂ c✝}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3588 ∨ a✝ = in₁ ?m.3591 ∨ a✝ = in₂ ?m.3594 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3745, in₁ ?m.3748, in₂ ?m.3751} ↔ a✝ ∈ {in₀ a✝⁵, in₂ c✝¹, in₁ b✝}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3745 ∨ a✝ = in₁ ?m.3748 ∨ a✝ = in₂ ?m.3751 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.3902, in₁ ?m.3905, in₂ ?m.3908} ↔ a✝ ∈ {in₂ c✝¹, in₀ a✝⁵, in₁ b✝}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3902 ∨ a✝ = in₁ ?m.3905 ∨ a✝ = in₂ ?m.3908 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4059, in₁ ?m.4062, in₂ ?m.4065} ↔ a✝ ∈ {in₁ b✝¹, in₂ c✝¹, in₀ a✝³}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4059 ∨ a✝ = in₁ ?m.4062 ∨ a✝ = in₂ ?m.4065 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝³
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.4216, in₁ ?m.4219, in₂ ?m.4222} ↔ a✝ ∈ {in₂ c✝¹, in₁ b✝¹, in₀ a✝³}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4216 ∨ a✝ = in₁ ?m.4219 ∨ a✝ = in₂ ?m.4222 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³
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 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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * ((1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U))) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)))

Tactic:
mul_div_left_comm

Goal state after:
α : 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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U))) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
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 α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : ↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) < ε * ↑(Fintype.card α ^ 2)
t : Finset α
ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
exact triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t

Tactic:
by
  ext; exact is3Clique_iff

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A / A) * #A ≤ #(A * A) * #(A * A)

Tactic:
exact ruzsa_triangle_inequality_div_mul_mul ..

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2} =
    (s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯

Tactic:
aesop (add unsafe mul_mem_mul)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t

Tactic:
aesop (add unsafe mul_mem_mul)

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.true
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit true n).bitIndices).sum = bit true n

Tactic:
simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ ofColex (toColex t)
hbc : b ≤ c
⊢ b ≤ a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ ofColex (toColex t)
hbc : b ≤ c
⊢ b < a
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
ha : a = 0
⊢ D'.rep = 0

Tactic:
by simp [← hD, ha]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card L ≤ #(s.biUnion t) + Fintype.card L - #s
⊢ #s ≤ #(s.biUnion t)

Tactic:
le_tsub_iff_left (le_add_left s.card_le_univ),

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : #s + Fintype.card L ≤ #(s.biUnion t) + Fintype.card L
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ (_ : ∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f), ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f

Tactic:
exists_prop,

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ ((∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f) ∧ ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a

Tactic:
and_comm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ⇑f ∧ fixedPoints ⇑f ⊆ {a} ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))

Tactic:
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]

Goal state after: