mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
W : D
f' : W ⟶ F.obj X✝
w✝ : EffectiveEpi f'
i : W ⟶ F.obj Z✝
w : i ≫ F.map g = f' ≫ F.map f
⊢ EffectiveEpi (F.map (F.preimage (F.effectiveEpiOver W ≫ f')))

Tactic:
simp only [Functor.map_preimage]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
W : D
f' : W ⟶ F.obj X✝
w✝ : EffectiveEpi f'
i : W ⟶ F.obj Z✝
w : i ≫ F.map g = f' ≫ F.map f
⊢ EffectiveEpi (F.effectiveEpiOver W ≫ f')
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_1.of
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (extensiveCoverage C).coverings Y ∨ T ∈ (regularCoverage C).coverings Y
⊢ T ∈ (coherentCoverage C).coverings Y

Tactic:
exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F →
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
rintro hF X _ ⟨Y, f, rfl, _⟩
    exact (equalizerConditionMap_iff_nonempty_isLimit F f).1 (hF f)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))

Tactic:
by
        rw [← Functor.map_comp, ← Functor.map_comp, Adj.unit_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁) ≫ D₂.hom q f₁ f₁ ⋯ ⋯ =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯

Tactic:
D₂.hom_self _ _ hf₁,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁) ≫ 𝟙 ((F.map f₁.op.toLoc).toFunctor.obj (D₂.obj i₁)) =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: case e'_3
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
e_2✝ : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ curry (F ◁ g ≫ α) = g ≫ curry α

Tactic:
rw [curry_natural_left]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : PresheafIsGeneratedBy F x
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
inst✝ : Epi f
⊢ PresheafIsGeneratedBy F' fun i ↦ (ConcreteCategory.hom (f.app (X i))) (x i)

Tactic:
by
  simpa only [Subfunctor.range_eq_top f] using h.range f

Goal state after:
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ (pullback.fst f f).hom ≫ p = (pullback.snd f f).hom ≫ p

Tactic:
rw [← cancel_mono i]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ ((pullback.fst f f).hom ≫ p) ≫ i = ((pullback.snd f f).hom ≫ p) ≫ i
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
⊢ (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) ≫ (shiftFunctor C 1).map (Triangle.mk α β γ).mor₁ = 0

Tactic:
simp [← Functor.map_comp, hl]

Goal state after:
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
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, 1

Tactic:
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ #s ≤ mulRothNumber A

Tactic:
← s.card_image_of_injOn ((invFunOn_injOn_image f _).mono hfsA)

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ #(image (invFunOn f ↑A) s) ≤ mulRothNumber A
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case succ
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
⊢ x₁ i = x₂ i

Tactic:
have x := (map_eq_iff hx₁ hx₂).1 h

Goal state after:
case succ
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
⊢ x₁ i = x₂ i
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
refine (div_le_div_of_nonneg_left (by positivity) (by positivity) ?_).trans hk

Goal state after:
case inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inr.inr.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

Tactic:
one_le_cast

Goal state after:
case inr.inr.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ n
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
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:
classical
  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
  exact ⟨F, by norm_cast; simp [*]⟩

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

Goal state before:
pp: case refine_1
α : 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 : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g ∈ a⁻¹ • ↑s

Tactic:
← hsg,

Goal state after:
case refine_1
α : 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 : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c * g ∈ a⁻¹ • ↑(op g • s)
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂

Tactic:
rw [isCorner_iff, isCorner_iff]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v) → u ∈ ⇑f '' G.neighborSet v

pp: case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)

Tactic:
· exact fun ⟨hne, v', u', hadj, hv, hu⟩ ↦ ⟨u', f.injective hv ▸ hadj, hu⟩

Goal state after:
case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)
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]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ ((image (fun x ↦ x ⊓ b) P.parts).erase ⊥).sup id = b

Tactic:
by
    simp only [sup_erase_bot, sup_image, Function.id_comp, (sup_inf_distrib_right ..).symm]
    have : P.parts.sup (fun x => x) = a := P.sup_parts
    rw [this, inf_eq_right.mpr hb]

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 α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁

Tactic:
by
    simp_rw [mem_interedges_iff]
    exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.bot
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
inst✝ : IsTriangulated C
a✝ b✝ b : EInt
X✝ X : C
a : ℤ
⊢ IsIso ((t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊥).app X)

Tactic:
simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)

Goal state after:
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.edgeFinset \ G.incidenceFinset t ∪ image (fun x ↦ s(x, t)) (G.neighborFinset s)) \ {s(t, t)}) =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
card_sdiff_of_subset (by simp [ha]),

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 \ G.incidenceFinset t ∪ image (fun x ↦ s(x, t)) (G.neighborFinset s)) - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp.refl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ s(⟨v, hv'⟩, ⟨w, hw'⟩) ∉ s

Tactic:
simpa only [Sym2.eq_swap]

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

Goal state before:
pp: case mp.swap
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ s(⟨w, hv'⟩, ⟨v, hw'⟩) ∉ s

Tactic:
simpa only [Sym2.eq_swap]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (⊤.induce s).coe.spanningCoe

Tactic:
exact (Subgraph.spanningCoe_coe _).symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
⊢ H.spanningCoe ≤ G

Tactic:
by
  intro v w hvw
  grind [adj_congr_of_sym2]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u✝ : V
d : G.Dart
h : d.toProd.2 = u✝
⊢ List.IsChain G.DartAdj (d :: nil.darts)

Tactic:
exact .singleton _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.1) p.darts = p.support.dropLast

Tactic:
by
  simpa! using! congr_arg List.dropLast (map_fst_darts_append p)

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * 49⁻¹ = 1 + ε ^ 5 / 49

Tactic:
by rw [div_eq_mul_inv]

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

pp: case inr
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support

Tactic:
· exact dart_fst_mem_support_of_mem_darts _ hd

Goal state after:
case inr
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support
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:
rw [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.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 = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
rw! [

Goal state after:
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 = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
hp : ¬nil.Nil
⊢ cons ⋯ nil.tail = nil

Tactic:
simp at hp ⊢

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hp : ¬(cons h✝ p✝).Nil
⊢ cons ⋯ (cons h✝ p✝).tail = cons h✝ p✝

Tactic:
simp at hp ⊢

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
hp : ¬p.Nil
⊢ cons ⋯ p.tail = p

Tactic:
by
  cases p <;> simp at hp ⊢

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
hp : ¬p.Nil
⊢ p.dropLast.support = p.support.dropLast

Tactic:
by
  simp [← support_dropLast_concat hp]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.tail.Nil

Tactic:
simp at hp ⊢

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

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

Tactic:
simp at hp ⊢

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.tail.Nil

Tactic:
by
  cases p <;> simp at hp ⊢

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.dropLast.Nil

Tactic:
simp at hp ⊢

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).dropLast.Nil

Tactic:
simp at hp ⊢

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.dropLast.Nil

Tactic:
by
  cases p <;> simp at hp ⊢

Goal state after: