mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_1
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ (shiftFunctor C 1).map (ι.map 0) = 0

Tactic:
Functor.map_zero,

Goal state after:
case refine_1
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ (shiftFunctor C 1).map 0 = 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : x₂ 0 + (∑ x, x₁ x.succ * d ^ ↑x) * d = x₂ 0 + (∑ x, x₂ x.succ * d ^ ↑x) * d
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
add_right_inj,

Goal state after:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (∑ x, x₁ x.succ * d ^ ↑x) * d = (∑ x, x₂ x.succ * d ^ ↑x) * d
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ s ≠ 0

Tactic:
grind [Multiset.card_eq_zero]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ t ≠ 0

Tactic:
grind [Multiset.card_eq_zero]

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

Goal state before:
pp: M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B₁ B₂ : Set X
hB : B₁ ⊆ B₂
hAB : CovBySMul M K A B₁
⊢ CovBySMul M K A B₂

Tactic:
by simpa using hAB.trans (.of_subset (M := M) hB)

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

Goal state before:
pp: case hbc
⊢ log 2 * 2 ^ 2 ≤ 3

Tactic:
linarith only [log_two_lt_d9.le]

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

Goal state before:
pp: ⊢ 4096 < rexp 16

Tactic:
rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
    ← rpow_natCast, log_rpow zero_lt_two, cast_ofNat]

Goal state after:
⊢ 12 * log 2 < 16
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ m ∩ B ^ n ⊆ ↑F₁ ^ (m - 1) * A ∩ (↑F₂ ^ (n - 1) * B)

Tactic:
gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> lia

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
⊢ ↑(#(C * B ^ m)) * ↑(#(C * B ^ n)) ≤ (↑(#(C * B)) / ↑(#C)) ^ m * ↑(#C) * ((↑(#(C * B)) / ↑(#C)) ^ n * ↑(#C))

Tactic:
by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e⁻¹ • e • (x.2 * x.1) ⊆ x.1 * x.2

Tactic:
inv_smul_smul,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 * x.1 ⊆ x.1 * x.2
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ (e⁻¹ • x.1 ∪ e⁻¹ • e • x.2) = x.2 ∩ e⁻¹ • x.1

Tactic:
inv_smul_smul,

Goal state after:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ (e⁻¹ • x.1 ∪ x.2) = x.2 ∩ e⁻¹ • x.1
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:
rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]

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

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

Tactic:
constructor

Goal state after:
case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) → ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)

case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)) → ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v ↔ ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v → ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩ = d

Tactic:
ext

Goal state after:
case fst
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ (G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩).toProd.1 = d.toProd.1

case snd
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ (G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩).toProd.2 = d.toProd.2
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
rintro ⟨e, he, rfl⟩
    rfl

Goal state after:
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 : s(f x✝, f y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹

Tactic:
Sym2.eq_iff

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 : f x✝ = x✝¹ ∧ f y✝ = y✝¹ ∨ f x✝ = y✝¹ ∧ f y✝ = x✝¹
⊢ ∃ 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
G : SimpleGraph V
⊢ SimpleGraph.map id G = G

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.map id G).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
⊢ SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x✝¹ x✝ : X
⊢ (SimpleGraph.map g (SimpleGraph.map f G)).Adj x✝¹ x✝ ↔ (SimpleGraph.map (g ∘ f) G).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

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

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ : W
⊢ x✝ ∈ (SimpleGraph.map (⇑f) G).support ↔ x✝ ∈ ⇑f '' G.support
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
⊢ SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map (⇑e.toEmbedding) G

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑e.symm.toEmbedding) G).Adj x✝¹ x✝ ↔ (SimpleGraph.map (⇑e.toEmbedding) G).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
⊢ SimpleGraph.comap f (completeGraph W) = completeGraph V

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
x✝¹ x✝ : V
⊢ (SimpleGraph.comap f (completeGraph W)).Adj x✝¹ x✝ ↔ (completeGraph V).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

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

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.comap (⇑f) (SimpleGraph.map (⇑f) G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
⊢ (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)

Tactic:
ext

Goal state after:
V : Type u_1
x✝² : SimpleGraph V
x✝¹ x✝ : V
⊢ ((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
⊢ Injective f.mapEdgeSet

Tactic:
by
  rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩
  dsimp [Hom.mapEdgeSet]
  repeat rw [Subtype.mk_eq_mk]
  apply Sym2.map.injective hinj

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

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

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑f) G).Adj x✝¹ x✝ ↔ H.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ⊆ s'
⊢ (G.induceHomOfLE h).toHom = induceHom Hom.id ⋯

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ⊆ s'
x✝ : ↑s
⊢ ↑((G.induceHomOfLE h).toHom x✝) = ↑((induceHom Hom.id ⋯) x✝)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
v : V
inst✝ : Fintype ↑(⊥.neighborSet v)
⊢ ⊥.neighborFinset v = ∅

Tactic:
ext

Goal state after:
V : Type u_1
v : V
inst✝ : Fintype ↑(⊥.neighborSet v)
a✝ : V
⊢ a✝ ∈ ⊥.neighborFinset v ↔ a✝ ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
⊢ G.neighborFinset v = {w | G.Adj v w}

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ G.neighborFinset v ↔ a✝ ∈ {w | G.Adj v w}
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v ∩ s.toFinset

Tactic:
ext

Goal state after:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
a✝ : V
⊢ a✝ ∈ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) ↔ a✝ ∈ G.neighborFinset ↑v ∩ s.toFinset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).SupIndep id

Tactic:
supIndep_iff_disjoint_erase

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ ∀ i ∈ image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts),
    Disjoint (id i) (((image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase i).sup id)
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
x : α
hx : x ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
y : α
hy : y ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
hxy : x ≠ y
⊢ (Disjoint on id) x y

Tactic:
by
    simp only [coe_erase, coe_image, Set.mem_sdiff, Set.mem_image, Set.mem_singleton_iff] at hx hy
    obtain ⟨⟨px, hpx, rfl⟩, _⟩ := hx
    obtain ⟨⟨py, hpy, rfl⟩, _⟩ := hy
    simpa [Function.onFun, id_eq]
      using (P.disjoint hpx hpy fun h => hxy (h ▸ rfl)).mono inf_le_left inf_le_left

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

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

Tactic:
constructor

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

case mpr
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q ↑a_2 ⋯).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
⊢ (∃ i_1 ∈ parts, i ∈ i_1) ↔ i ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
⊢ (∃ i_1 ∈ parts, i ∈ i_1) → i ∈ s

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
⊢ i ∈ s → ∃ i_1 ∈ parts, i ∈ i_1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ P.part a = t ↔ a ∈ t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ P.part a = t → a ∈ t

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ a ∈ t → P.part a = t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ a ∈ P.part b → ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

case mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ (∃ p ∈ P.parts, a ∈ p ∧ b ∈ p) → a ∈ P.part b
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∀ (a b : ↥s),
    P.part ↑a = P.part ↑b ↔
      ((P.equivSigmaParts.trans ((Equiv.refl ↥P.parts).sigmaCongr fun t ↦ (↑t).equivFin)) a).fst =
        ((P.equivSigmaParts.trans ((Equiv.refl ↥P.parts).sigmaCongr fun t ↦ (↑t).equivFin)) b).fst
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
⊢ (image (fun a ↦ {b ∈ x | s a b}) x).SupIndep id

Tactic:
by
      simp only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise, coe_image,
        Set.mem_image, mem_coe, ne_eq, onFun, id_eq, disjoint_iff_ne, forall_mem_not_eq,
        forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_filter, not_and, filter_inj',
        not_forall, @not_imp_comm (_ ↔ _), Decidable.not_not]
      intro _ _ _ _ _ _ _ _ ha _ hb
      exact ⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t

Tactic:
rwa [← hb.2 _ ht, hau.2 _ ht]

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

Goal state before:
pp: ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
⊢ interedges r (s.biUnion f) t = s.biUnion fun a ↦ interedges r (f a) t

Tactic:
ext

Goal state after:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a✝ : α × β
⊢ a✝ ∈ interedges r (s.biUnion f) t ↔ a✝ ∈ s.biUnion fun a ↦ interedges r (f a) t
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.top
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✝ : EInt
X : C
b : ℤ
⊢ IsZero ((t.truncLT b).obj (Functor.obj 0 ((t.truncLT b).obj X))) ∧ IsZero ((t.truncLT b).obj (Functor.obj 0 X))

Tactic:
constructor

Goal state after:
case coe.top.left
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✝ : EInt
X : C
b : ℤ
⊢ IsZero ((t.truncLT b).obj (Functor.obj 0 ((t.truncLT b).obj X)))

case coe.top.right
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✝ : EInt
X : C
b : ℤ
⊢ IsZero ((t.truncLT b).obj (Functor.obj 0 X))
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a ↦ #(interedges r a t)) = fun x ↦ ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
ext

Goal state after:
case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ #(interedges r x✝ t) = ∑ y ∈ Q.parts, #(interedges r (x✝, y).1 (x✝, y).2)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ (a - 1) * m + b * (m + 1) = a * m + b * (m + 1) - m

Tactic:
rw [tsub_mul, one_mul]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ a * m - m + b * (m + 1) = a * m + b * (m + 1) - m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

pp: case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(#{b})
⊢ |↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
· replace ht : ε ≤ 0 := by simpa using ht
    exact (hε.not_ge ht).elim

Goal state after:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(#{b})
⊢ |↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε