mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ -2 ≤ -(2 / ↑n) * √(log ↑N)

pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Tactic:
neg_mul,

Goal state after:
case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ -2 ≤ -(2 / ↑n * √(log ↑N))

case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ log ↑N + -4 * √(log ↑N) ≤ 0

Tactic:
neg_mul,

Goal state after:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ log ↑N + -(4 * √(log ↑N)) ≤ 0
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
add_mul

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

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

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_2
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H : S
⊢ ↑(#{1}) ≤ 1 ∧ ↑H ^ 2 ⊆ ↑{1} • ↑H

Tactic:
by simp

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

Goal state before:
pp: α : 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
⊢ op (b⁻¹ * a) • b = a

Tactic:
by simp

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 : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ ∀ (i : Fin 3), |1 i| = 1

Tactic:
by simp

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
x : G
⊢ A.convolution B x = 0 ↔ x ∉ A * B

Tactic:
by
  simp [← convolution_ne_zero]

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 : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |Fin.cons 1 (tail (tail ε)) 0| = 1

Tactic:
by simp

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)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ 2 ≤ 3

Tactic:
by simp

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)
hA₀ : A.Nonempty
⊢ 2 ≤ 3

Tactic:
by simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ 3 ≠ 0

Tactic:
by simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) = ↑(#(List.map (fun i ↦ A ^ 1) (finRange m)).prod)

Tactic:
by simp

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ∀ (i : Fin m), |1| = 1

Tactic:
by simp

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
this : DecidableEq V
⊢ Set.MapsTo (fun d ↦ d.toProd.1) ↑univ ↑univ

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
a b : V
⊢ (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
e : V ≃ W
x✝ : SimpleGraph V
⊢ SimpleGraph.comap (⇑e) (SimpleGraph.comap (⇑e.symm) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
e : V ≃ W
x✝ : SimpleGraph W
⊢ SimpleGraph.comap (⇑e.symm) (SimpleGraph.comap (⇑e) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f✝ : G✝ →g G'
f : V → W
G : SimpleGraph W
⊢ ∀ {a b : V}, (SimpleGraph.comap f G).Adj a b → G.Adj (f a) (f b)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f : G ↪g G'
⊢ ∀ {a b : V}, (induce (Set.range ⇑f) G').Adj ((Equiv.ofInjective ⇑f ⋯) a) ((Equiv.ofInjective ⇑f ⋯) b) ↔ G.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f✝ : G✝ ↪g G'
f : V ↪ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f✝ : G✝ ↪g G'
f : V ↪ W
G : SimpleGraph V
⊢ ∀ {a b : V}, (SimpleGraph.map (⇑f) G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f✝ : G ↪g G'
α : Type u_5
β : Type u_6
f : α ↪ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : G ↪g H
⊢ ∀ {a b : V}, Hᶜ.Adj (f.toEmbedding a) (f.toEmbedding b) ↔ Gᶜ.Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
s s' : Set V
h✝ h : s ⊆ s'
⊢ ∀ {a b : ↑s}, (induce s' G).Adj ((s.embeddingOfSubset s' h) a) ((s.embeddingOfSubset s' h) b) ↔ (induce s G).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
f : G ≃g G'
v : V
w : ↑(G.neighborSet v)
⊢ (fun w ↦ ⟨f.symm ↑w, ⋯⟩) ((fun w ↦ ⟨f ↑w, ⋯⟩) w) = w

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
f : G ≃g G'
v : V
w : ↑(G'.neighborSet (f v))
⊢ (fun w ↦ ⟨f ↑w, ⋯⟩) ((fun w ↦ ⟨f.symm ↑w, ⋯⟩) w) = w

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
f✝ : G✝ ≃g G'
f : V ≃ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj (f a) (f b) ↔ (SimpleGraph.comap (⇑f) G).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f✝ : G ≃g G'
α : Type u_5
β : Type u_6
f : α ≃ β
⊢ ∀ {a b : α}, (completeGraph β).Adj (f a) (f b) ↔ (completeGraph α).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
f : G ≃g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
v : ↑s
⊢ (fun w ↦ ⟨φ.symm ↑w, ⋯⟩) ((fun v ↦ ⟨φ ↑v, ⋯⟩) v) = v

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
w : ↑t
⊢ (fun v ↦ ⟨φ ↑v, ⋯⟩) ((fun w ↦ ⟨φ.symm ↑w, ⋯⟩) w) = w

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
V₁ : Type u_5
V₂ : Type u_6
W₁ : Type u_7
W₂ : Type u_8
hV : V₁ ≃ V₂
hW : W₁ ≃ W₂
⊢ ∀ {a b : V₁ ⊕ W₁},
    (completeBipartiteGraph V₂ W₂).Adj ((hV.sumCongr hW) a) ((hV.sumCongr hW) b) ↔
      (completeBipartiteGraph V₁ W₁).Adj a b

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ v ∉ G.neighborFinset v

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
⊢ ∀ (v : V), ⊥.degree v ≤ 0

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
⊢ ⊥.maxDegree ≤ 0

Tactic:
by simp

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
z : ∑ x ∈ P.parts with #x = #s / #P.parts + 1, #x + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ ∀ x ∈ {x ∈ P.parts | #x = #s / #P.parts + 1}, #x = #s / #P.parts + 1

Tactic:
by simp

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
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts + 1) + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ ∀ x ∈ {p ∈ P.parts | #p = #s / #P.parts}, #x = #s / #P.parts

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
simp_rw [← P.sup_parts]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥
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
⊢ (t.eTruncGE.obj ⊥).map ((t.eTruncGEπ ⊥).app X) = (t.eTruncGEπ ⊥).app ((t.eTruncGE.obj ⊥).obj X)

Tactic:
simp [truncGE_map_truncGEπ_app]

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
X : C
a✝ : ℤ
⊢ (t.eTruncGE.obj (WithBotTop.coe a✝)).map ((t.eTruncGEπ (WithBotTop.coe a✝)).app X) =
    (t.eTruncGEπ (WithBotTop.coe a✝)).app ((t.eTruncGE.obj (WithBotTop.coe a✝)).obj X)

Tactic:
simp [truncGE_map_truncGEπ_app]

Goal state after:
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
⊢ (t.eTruncGE.obj ⊤).map ((t.eTruncGEπ ⊤).app X) = (t.eTruncGEπ ⊤).app ((t.eTruncGE.obj ⊤).obj X)

Tactic:
simp [truncGE_map_truncGEπ_app]

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

Goal state before:
pp: n : ℕ
⊢ 0 < 4

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
ε : ℝ
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 0 < 100

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ IsZero ((t.eTruncLT.obj ⊥).obj X)

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
⊢ 1 ≤ 4

Tactic:
by simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
h : ¬a < b
⊢ p ∈ P.parts ∨ p = b \ a

Tactic:
· left
    simpa [parts_extendOfLE_of_eq _ (LE.le.eq_of_not_lt hab h)] using hp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ IsZero ((t.eTruncGE.obj ⊤).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
h : ⊥ ≤ WithBotTop.coe (n + 1)
⊢ IsZero ((t.eTruncLT.obj ⊥).obj X)

Tactic:
by simp

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

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

Tactic:
rintro rfl
    simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
⊢ p ∈ P.part '' ↑s

Tactic:
obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
  have hx' := mem_of_subset (P.le hp) hx
  use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem.2 hx', P.mem_part hx'⟩ ⟨hp, hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : ↥s
⊢ (fun x ↦ ⟨↑x.snd, ⋯⟩) ((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) x) = x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ ⊥ ∉ Finset.map { toFun := singleton, inj' := ⋯ } s

Tactic:
by simp

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 : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
⊢ Fintype.card ↥s = Fintype.card (Fin #s)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a : EInt
X : C
h : a ≤ ⊤
⊢ IsZero ((t.eTruncGE.obj ⊤).obj ((𝟭 C).obj X))

Tactic:
by simp

Goal state after:
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
⊢ ⊥ ∉ image (fun a ↦ {b ∈ x | s a b}) x

Tactic:
suffices ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂ by simpa [filter_eq_empty_iff]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
⊢ ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 1 < 4

Tactic:
by simp

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a : EInt
X : C
h : a ≤ ⊤
⊢ IsZero ((t.eTruncGE.obj ⊤).obj ((t.eTruncGE.obj a).obj X))

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
b : EInt
X : C
h : ⊥ ≤ b
⊢ IsZero ((t.eTruncLT.obj ⊥).obj ((t.eTruncLT.obj b).obj X))

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
b : EInt
X : C
h : ⊥ ≤ b
⊢ IsZero ((t.eTruncLT.obj ⊥).obj ((𝟭 C).obj X))

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ IsZero ((t.eTruncLT.obj ⊥).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ IsZero ((t.eTruncGE.obj ⊤).obj X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ IsIso (t.eTruncGEToGEGE a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
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
hab : a ≤ b
⊢ ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ a ∈ ↑⊥.parts, #a = 1 ∨ #a = 1 + 1

Tactic:
by simp

Goal state after: