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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ : ι'
⊢ ∀ ⦃i₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom

Tactic:
j₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
⊢ ∀ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' j₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b) =
    shrinkYonedaObjObjEquiv.symm (𝟙 X)
⊢ shrinkYonedaObjObjEquiv.symm (b ≫ a) = shrinkYonedaObjObjEquiv.symm (𝟙 X)

Tactic:
rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map
        (((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
          ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
← unop_comp,

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map
        ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X))) ≫
            (shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map
      (((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop ≫
        ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop) =
    (((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
          (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))) ≫
      F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop

Tactic:
← unop_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X ≫ (opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
    (((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
          (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))) ≫
      F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop =
    ((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
      ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
        ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop

Tactic:
apply Quiver.Hom.op_inj
  dsimp [opShiftFunctorEquivalence]
  rw [assoc, F.op_commShiftIso_hom_app_assoc _ _ _ (add_neg_cancel n), map_comp,
    map_shiftFunctorCompIsoId_inv_app_assoc, op_comp, op_comp_assoc, op_comp_assoc,
    NatTrans.naturality_assoc, op_map, Iso.inv_hom_id_app_assoc, Quiver.Hom.unop_op]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map
      (((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop ≫
        ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop) =
    F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
← unop_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map
      ((opShiftFunctorEquivalence C n).counitIso.inv.app X ≫ (opShiftFunctorEquivalence C n).counitIso.hom.app X).unop =
    F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
mem_bipartiteBelow

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
⊢ s.prod = t.prod

Tactic:
have : (map g (map f s)).prod = (map g (map f t)).prod := by
      have := hf.mapsTo
      apply hg.map_prod_eq_map_prod <;> simp_all [MapsTo]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map g (map f s)).prod = (map g (map f t)).prod
⊢ s.prod = t.prod
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)

Tactic:
apply log_two_mul_two_le_sqrt_log_eight.trans

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B)) * ((↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)) = (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A) * ↑(#A)

Tactic:
by simp [field, pow_add]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x✝ : G
hx : x✝ ∈ A
⊢ x✝⁻¹ ∈ A

Tactic:
rwa [← hA.inv_eq_self, inv_mem_inv]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ ↑(#(B ^ m * C)) * ↑(#(B ^ n * C)) = ↑(#(C * B ^ m)) * ↑(#(C * B ^ n))

Tactic:
by simp_rw [mul_comm]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)

Tactic:
← inv_inv (B <• s),

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1

Tactic:
exact Finset.EquitableOn.le_add_one hP ht

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q ↑A ⋯).parts

Tactic:
by
  apply card_biUnion
  rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc
  rw [Function.onFun, Finset.disjoint_left]
  rintro d hdb hdc
  rw [Ne, Subtype.mk_eq_mk] at hbc
  exact
    (Q b hb).ne_bot hdb
      (eq_bot_iff.2 <|
        (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Tactic:
obtain ⟨f, hf⟩ := P.exists_enumeration
  obtain ⟨g, hg⟩ := hP.exists_partsEquiv
  let z := fun a ↦ #P.parts * (f a).2 + g (f a).1
  have gl := fun a ↦ (g (f a).1).2
  have less : ∀ a, z a < #s := fun a ↦ by
    rcases hP.card_parts_eq_average (f a).1.2 with (c | c)
    · calc
        _ < #P.parts * ((f a).2 + 1) := by simp only [z, mul_add_one]; gcongr; exact gl a
        _ ≤ #P.parts * (#s / #P.parts) := by gcongr; exact c ▸ (f a).2.2
        _ ≤ #P.parts * (#s / #P.parts) + #s % #P.parts := Nat.le_add_right ..
        _ = _ := Nat.div_add_mod ..
    · rw [← Nat.div_add_mod #s #P.parts]
      exact add_lt_add_of_le_of_lt (mul_le_mul_right (by lia) _) ((hg (f a).1).mp c)
  let z' : s → Fin #s := fun a ↦ ⟨z a, less a⟩
  have bij : z'.Bijective := by
    refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩
    simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e
    have : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
    change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) at e
    simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
    apply_fun f
    exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1
  use Equiv.ofBijective _ bij
  intro a b
  simp_rw [z', z, Equiv.ofBijective_apply, hf a b, Nat.mul_add_mod,
    Nat.mod_eq_of_lt (gl a), Nat.mod_eq_of_lt (gl b), Fin.val_eq_val, g.apply_eq_iff_eq]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s' ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
⊢ False

Tactic:
exact hs hx.1 hy.1

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

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

Tactic:
by
  rw [mem_interedges_iff, mem_interedges_iff, Std.Symm.iff (r := r)]
  exact and_left_comm

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Tactic:
rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t)) = ↑(#s) * ↑(#t)

α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#s) * ↑(#t) ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1

Tactic:
← Set.card_singleton x,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - Fintype.card ↑{x}
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' G'.edgeSet).Nonempty

Tactic:
exact (aux hH hHG').image _

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

Goal state before:
pp: case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : Walk.map f (cons h✝¹ p✝¹) = Walk.map f (cons h✝ p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Tactic:
simp only [map_cons, cons.injEq] at h

Goal state after:
case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝¹ = f v✝ ∧ Walk.map f p✝¹ ≍ Walk.map f p✝
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
hnil : ¬nil.Nil
⊢ w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e

Tactic:
simp at hnil

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

Goal state before:
pp: case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      ([] ++ List.drop (s.length + p₁.length + 1 - s.length) p₁.support ++
        List.drop (s.length + p₁.length + 1 - (s ++ p₁.support).length) t)

Tactic:
List.drop_eq_nil_of_le (by grind),

Goal state after:
case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      ([] ++ [] ++ List.drop (s.length + p₁.length + 1 - (s ++ p₁.support).length) t)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
⊢ nil.takeUntil v ⋯ = nil

Tactic:
simp [Walk.takeUntil]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).takeUntil u ⋯ = nil

Tactic:
simp [Walk.takeUntil]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat (cons ⋯ p.reverse) ≍ Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
rw [concatRecAux, eqRec_heq_iff]
    congr <;> simp

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (p✝.concat h) = nil.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil

Tactic:
simp only [concat_nil, cons.injEq] at he

Goal state after:
case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : v✝ = w ∧ p✝.concat h ≍ nil
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil
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
p' : G.Walk v w
⊢ ↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail

Tactic:
by
  rw [support_append, ← Multiset.coe_add, coe_support]

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

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

Tactic:
rw [edges_cons, List.count_cons]
        split_ifs with h''
        · simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''
          obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
          · exact (h' rfl).elim
          · cases p' <;> simp!
        · apply ih

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

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

Tactic:
by
  simpa using p.darts_takeUntil_prefix_darts h |>.length_le

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
h : p.IsCycle
⊢ p.reverse.IsCycle

Tactic:
simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢
  exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet
  let s := {n | ∃ (u v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
  have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.isTrail.length_le_card_edgeFinset
  obtain ⟨x⟩ := N
  obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
  refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
  have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
  lia

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support

Tactic:
rw [Nat.min_eq_right h, ← length_support, List.drop_length]
    simp [h]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
simp [*, ← length_eq_zero_iff]

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

Goal state before:
pp: case hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil

Tactic:
simp [*, ← length_eq_zero_iff]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hadj : G.Adj u✝ v✝
p : G.Walk v✝ w✝
hind : ∀ (hp : G.Adj p.penultimate w✝), p.dropLast.concat hp = p
hp : G.Adj (cons hadj p).penultimate w✝
⊢ (cons hadj p).dropLast.concat hp = cons hadj p

Tactic:
cases p with
    | nil => rfl
    | _ => simp [hind]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' s) ↔ G.IsClique s

Tactic:
isClique_map_iff,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ ((⇑f '' s).Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
simp [or_iff_right hs.not_subsingleton, Set.image_eq_image f.injective]

Goal state after: