mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ (Sieve.overEquiv (Over.mk a)).symm R =
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ (Sieve.overEquiv (Over.mk a)).symm R ≤
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R)) ≤
    (Sieve.overEquiv (Over.mk a)).symm R
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      (Ext.biprodAddEquiv.symm
        ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
          (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))))
      ⋯ =
    (ConcreteCategory.hom (S.fromBiprod F n))
      (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))

Tactic:
rw [Ext.biprodAddEquiv_symm_apply,
    Iso.addCommGroupIsoToAddEquiv_symm_apply,
    fromBiprod_biprodIsoProd_inv_apply]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      ((Ext.mk₀ biprod.fst).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).1
          ⋯ +
        (Ext.mk₀ biprod.snd).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).2
          ⋯)
      ⋯ =
    (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₂.op)) x₂ -
      (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₃.op)) x₃
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : ↑(#s) < #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) < b

Tactic:
by
  simp_rw [cast_card] at ht ⊢
  exact
    exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) = mulRothNumber s

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_5
β₁ : Type u_6
β₂ : Type u_7
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A : Set α
B₁ : Set β₁
B₂ : Set β₂
f₁ : α → β₁
f₂ : α → β₂
n : ℕ
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (fun x ↦ (f₁ x, f₂ x)) s).prod = (map (fun x ↦ (f₁ x, f₂ x)) t).prod

Tactic:
by
    simp [Prod.ext_iff, fst_prod, snd_prod,
      h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h]

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

Goal state before:
pp: case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑↑(k + 1) ↔ ↑x ≤ k

Tactic:
rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n = ↑(d ^ n) / ↑(n * d ^ 2)

Tactic:
cast_mul,

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n = ↑(d ^ n) / (↑n * ↑(d ^ 2))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ n / ↑d ^ 2 / ↑n = ↑d ^ n / ↑(d ^ 2) / ↑n

pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ≠ 0

Tactic:
cast_pow

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ n / ↑d ^ 2 / ↑n = ↑d ^ n / ↑d ^ 2 / ↑n

n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ≠ 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith

Goal state after:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift A to Finset G using hA

Goal state after:
G : Type u_1
inst✝ : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : ↑(Nat.card ↑(↑A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (B / B) ∧ F.Finite
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * (2 * √(log ↑N)) ≤ log ↑N

Tactic:
rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ √(log ↑N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ {x} * A' = {x} * A ∩ (C * A)

Tactic:
hA',

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ {x} * (A ∩ ({x}⁻¹ * C * A)) = {x} * A ∩ (C * A)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ #(SimpleGraph.map (⇑f) G).edgeFinset = #G.edgeFinset

Tactic:
edgeFinset_map

Goal state after:
V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ #(map f.sym2Map G.edgeFinset) = #G.edgeFinset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
⊢ ∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p

Tactic:
by
  by_cases hbot : ⊥ ∈ parts
  · simp only [Finpartition.ofPairwiseDisjoint]
    rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]
    · simp
    grind
  · simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hucard : #u = m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - a + a) * m + a = m * 4 ^ #P.parts + a

Tactic:
Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card),

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hucard : #u = m * 4 ^ #P.parts + a
⊢ 4 ^ #P.parts * m + a = m * 4 ^ #P.parts + a
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ a ∈ P.part a ↔ a ∈ s

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
· simp [part, ha, choose_property (p := fun s => a ∈ s) P.parts (P.existsUnique_mem ha)]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ a ∈ P.part a ↔ a ∈ s
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
X : C
n : ℤ
inst✝ : t.IsLE X n
j : EInt
hj : WithBotTop.coe n < j
⊢ IsZero ((t.eTruncGE.obj j).obj X)

Tactic:
induction j using WithBotTop.rec with
  | bot => simp at hj
  | coe j =>
    simp only [WithBotTop.coe_lt_coe] at hj
    have := t.isLE_of_le X n (j - 1) (by lia)
    exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _
  | top => simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) *
        (4 ^ #P.parts - (Fintype.card α / #P.parts - m * 4 ^ #P.parts) +
          (Fintype.card α / #P.parts - m * 4 ^ #P.parts)) +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) *
        4 ^ #P.parts =
    stepBound #P.parts

Tactic:
Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card),

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * 4 ^ #P.parts +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) *
        4 ^ #P.parts =
    stepBound #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w}

Tactic:
ext u

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff_of_subset (by simp [ha]),
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - G.degree t - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

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

Tactic:
constructor <;>
      simp +contextual only [induce_adj, imp_true_iff, and_true]

Goal state after:
case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts

Tactic:
exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε

Tactic:
· gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.getVert i ∈ p.support

Tactic:
induction p generalizing i <;> cases i

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.getVert 0 ∈ nil.support

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ nil.getVert (n✝ + 1) ∈ nil.support

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✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
⊢ (cons h✝ p✝).getVert 0 ∈ (cons h✝ p✝).support

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✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
n✝ : ℕ
⊢ (cons h✝ p✝).getVert (n✝ + 1) ∈ (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
induction p generalizing i <;> cases i

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 < nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 < nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i < p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).getVert 0 =
    if 0 < (cons h✝ p✝).length then (cons h✝ p✝).getVert 0 else q.getVert (0 - (cons h✝ p✝).length)

case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i < p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
n✝ : ℕ
⊢ ((cons h✝ p✝).append q).getVert (n✝ + 1) =
    if n✝ + 1 < (cons h✝ p✝).length then (cons h✝ p✝).getVert (n✝ + 1) else q.getVert (n✝ + 1 - (cons h✝ p✝).length)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
induction p generalizing i <;> cases i

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 ≤ nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i ≤ p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).getVert 0 =
    if 0 ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert 0 else q.getVert (0 - (cons h✝ p✝).length)

case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i ≤ p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
n✝ : ℕ
⊢ ((cons h✝ p✝).append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert (n✝ + 1) else q.getVert (n✝ + 1 - (cons h✝ p✝).length)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

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

Tactic:
exact (h' rfl).elim

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : s(u', v') ∈ p.edges
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support

Tactic:
have := (isSubwalk_toWalk_iff_mem_edges <| p.adj_of_mem_edges h).mpr h

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : s(u', v') ∈ p.edges
this : ⋯.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
by
  refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
  · rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne
    obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
    rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
    rwa [← hux, ← hvy]
  rw [Set.image_preimage_eq_iff]
  intro x hxt
  obtain ⟨y, hyt, hyne⟩ := ht.exists_ne x
  obtain ⟨-, u, v, -, rfl, rfl⟩ := h hyt hxt hyne
  exact Set.mem_range_self _

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ u :: (cons h p).dropLast.support ~ u :: (cons h p).tail.support

Tactic:
← List.perm_append_singleton,

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).dropLast.support ++ [u] ~ u :: (cons h p).tail.support
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:
refine ⟨fun h ↦ ?_, ?_⟩

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

case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

case refine_2
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s
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
hu : u ∈ c.support
⊢ (c.rotate u hu).edges.Nodup ↔ c.edges.Nodup

Tactic:
(c.rotate_edges u hu).perm.nodup_iff

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ c.edges.Nodup ↔ c.edges.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique (Fintype.card (Fin n)) (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
rw [Fintype.card_fin] at this

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n