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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l✝ : List G.Dart
d₁ d₂ : G.Dart
l : List G.Dart
hne : d₁ :: d₂ :: l ≠ []
hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)
⊢ (ofDarts (d₁ :: d₂ :: l) hne hchain).darts = d₁ :: d₂ :: l

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
l✝ : List G.Dart
d₁ d₂ : G.Dart
l : List G.Dart
hne : d₁ :: d₂ :: l ≠ []
hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)
⊢ (ofDarts (d₁ :: d₂ :: l) hne hchain).darts = d₁ :: d₂ :: l
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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B))

Tactic:
have : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / ↑50 ≤
      (↑1 - ε ^ 5 / 50) * G.edgeDensity (A.biUnion id) (B.biUnion id) := by
    rw [sub_mul, one_mul, sub_le_sub_iff_left]
    refine mul_le_of_le_one_right (by sz_positivity) ?_
    exact mod_cast G.edgeDensity_le_one _ _

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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ofSupport nil.support ⋯ ⋯ = nil.copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ofSupport nil.support ⋯ ⋯ = nil.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
w : V
h : G.Adj u w
⊢ ofSupport (cons h nil).support ⋯ ⋯ = (cons h nil).copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
w : V
h : G.Adj u w
⊢ ofSupport (cons h nil).support ⋯ ⋯ = (cons h nil).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
p✝ : G.Walk u v✝
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
⊢ ofSupport (cons h₁ (cons h₂ p)).support ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v✝ : V
p✝ : G.Walk u v✝
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
⊢ ofSupport (cons h₁ (cons h₂ p)).support ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯
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
hp : ¬nil.Nil
⊢ ofDarts nil.darts ⋯ ⋯ = nil.copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp✝ : ¬p.Nil
hp : ¬nil.Nil
⊢ ofDarts nil.darts ⋯ ⋯ = nil.copy ⋯ ⋯
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
w : V
h : G.Adj u w
x✝ : ¬(cons h nil).Nil
⊢ ofDarts (cons h nil).darts ⋯ ⋯ = (cons h nil).copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
h : G.Adj u w
x✝ : ¬(cons h nil).Nil
⊢ ofDarts (cons h nil).darts ⋯ ⋯ = (cons h nil).copy ⋯ ⋯
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
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
x✝ : ¬(cons h₁ (cons h₂ p)).Nil
⊢ ofDarts (cons h₁ (cons h₂ p)).darts ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v✝ : V
p✝ : G.Walk u v✝
hp : ¬p✝.Nil
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
x✝ : ¬(cons h₁ (cons h₂ p)).Nil
⊢ ofDarts (cons h₁ (cons h₂ p)).darts ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
n : ℕ
hn : n ≠ 0
⊢ (cons h p).drop n = (p.drop (n - 1)).copy ⋯ ⋯

Tactic:
apply ext_support
  obtain ⟨_, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.ne_zero_iff_zero_lt.mp hn)
  conv_lhs => unfold drop
  simp

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
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support

Tactic:
support_tail_of_not_nil q hq

Goal state after:
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
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail
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 : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.tail.support

Tactic:
support_tail_of_not_nil q hq

Goal state after:
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 : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hadj : G.Adj v v
hp : (cons hadj nil).IsCircuit
⊢ 3 ≤ (cons hadj nil).length

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hadj : G.Adj v v
hp : (cons hadj nil).IsCircuit
⊢ 3 ≤ (cons hadj nil).length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp : (cons h✝¹ (cons h✝ nil)).IsCircuit
⊢ 3 ≤ (cons h✝¹ (cons h✝ nil)).length

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp : (cons h✝¹ (cons h✝ nil)).IsCircuit
⊢ 3 ≤ (cons h✝¹ (cons h✝ nil)).length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝² : V
h✝² : G.Adj v v✝²
v✝¹ : V
h✝¹ : G.Adj v✝² v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ v
hp : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsCircuit
⊢ 3 ≤ (cons h✝² (cons h✝¹ (cons h✝ p✝))).length

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝² : V
h✝² : G.Adj v v✝²
v✝¹ : V
h✝¹ : G.Adj v✝² v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ v
hp : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsCircuit
⊢ 3 ≤ (cons h✝² (cons h✝¹ (cons h✝ p✝))).length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ∈ {i | i ≤ (cons h p).length}
m : ℕ
hm : m ∈ {i | i ≤ (cons h p).length}
hnm : (cons h p).getVert n = (cons h p).getVert m
⊢ n = m

Tactic:
simp only [length_cons, Set.mem_ofPred_eq] at hn hm hnm

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ nil.tail.reverse = nil.reverse.dropLast.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse = (cons hadj p).reverse.dropLast.copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse = (cons hadj p).reverse.dropLast.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse.support = (cons hadj p).reverse.dropLast.support

Tactic:
simp [-reverse_cons]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ nil.dropLast.reverse = nil.reverse.tail.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).dropLast.reverse = (cons hadj p).reverse.tail.copy ⋯ ⋯

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).dropLast.reverse = (cons hadj p).reverse.tail.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).dropLast.reverse = (cons hadj p).reverse.tail.copy ⋯ ⋯

Tactic:
apply ext_support
    simp [-reverse_cons, List.dropLast_cons_of_ne_nil p.support_ne_nil]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
⊢ Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length} → (cons h q).IsPath

Tactic:
intro hinj

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ (cons h q).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ p.support[k]? = q.support[k]?
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
exact Finset.one_lt_card_iff_nontrivial.mp ht

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear

Tactic:
exact h.map _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ∈ {i | i ≤ p.length - 1}
m : ℕ
hm : m ∈ {i | i ≤ p.length - 1}
hnm : p.getVert n = p.getVert m
⊢ n = m

Tactic:
simp only [Set.mem_ofPred_eq] at *

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : Walk.nil.IsTrail
h : ∀ (v : V) (w : G.Walk v v), w.IsSubwalk Walk.nil → ¬w.IsCycle
⊢ Walk.nil.IsPath

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : Walk.nil.IsTrail
h : ∀ (v : V) (w : G.Walk v v), w.IsSubwalk Walk.nil → ¬w.IsCycle
⊢ Walk.nil.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
⊢ (cons hadj p).IsPath

Tactic:
| =>

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
⊢ (cons hadj p).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False

Tactic:
exact hG _ ⟨hs.isClique.subset hts, ht⟩

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

Goal state before:
pp: case right.refine_2
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ q'.support <+ q.support

Tactic:
exact isSubwalk_iff_support_isInfix.mp hq' |>.sublist

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
⊢ ↑(G.edgeDensity U V) ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 ≤
    ↑(G.edgeDensity U V) ^ 2 - ↑(G.edgeDensity U V) * ε ^ 5 / 25 + ε ^ 10 / 2500

Tactic:
by
      gcongr; exact mod_cast G.edgeDensity_le_one ..

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * δₘ[A, B] = ↑(#(A / B))

Tactic:
exact card_mul_divConst _ _

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert 0 A ∪ (a +ᵥ A.subsetSum)) ≤ #(insert a A).subsetSum

Tactic:
union_subset insert_subset vadd_subset

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert a A).subsetSum ≤ #(insert a A).subsetSum
Module: Mathlib.Data.Nat.BitIndices

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

Tactic:
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

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g ↑t ⋯ x
s : Set α
hs : s.Finite
⊢ ∃ t, ∃ (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Tactic:
obtain ⟨t, ht, ht'⟩ := hχ hs.toFinset

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g ↑t ⋯ x
s : Set α
hs : s.Finite
t : Finset α
ht : hs.toFinset ⊆ t
ht' : ∀ x ∈ hs.toFinset, χ x = g ↑t ⋯ x
⊢ ∃ t, ∃ (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ w ⬝ᵥ (crossProduct v) w = 0

Tactic:
rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
hst : s ≠ t
⊢ ∃ b ∈ ofColex (toColex t), b ∉ ofColex (toColex s) ∧ a ≤ b

Tactic:
refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ ofColex (toColex s)
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : L
ha : a • f v = f u
⊢ f (τ a • v) = f u

Tactic:
f.map_smulₛₗ,

Goal state after:
case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : L
ha : a • f v = f u
⊢ σ (τ a) • f v = f u
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 : (b * a) • (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨(b * a) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
mul_comm b a,

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 : (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⟩
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
h₁ z₁ : G
hh₁ : (h₁, z₁).1 ∈ ↑(↑H).toFinset
hz₁ : (h₁, z₁).2 ∈ ↑Z
h₂ z₂ : G
hh₂ : (h₂, z₂).1 ∈ ↑(↑H).toFinset
hz₂ : (h₂, z₂).2 ∈ ↑Z
h : (fun p ↦ p.1 * p.2) (h₁, z₁) = (fun p ↦ p.1 * p.2) (h₂, z₂)
⊢ (h₁, z₁) = (h₂, z₂)

Tactic:
simp only [Set.coe_toFinset, SetLike.mem_coe] at *

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
h₁ z₁ h₂ z₂ : G
h : h₁ * z₁ = h₂ * z₂
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
hz₂ : z₂ ∈ Z
⊢ (h₁, z₁) = (h₂, z₂)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f + ⇑g) a b = 0

Tactic:
Pi.add_apply,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ f a b + g a b = 0