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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
replace hA := calc (#(A ^ 4 * A) : ℝ)
      _ = #(A ^ 5) := by rw [← pow_succ]
      _ ≤ K ^ 3 * #A := small_pow_of_small_tripling (by lia) hA hAsymm
    have hA₀ : A.Nonempty := ⟨1, hA₁⟩
    obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA
    exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩

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

Goal state before:
pp: case 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
⊢ (t.eTruncLT.obj ⊥).Additive

Tactic:
dsimp

Goal state after:
case 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
⊢ Functor.Additive 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
a✝ : ℤ
⊢ (t.eTruncLT.obj (WithBotTop.coe a✝)).Additive

Tactic:
dsimp

Goal state after:
case coe
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
a✝ : ℤ
⊢ (t.truncLT a✝).Additive
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
⊢ (t.eTruncLT.obj ⊤).Additive

Tactic:
dsimp

Goal state after:
case 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
⊢ (𝟭 C).Additive
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(mulDysonETransform e x).1 + #(mulDysonETransform e x).2 = #x.1 + #x.2

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonETransform e (mulDysonETransform e x)).1 = (mulDysonETransform e x).1

Tactic:
dsimp

Goal state after:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2
Module: Mathlib.Combinatorics.Additive.ETransform

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

Tactic:
dsimp

Goal state after:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1
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 : ℕ
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
have hA' : A ∈ A.powerset.erase ∅ := mem_erase_of_ne_of_mem hA.ne_empty (mem_powerset_self _)
  obtain ⟨C, hC, hCmin⟩ :=
    exists_min_image (A.powerset.erase ∅) (fun C ↦ #(C * B) / #C : _ → ℚ≥0) ⟨A, hA'⟩
  rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC
  obtain ⟨hC, hCA⟩ := hC
  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #C)
  calc
    (#(B ^ m / B ^ n) * #C : ℚ≥0)
      ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
    _ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
    _ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
    _ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
    _ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'

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

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

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

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

Tactic:
rw [← card_smul_finset g⁻¹ t]
    right
    grw [hst, ← card_union_of_disjoint hgt]
    exact (card_le_card_mul_left hgs).trans (le_add_of_le_left aux1)

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

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

Tactic:
obtain rfl | hA₀ := A.eq_empty_or_nonempty
  · simp
  have : 0 ≤ K := nonneg_of_mul_nonneg_left (hA.trans' <| by positivity) (by positivity)
  refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
  calc
    (#A * #(A⁻¹ * A * A) : ℝ) = #A * #(A⁻¹ * (A * A)) := by rw [mul_assoc]
    _ ≤ #(A * A) * #(A * (A * A)) := by
      norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)
    _ = #(A ^ 2) * #(A ^ 3) := by simp [pow_succ']
    _ ≤ (K * #A) * (K * #A) := by
      gcongr
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA
    _ = #A * (K ^ 2 * #A) := by ring

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

Goal state before:
pp: V : Type u_1
s : Set V
⊢ induce s ⊥ = ⊥

Tactic:
dsimp

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ G.support
⊢ v ∈ s

Tactic:
rw [← h, support_spanningCoe] at hv
    have ⟨u, _, hvu⟩ := hv
    exact hvu ▸ u.prop

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe.Adj u v

Tactic:
· exact ⟨hadj.ne, ⟨u, h hadj.left_mem_support⟩, ⟨v, h hadj.right_mem_support⟩, hadj, rfl, rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ∈ {w | w ≠ v ∧ Odd (G.degree w)}
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
rw [mem_filter_univ] at hw

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ f x ≤ f y + 1

Tactic:
(hb x hx).2,

Goal state after:
α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ b + 1 ≤ f y + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i ∈ s, f i) / #s ≤ b + 1 ∧ b + 1 ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
sum_const_nat h,

Goal state after:
case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ #s * (b + 1) / #s ≤ b + 1 ∧ b + 1 ≤ #s * (b + 1) / #s + 1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ R.parts, b ≤ c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
⊢ b ∈ Q.parts

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ b ∈ Q.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
⊢ P = Q

Tactic:
by
      ext b
      refine ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩
      · obtain ⟨c, hc, hbc⟩ := hPQ hb
        obtain ⟨d, hd, hcd⟩ := hQP hc
        rwa [hbc.antisymm]
        rwa [P.disjoint.eq_of_le hb hd (P.ne_bot hb) (hbc.trans hcd)]
      · obtain ⟨c, hc, hbc⟩ := hQP hb
        obtain ⟨d, hd, hcd⟩ := hPQ hc
        rwa [hbc.antisymm]
        rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]

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
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let es := {p ∈ P.parts | #p = #s / #P.parts}.equivFin

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
⊢ (t.eTruncGE.obj ⊥).Additive

Tactic:
dsimp

Goal state after:
case 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
⊢ (𝟭 C).Additive
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
a✝ : ℤ
⊢ (t.eTruncGE.obj (WithBotTop.coe a✝)).Additive

Tactic:
dsimp

Goal state after:
case coe
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
a✝ : ℤ
⊢ (t.truncGE a✝).Additive
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
⊢ (t.eTruncGE.obj ⊤).Additive

Tactic:
dsimp

Goal state after:
case 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
⊢ Functor.Additive 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c
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
this : (P.parts.sup fun x ↦ x) = a
⊢ a ⊓ b = b

Tactic:
inf_eq_right.mpr hb

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
this : (P.parts.sup fun x ↦ x) = a
⊢ b = b
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂

Tactic:
dsimp

Goal state after:
case 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
X : C
⊢ IsIso (𝟙 X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁

Tactic:
dsimp

Goal state after:
case 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
X : C
⊢ IsIso (𝟙 X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
a✝ : ℤ
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
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
a✝ : ℤ
⊢ t.IsLE ((t.truncLT a✝).obj X) n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
dsimp

Goal state after:
case 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
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
dsimp

Goal state after:
case 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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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.IsGE X n
a✝ : ℤ
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
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.IsGE X n
a✝ : ℤ
⊢ t.IsGE ((t.truncGE a✝).obj X) n
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) * m + a * (m + 1) = #u

Tactic:
rw [hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), mul_comm]

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

Goal state before:
pp: case coe
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
n : ℤ
X : C
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
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
n : ℤ
X : C
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
⊢ t.IsGE ((t.truncGE i).obj X) n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
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
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ t.IsLE ((t.truncLT i).obj X) n
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ (ofSetoid s).part a ↔ s a b

Tactic:
suffices b ∈ (ofSetSetoid s univ).part a ↔ a ∈ univ ∧ b ∈ univ ∧ s a b by simpa

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ (ofSetSetoid s univ).part a ↔ a ∈ univ ∧ b ∈ univ ∧ s a b
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
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊤
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι ⊤).app X))

Tactic:
dsimp

Goal state after:
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
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊤
⊢ IsIso ((t.truncLT a).map (𝟙 X))
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
X : C
n : ℤ
inst✝ : t.IsGE X n
a✝ : ℤ
⊢ t.IsGE ((t.eTruncLT.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp

Goal state after:
case coe
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
X : C
n : ℤ
inst✝ : t.IsGE X n
a✝ : ℤ
⊢ t.IsGE ((t.truncLT a✝).obj X) n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
dsimp

Goal state after:
case 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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case 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
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
dsimp

Goal state after:
case 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
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE X n