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
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v := by
    ext w
    rw [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
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case pos
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [eq_bot_iff_isIsolated]
    intro v
    grind [degree_eq_zero, G.degree_le_maxDegree v]
  · convert maxDegree_bot_eq_zero
    assumption

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
p : α
hpi : p ∈ (P i).parts
⊢ p ∉ (P j).parts

Tactic:
hpj

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
p : α
hpi : p ∈ (P i).parts
hpj : p ∈ (P j).parts
⊢ False
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (↑(Finset.map { toFun := singleton, inj' := ⋯ } s)).PairwiseDisjoint id

Tactic:
rw [Finset.coe_map]
        exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#∅)
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
rw [Finset.card_empty, Nat.cast_zero] at ht₂

Goal state after:
case inr.inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(#t₁) ≤ 0
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'

Tactic:
by
    rw [deleteEdges, sdiff_le_iff]

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.degree v = 0

Tactic:
← G'.coe_degree ⟨v, hv⟩

Goal state after:
case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.coe.degree ⟨v, hv⟩ = 0
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} =
    sSup {x | ∃ x_1 y, ∃ (_ : s(x_1, y) ∈ G.edgeSet), fromEdgeSet {s(x_1, y)} = x}

Tactic:
mem_edgeSet

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 v w
h : u ∈ p.support
⊢ (p.drop (List.idxOf u p.support)).support <:+ p.support

Tactic:
drop_support_eq_support_drop_min,

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ List.drop (min (List.idxOf u p.support) p.length) p.support <:+ p.support
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 v w
h : u ∈ p.support
⊢ (p.dropUntil u h).support <:+ p.support

Tactic:
grw [dropUntil_eq_drop, support_copy, drop_support_eq_support_drop_min, List.drop_suffix]

Goal state after:
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.drop k).IsSubwalk (p.drop n)
⊢ (p.drop (k + 1)).IsSubwalk (p.drop n)

Tactic:
apply IsSubwalk.trans ?_ ih

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.take n).getVert m = p.getVert (min n m)

Tactic:
induction p generalizing n m <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
m : ℕ
⊢ (nil.take 0).getVert m = nil.getVert (min 0 m)

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
m n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert m = nil.getVert (min (n✝ + 1) m)

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m : ℕ
⊢ ((cons h✝ p✝).take 0).getVert m = (cons h✝ p✝).getVert (min 0 m)

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (min (n✝ + 1) m)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath ↔ p.IsPath

Tactic:
by
  constructor <;> intro h <;> convert! h.reverse; simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
hp : (cons hadj p).IsPath
⊢ (cons hadj p).tail.IsPath

Tactic:
| cons hadj p =>

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
n m : ℕ
⊢ ((p.drop n).drop m).support = (p.drop (n + m)).support

Tactic:
drop_support_eq_support_drop_min,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ List.drop (min m (p.drop n).length) (List.drop (min n p.length) p.support) =
    List.drop (min (n + m) p.length) p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ List.take (n + 1) p.support ++ (p.drop n).support.tail = p.support

Tactic:
drop_support_eq_support_drop_min,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ List.take (n + 1) p.support ++ (List.drop (min n p.length) p.support).tail = p.support
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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
⊢ False

Tactic:
obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'

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}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : ⊤.Adj w✝¹ w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)

Tactic:
← f.topEmbedding.map_adj_iff

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
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 ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ n = m

Tactic:
have : p.length - n = p.length - m := Walk.length_reverse _ ▸ hpc.reverse.getVert_injOn
    (by simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia)
    (by simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia)
    (by simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by lia, hnm,
      show p.length - (p.length - m) = m by lia])

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
this✝ : 3 ≤ p.length
this : p.length - n = p.length - m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #(s.erase a) = n - 1

Tactic:
rw [card_erase_of_mem ha, hs.2]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
by rwa [← take_spec _ h] at hc

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
by rwa [← take_spec _ h] at hc

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
⊢ G.CliqueFree m → G.CliqueFree n

Tactic:
intro hG

Goal state after:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
⊢ G.CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), s(x, y) ∉ G.edgeSet

Tactic:
mem_edgeSet

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ G.cliqueFinset n = ∅ ↔ G.CliqueFree n

Tactic:
by
  simp_rw [CliqueFree, eq_empty_iff_forall_notMem, mem_cliqueFinset_iff]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
⊢ ε ≤ 0

Tactic:
by
  have := h₀ (empty_subset _)
  rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty] at this
  exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ δₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, divConst]; gcongr; exact card_le_univ _

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

Goal state before:
pp: case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ List.Pairwise (fun a_1 b ↦ a_1 - (a + 1) < b - (a + 1)) L

Tactic:
Pairwise.and_mem,

Goal state after:
case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ List.Pairwise (fun x y ↦ x ∈ L ∧ y ∈ L ∧ x - (a + 1) < y - (a + 1)) L
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ StrictMono fun s ↦ ∑ k ∈ ofColex s, n ^ k

Tactic:
intro s

Goal state after:
n : ℕ
hn : 2 ≤ n
s : Colex (Finset ℕ)
⊢ ∀ ⦃b : Colex (Finset ℕ)⦄, s < b → (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) b
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), #s ≤ #(s.biUnion t)

Tactic:
intro s

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
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
⊢ (∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a) → f ∈ derangements (Subtype p)

Tactic:
rintro hf ⟨a, ha⟩ hfa

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ False
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∈ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
exact ⟨p, hl₁, hl₂⟩

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(#(A⁻¹ * A)) < 3 / 2 * ↑(#A)

Tactic:
card_inv_mul_of_doubling_lt_three_halves h

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(#(A * A)) < 3 / 2 * ↑(#A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count U (List.take i (List.take (i + k) ↑p)) + count D (List.drop i (List.take (i + k) ↑p)) ≤
    count U (List.take i (List.take (i + k) ↑p)) + count U (List.drop i (List.take (i + k) ↑p))

Tactic:
← count_append,

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count U (List.take i (List.take (i + k) ↑p)) + count D (List.drop i (List.take (i + k) ↑p)) ≤
    count U (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take i (List.take (i + k) ↑p)) + count D (List.drop i (List.take (i + k) ↑p)) ≤
    count U (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p))

Tactic:
← count_append,

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p)) ≤
    count U (List.take i (List.take (i + k) ↑p) ++ List.drop i (List.take (i + k) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hmem : a ∈ m.toFinset.erase 0
⊢ (count a m)! * rest = ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
rw [← Finset.mul_prod_erase _ _ hmem]

Goal state after:
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:
simp_rw [Pi.add_apply, apply_eq_zero_of_not_le h, zero_add]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
j : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (j + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (j + 1) * x ^ ((j + 1) * (3 * j + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow j n x

Tactic:
induction j with
  | zero =>
    simp [tprod_one_sub_pow_eq_powMulProdOneSubPow_zero hsum h, powMulProdOneSubPow,
      ← sub_eq_add_neg]
  | succ n ih =>
    rw [ih, tsum_powMulProdOneSubPow _ hx hsum h, Finset.sum_range_succ _ (n + 1)]
    have h (n) : (n + 1 + 1) * (3 * (n + 1) + 2) / 2 =
        (n + 1) * (3 * n + 4) / 2 + (2 * n + 3) := by
      rw [← Nat.add_mul_div_left _ _ (by simp)]
      ring_nf
    simp_rw [h]
    have h (n) : (n + 1 + 1) * (3 * (n + 1) + 4) / 2 =
        (n + 1) * (3 * n + 4) / 2 + (3 * n + 5) := by
      rw [← Nat.add_mul_div_left _ _ (by simp)]
      ring_nf
    simp_rw [h]
    ring_nf

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u v : α
⊢ (ofSimpleGraph G).Adj u v ↔ G.Adj u v

Tactic:
simp [Adj]

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e e' : Set α
H : Hypergraph α
he : e ∈ E(H)
he' : e' ∈ E(H)
⊢ e = e' ↔ ∀ x ∈ V(H), x ∈ e ↔ x ∈ e'

Tactic:
grind [he.subset_vertexSet, he'.subset_vertexSet]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ (∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) →
    ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
ihα

Goal state after:
α : Type u
inst✝ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
⊢ ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ #(prefixed s) = (#s)! * (Fintype.card X - #s)!

Tactic:
simpa [-mem_prefixed] using Fintype.card_congr (prefixedEquiv s)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
⊢ M.Dep (C ∪ X)

Tactic:
rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans sdiff_subset))]

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
⊢ ¬M.Indep (C ∪ X)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
x : σ → R
hx : ∀ (i : σ), x i ∈ S (e i)
⊢ ∀ (i : τ), (x ∘ ⇑e.symm) i ∈ S i

Tactic:
intro s

Goal state after:
case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
x : σ → R
hx : ∀ (i : σ), x i ∈ S (e i)
s : τ
⊢ (x ∘ ⇑e.symm) s ∈ S s
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ (C ∩ K).Nonempty

Tactic:
inter_eq_self_of_subset_right hKC

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ K.Nonempty