mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge

Goal state after:
case inr.inr.inr.inr.inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 ≤ #(mulETransformLeft g (s, t)).1 + #(mulETransformLeft g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

case inr.inr.inr.inr.inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 < #(mulETransformRight g (s, t)).1 + #(mulETransformRight g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A⁻¹ * A * A)) ≤ ↑(#A) * (K ^ 2 * ↑(#A))

Tactic:
calc
    (#A * #(A⁻¹ * A * A) : ℝ) = #A * #(A⁻¹ * (A * A)) := by rw [mul_assoc]
    _ ≤ #(A * A) * #(A * (A * A)) := by
      norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)
    _ = #(A ^ 2) * #(A ^ 3) := by simp [pow_succ']
    _ ≤ (K * #A) * (K * #A) := by
      gcongr
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA
    _ = #A * (K ^ 2 * #A) := by ring

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ (K ^ 3) ^ (m - 2) * ↑(#A)

Tactic:
refine inductive_claim_mul hm (fun δ hδ ↦ ?_) ε hε

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ δ i) (finRange 3)).prod) ≤ K ^ 3 * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ f.sym2Map s(a, b) = s(x✝, y✝)

Tactic:
Embedding.sym2Map_apply,

Goal state after:
case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ Sym2.map ⇑f s(a, b) = s(x✝, y✝)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : f.sym2Map s(x✝, y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹

Tactic:
Embedding.sym2Map_apply,

Goal state after:
case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : Sym2.map ⇑f s(x✝, y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.map (⇑f) (SimpleGraph.comap (⇑f) G) ≤ G

Tactic:
map_le_iff_le_comap

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.comap (⇑f) G ≤ SimpleGraph.comap (⇑f) G
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ SimpleGraph.map (⇑f) G ≤ G'

Tactic:
map_le_iff_le_comap

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
⊢ induce {v} G = ⊤

Tactic:
rw [eq_top_iff]; apply le_comap_of_subsingleton

Goal state after:
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
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}

Tactic:
· rwa [mem_filter_univ]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ #{x | v ≠ x} = Fintype.card V - 1

Tactic:
filter_ne

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ #(univ.erase v) = Fintype.card V - 1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
⊢ P ≤ (Finpartition.empty α).copy ⋯

Tactic:
intro x hx

Goal state after:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
x : α
hx : x ∈ P.parts
⊢ ∃ c ∈ ((Finpartition.empty α).copy ⋯).parts, x ≤ c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
⊢ #Q.parts ≤ #P.parts

Tactic:
choose f hP hf using this

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts ≤ #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).sup id = c

Tactic:
sup_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
⊢ id b ⊔ P.parts.sup id = c
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #P.parts * (#s / #P.parts) + #s % #P.parts

Tactic:
exact add_lt_add_of_le_of_lt (mul_le_mul_right (by lia) _) ((hg (f a).1).mp c)

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : Std.Symm r
s t : Finset α
⊢ ↑(#(interedges r s t)) / (↑(#t) * ↑(#s)) = edgeDensity r t s

Tactic:
card_interedges_comm,

Goal state after:
α : Type u_4
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : Std.Symm r
s t : Finset α
⊢ ↑(#(interedges r t s)) / (↑(#t) * ↑(#s)) = edgeDensity r t s
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.deleteEdges ∅ = G

Tactic:
simp [deleteEdges]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.deleteEdges Set.univ = ⊥

Tactic:
simp [deleteEdges]

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

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

Tactic:
sdiff_le_iff

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G ≤ fromEdgeSet s ⊔ G' ↔ G ≤ fromEdgeSet s ⊔ G'
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (G.deleteEdges s).edgeSet = G.edgeSet \ s

Tactic:
simp [deleteEdges]

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

Goal state before:
pp: V : Type u_1
s t : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((fromEdgeSet s).deleteEdges t).Adj x✝¹ x✝ ↔ (fromEdgeSet (s \ t)).Adj x✝¹ x✝

Tactic:
simp +contextual

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = ⊥ ↔ G.edgeSet ⊆ s

Tactic:
simp [deleteEdges]

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
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
⊢ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id

Tactic:
intro x hx

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
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
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
h : G ⊑ H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
have ⟨f⟩ := h
  exact f.maxDegree_mono

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}

Tactic:
refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩
  ext
  · rw [h, singletonSubgraph_verts]
  · simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]
    intro ha
    have ha1 := ha.fst_mem
    have ha2 := ha.snd_mem
    rw [h, Set.mem_singleton_iff] at ha1 ha2
    subst_vars
    exact ha.ne rfl

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

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).verts ⊆ G'.verts

Tactic:
simp +contextual

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s).Adj v w → G'.Adj v w

Tactic:
simp +contextual

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x✝ ∈ (G'.deleteEdges s).verts

Tactic:
simp +contextual

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).Adj x✝¹ x✝

Tactic:
simp +contextual

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : ↑(G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w

Tactic:
simp +contextual

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

Tactic:
simp +contextual

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (G'.verts ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝

Tactic:
simp +contextual

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

Tactic:
simp +contextual

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (s ∩ G'.verts)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝

Tactic:
simp +contextual

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

Goal state before:
pp: case neg
α : 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
hm : m ≠ 0
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ 4 ^ #P.parts - (Fintype.card α / #P.parts - m * 4 ^ #P.parts + 1) +
      (Fintype.card α / #P.parts - m * 4 ^ #P.parts + 1) =
    4 ^ #P.parts

Tactic:
tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card

Goal state after:
case neg
α : 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
hm : m ≠ 0
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ 4 ^ #P.parts = 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case cons.mp
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv

Tactic:
rintro ⟨_ | _, _, h⟩ <;> simp at h

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
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : v = u
⊢ G.Walk u w

Tactic:
subst u

Goal state after:
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
h : v ∈ (cons r p).support
⊢ G.Walk v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ (nil.takeUntil u h✝).append (nil.dropUntil u h✝) = nil

Tactic:
subst u

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count u (nil.takeUntil u h✝).support = 1

Tactic:
subst u

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ nil.support
⊢ List.count u✝ (nil.takeUntil u✝ h).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count s(u, x) (nil.takeUntil u h✝).edges ≤ 1

Tactic:
subst u

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ : V
h : u✝ ∈ nil.support
⊢ List.count s(u✝, x) (nil.takeUntil u✝ h).edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.IsPath

Tactic:
isPath_def

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.length < Fintype.card V

Tactic:
rw [Nat.lt_iff_add_one_le, ← length_support]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
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
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

Tactic:
simp only [hm0, Walk.getVert_cons p h hn0] at hnm
      have hvp : v ∉ p.support := by simp_all
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by lia⟩⟩)).elim

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsClique s ↔ IsChain G.Adj s

Tactic:
by
  simp [IsChain, G.symm.iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this : u = c.support.head ⋯ ∨ u ∈ c.support.tail
⊢ List.count u c.support = 1

Tactic:
have := List.count_eq_one_of_mem hc.support_nodup <| this.resolve_left <| head_support _ ▸ hv

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this✝ : u = c.support.head ⋯ ∨ u ∈ c.support.tail
this : List.count u c.support.tail = 1
⊢ List.count u c.support = 1
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.takeUntil w hw).getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ False

Tactic:
getVert_takeUntil hw hnl

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
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {a, b, c}.sym2

Tactic:
simpa using And.intro hg₁ hh₁

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support <+ u✝ :: p✝.support

Tactic:
· simpa

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts

Tactic:
· simpa

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsPath
⊢ p.IsPath

Tactic:
isPath_def

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsPath
⊢ p.support.Nodup
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 ∨ a✝ = in₁ ?m.3434 ∨ a✝ = in₂ ?m.3437 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝

Tactic:
try tauto

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
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✝

Tactic:
try tauto

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.3745 ∨ a✝ = in₁ ?m.3748 ∨ a✝ = in₂ ?m.3751 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝

Tactic:
try tauto

Goal state after: