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✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
hg

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v

Tactic:
refine Finset.card_lt_card <| Finset.ssubset_iff.mpr ⟨w, ?_, ?_⟩

Goal state after:
case refine_1
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset

case refine_2
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
by
      obtain ⟨c, hc, hbc⟩ := hPQ hb
      obtain ⟨d, hd, hcd⟩ := hQR hc
      exact ⟨d, hd, hbc.trans hcd⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #↑⟨p, property✝⟩ = #s / #P.parts + 1 ↔ ↑((f.trans (finCongr ⋯)) ⟨p, property✝⟩) < #s % #P.parts

Tactic:
simp_rw [f, Equiv.trans_apply, Equiv.sumCongr_apply, finCongr_apply, Fin.val_cast]

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ (insert b P.parts).SupIndep id

Tactic:
refine P.supIndep.insert ?_

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint (id b) (P.parts.sup id)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : ¬b \ a = ⊥
⊢ P.parts ⊆ (P.extend hr ⋯ ⋯).parts

Tactic:
· exact Finset.subset_insert _ _

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 / ε ^ 5 < 4 ^ ↑(initialBound ε l)

Tactic:
lt_rpow_iff_log_lt _ zero_lt_four,

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) < ↑(initialBound ε l) * log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
h' : Q = R
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}

Tactic:
subst h'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
hR : Q ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∀ x ∈ P.parts, ∀ ⦃x_1 : α⦄, x_1 ∈ x → ∃ a ∈ ⊥.parts, (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a

Tactic:
exact fun x hx a ha =>
      ⟨{a}, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, mem_singleton_self _⟩

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
hab : b ≤ a
X : C
⊢ (t.eTruncLTLTIsoLT a b hab).inv.app X ≫ (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) = 𝟙 ((t.eTruncLT.obj b).obj X)

Tactic:
by
  simpa using (t.eTruncLTLTIsoLT a b hab).inv_hom_id_app X

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {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
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : ¬(a = 0 ∧ b = 0)
⊢ ∃ 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

Tactic:
not_and_or,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {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
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : ¬a = 0 ∨ ¬b = 0
⊢ ∃ 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
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
replace hs : ε ≤ 0 := by simpa using hs
    exact (hε.not_ge hs).elim

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
inst✝¹ : DecidableRel r
s t : Finset α
inst✝ : Std.Symm r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.1 x.swap.2 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Tactic:
Std.Symm.iff (r := r)

Goal state after:
α : Type u_4
r : α → α → Prop
inst✝¹ : DecidableRel r
s t : Finset α
inst✝ : Std.Symm r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
by
  cases isEmpty_or_nonempty V
  · simp
  obtain ⟨v, h⟩ := exists_maximal_degree_vertex G
  grind [degree_le_maxDegree H (f v), f.degree_le v]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G✝ G₁ G₂ G₃ : SimpleGraph V
H✝ : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst✝¹ : Fintype V
inst✝ : Fintype W
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
exact Fintype.card (Copy H G)

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
⊢ List.map (fun x ↦ x.toProd.1) p.darts = p.support.dropLast

Tactic:
simpa! using! congr_arg List.dropLast (map_fst_darts_append p)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝ v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (Embedding.induce s).toHom (Walk.induce s (cons huu' w) hw) = cons huu' w

Tactic:
by simp [map_induce]

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

Goal state before:
pp: case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
· assumption

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (nil.dropUntil w h).support = ((nil.drop (List.idxOf w nil.support)).copy ⋯ ⋯).support

Tactic:
simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (cast ⋯ nil).support = [u✝]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w = a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
subst h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ w✝ : V
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h✝ : G.Adj w v✝
h : w ∈ (cons h✝ p).support
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : u✝ = u
⊢ List.count s(u, x) (h' ▸ nil).edges ≤ 1

Tactic:
subst h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u✝ ∈ p'.support), List.count s(u✝, x) (p'.takeUntil u✝ h).edges ≤ 1
a✝ : List.Mem u✝ p'.support
⊢ List.count s(u✝, x) (⋯ ▸ nil).edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : Sym2.Rel V (d.toProd.1, d.toProd.2) (u', v')
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
Sym2.rel_iff'

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts
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.length + 1 = p.length

Tactic:
by
  rw [← length_concat _ <| p.adj_penultimate hp, concat_dropLast]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ ∀ ⦃x : α⦄, (∃ (x_1 : x ∈ F), ⟨x, ⋯⟩ ∈ A) → ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x ≠ y → G.Adj x y

Tactic:
intro _ ⟨_, ainA⟩ _ ⟨_, binA⟩ anb

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
anb : x✝ ≠ y✝
⊢ G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ (SimpleGraph.comap (⇑e) G).LocallyLinear ↔ G.LocallyLinear

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]
    exact h.map _
  · rw [← Equiv.coe_toEmbedding, ← map_symm]
    exact LocallyLinear.map _

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
hp : p.IsPath
hnil : ¬p.Nil
hmem : Sym2.Rel V (u, w) (u, p.snd) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd

Tactic:
Sym2.rel_iff'

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.getVert (p.length - 1) = u

Tactic:
exact (hp.eq_penultimate_of_mem_edges <| Sym2.eq_swap ▸ h).symm

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
⊢ G.CliqueFreeOn s n

Tactic:
by
  rintro t hts ht
  obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)
  exact hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 = 2⁻¹

Tactic:
by rw [mul_inv, inv_mul_cancel_right₀]; positivity

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.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ triangleRemovalBound ε * ↑l ^ 3

Tactic:
by
        gcongr; exact (triangleRemovalBound_pos hε).le

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Tactic:
refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑t \ ↑u ⊆ s

case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑u \ ↑t ⊆ s
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
⊢ Eₘ[∅, t] = 0

Tactic:
by simp [mulEnergy]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s, ∅] = 0

Tactic:
by simp [mulEnergy]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ

Tactic:
refine Complex.ofReal_injective ?_

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ ↑(𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re)) = ↑(∏ ψ, c ψ)
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v

Tactic:
rwa [c, zero_smul] at ha

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬(b ≠ m ∧ b ∈ t)
⊢ b < a

Tactic:
not_and_or,

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬b ≠ m ∨ b ∉ t
⊢ b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
hbs : m ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
⊢ m < a

pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < a

Tactic:
· assumption

Goal state after:
case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < a
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ ((w✝ * w✝¹) • (↑x✝³ ⬝ᵥ ↑x✝²) = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
smul_eq_zero_iff_eq

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬(b ≠ m ∧ b ∈ t)
⊢ b < w

Tactic:
not_and_or,

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬b ≠ m ∨ b ∉ t
⊢ b < w
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
⊢ ∃ w, ¬(mk F v hv).orthogonal w

Tactic:
exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
hbs : m ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
⊢ m < w

pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < w

Tactic:
· assumption

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < w
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (a * b) • (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨(a * b) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
smul_eq_zero_iff_eq

Goal state after:
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨(a * b) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨_, h𝒜.1 hs, ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ ⇑toColex)
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ mk F ((crossProduct v) w) ⋯ = mk F ((crossProduct w) v) ⋯

Tactic:
mk_eq_mk_iff_crossProduct_eq_zero,

Goal state after:
case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (crossProduct ((crossProduct v) w)) ((crossProduct w) v) = 0