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

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 c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
⊢ t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc' =
    t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C 1)

Tactic:
by
  ext
  dsimp
  simp only [ω₁δ_app, ← Functor.map_comp, NatTrans.naturality_assoc, Functor.comp_map,
    Category.assoc, ← Functor.map_comp_assoc, NatTrans.naturality_app_assoc,
    Functor.whiskeringRight_obj_map, Functor.whiskerRight_app, NatTrans.naturality]
  congr 2
  simp only [Functor.map_comp, Category.assoc]
  have h₁ := t.eTruncLTGEIsoGELT_naturality_app a b hab a' b' hab' (homMk₁ (φ.app 0) (φ.app 1))
  rw [← reassoc_of% dsimp% h₁, ← eTruncLTGEIsoGELT_hom_naturality,
    ← eTruncLTGEIsoGELT_hom_naturality, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 2)]
  simp only [↓NatTrans.naturality_assoc, ↓← Functor.map_comp_assoc]
  simp

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (sphere x 0)

pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)

Tactic:
· rw [sphere_zero]
    exact threeAPFree_singleton _

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B * A) * #(B * C)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_invMul_invMul A B⁻¹ C

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

Goal state before:
pp: ⊢ rexp 4 < 64

Tactic:
by
  rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1,
    ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']
  · exact log_two_gt_d9.trans_le' (by norm_num1)
  · simp

Goal state after:
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)
⊢ (↑A ^ 2)⁻¹ = ↑A ^ 2

Tactic:
by simp [← inv_pow, hAsymm, ← coe_inv]

Goal state after:
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Tactic:
obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul

Goal state after:
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)
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
n : ℕ
⊢ ↑(#(B ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
by
  simpa only [_root_.pow_zero, div_one] using! pluennecke_ruzsa_inequality_pow_div_pow_div hA _ _ 0

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
⊢ v ∈ G.support.toFinsetᶜ → G.degree v = 0

Tactic:
hv

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
⊢ G.degree v = 0
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1

Tactic:
by
  simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]

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)
⊢ (G.neighborFinset v).Nonempty ↔ ¬G.IsIsolated v

Tactic:
by
  simp [nonempty_iff_ne_empty]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.minDegree

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.minDegree < Fintype.card V

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree < Fintype.card V

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
s : Set G.Subgraph
⊢ ∀ {v w : V}, (∃ G' ∈ s, G'.Adj v w) → v ∈ ⋃ G' ∈ s, G'.verts

Tactic:
rintro a b ⟨G', hG', hab⟩
        exact Set.mem_iUnion₂_of_mem hG' (G'.edge_vert hab)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G.killCopies H)

Tactic:
rw [killCopies_of_ne_bot hH, deleteEdges, Free, isContained_iff_exists_iso_subgraph]
  rintro ⟨G', hHG'⟩
  have hG' : (G'.map <| .ofLE (sdiff_le : G \ _ ≤ G)).edgeSet.Nonempty := by
    rw [Subgraph.edgeSet_map]
    exact (aux hH hHG').image _
  set e := hG'.some with he
  have : e ∈ _ := hG'.some_mem
  clear_value e
  rw [← Subgraph.image_coe_edgeSet_coe] at this
  subst he
  obtain ⟨e, he₀, he₁⟩ := this
  let e' : Sym2 G'.verts := Sym2.map (Copy.isoSubgraphMap (.ofLE _ _ _) _).symm e
  have he' : e' ∈ G'.coe.edgeSet := (Iso.map_mem_edgeSet_iff _).2 he₀
  rw [Subgraph.edgeSet_coe] at he'
  have := Subgraph.edgeSet_subset _ he'
  simp only [edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag, Set.mem_sdiff,
    Set.mem_iUnion, not_exists] at this
  refine this.2 (G'.map <| .ofLE sdiff_le) ⟨((Copy.ofLE _ _ _).isoSubgraphMap _).comp hHG'.some⟩ ?_
  rw [Sym2.map_map, Set.mem_singleton_iff, ← he₁]
  congr 1 with x
  exact congr_arg _ (Equiv.Set.image_symm_apply _ _ injective_id _ _)

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
⊢ v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
hv

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
⊢ w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk w✝ w) (r : G.Walk v✝ x), (p✝.append q).reverseAux r = q.reverseAux (p✝.reverseAux r)
q : G.Walk w✝ w
r : G.Walk u✝ x
⊢ ((cons h p✝).append q).reverseAux r = q.reverseAux ((cons h p✝).reverseAux r)

Tactic:
| cons h _ ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk v✝ w), (p✝.reverseAux q).append r = p✝.reverseAux (q.append r)
q : G.Walk u✝ w
⊢ ((cons h p✝).reverseAux q).append r = (cons h p✝).reverseAux (q.append r)

Tactic:
| cons h _ ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : n ∈ {i | i ≤ p.length}
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ p.length} → p.getVert n = p.getVert x₂ → n = x₂

Tactic:
m

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : n ∈ {i | i ≤ p.length}
m : ℕ
⊢ m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
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
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.getVert (i + 1) ∈ p.support.tail

Tactic:
← getVert_tail,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ q.length} → q.getVert n = q.getVert x₂ → n = x₂

Tactic:
m

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
m : ℕ
⊢ m ∈ {i | i ≤ q.length} → q.getVert n = q.getVert m → n = m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (Finset.map f '' G.cliqueSet 3).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton

Tactic:
(Finset.map_injective f).injOn.pairwise_image

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y ↦ (↑x ∩ ↑y).Subsingleton) (Finset.map f))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : u ∈ {w | w ∈ p.support}
v : V
⊢ v ∈ {w | w ∈ p.support} → f u = f v → u = v

Tactic:
hv

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : u ∈ {w | w ∈ p.support}
v : V
hv : v ∈ {w | w ∈ p.support}
⊢ f u = f v → u = v
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : n ∈ {i | 1 ≤ i ∧ i ≤ p.length}
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | 1 ≤ i ∧ i ≤ p.length} → p.getVert n = p.getVert x₂ → n = x₂

Tactic:
m

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : n ∈ {i | 1 ≤ i ∧ i ≤ p.length}
m : ℕ
⊢ m ∈ {i | 1 ≤ i ∧ i ≤ p.length} → p.getVert n = p.getVert m → n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ∈ {i | i ≤ p.length - 1}
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ p.length - 1} → p.getVert n = p.getVert x₂ → n = x₂

Tactic:
m

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ∈ {i | i ≤ p.length - 1}
m : ℕ
⊢ m ∈ {i | i ≤ p.length - 1} → p.getVert n = p.getVert m → n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp ≠ q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)

Goal state after:
case pos
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp ≠ q.takeUntil w hwq
this :
  p.takeUntil w hwp ≠ q.takeUntil w hwq →
    (p.takeUntil w hwp).length = (p.takeUntil w hwp).length →
      ∃ u' v' p' q',
        p'.IsSubwalk (p.takeUntil w hwp) ∧ q'.IsSubwalk (q.takeUntil w hwq) ∧ (p'.append q'.reverse).IsCycle
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2

Tactic:
· rintro rfl
    exact cliqueFree_bot le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ |↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) -
        ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))| ≤
    ε / 5

Tactic:
convert!
    abs_edgeDensity_sub_edgeDensity_le_two_mul G.Adj
      (biUnion_star_subset_nonuniformWitness hP G ε hU V)
      (biUnion_star_subset_nonuniformWitness hP G ε hV U) (by sz_positivity)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV' hUV hPε hε₁)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hU hUV'.symm (fun hVU => hUV hVU.symm)
        hPε hε₁) using 1

Goal state after:
case e'_4
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ε / 5 = 2 * (ε / 10)
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := ⋯
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ⋯
x : σ → K
hx✝ : x ∉ S
i : ι
hi : i ∈ s
hx : (eval x) (f i) ≠ 0
⊢ 1 - (eval x) (f i) ^ (q - 1) = 0

Tactic:
pow_card_sub_one_eq_one (eval x (f i)) hx,

Goal state after:
case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx✝ : x ∉ S
i : ι
hi : i ∈ s
hx : (eval x) (f i) ≠ 0
⊢ 1 - 1 = 0
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ ((fun x ↦ x + a + 1) ∘ fun x ↦ x - (a + 1)) x = x

Tactic:
simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∈ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s < toColex t ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v

Tactic:
exact ⟨a, ha⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
⊢ H ∈ Set.range Projectivization.submodule ↔ finrank K ↥((Equiv.refl (Submodule K V)) H) = 1

Tactic:
by
    refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
    rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩
    use mk K (v : V) (Subtype.coe_injective.ne hv₀)
    rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]
    refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_
    rcases hv ⟨x, hx⟩ with ⟨c, hc⟩
    exact ⟨c, congr_arg Subtype.val hc⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
· have : erase t m ⊆ erase s a := by
      rintro b hb
      rw [mem_erase] at hb ⊢
      exact ⟨(haw.trans_le <| min'_le _ _ hb.2).ne',
        (hw <| hb.1.lt_of_le' <| min'_le _ _ hb.2).2 hb.2⟩
    rw [eq_of_subset_of_card_le this]
    rw [card_erase_of_mem ha, card_erase_of_mem (min'_mem _ _)]
    exact tsub_le_tsub_right hcard _

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ toColex (s.erase a) ≤ toColex (t.erase m)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)

pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)

Tactic:
· intro x
      apply_fun fun x => Equiv.swap none (some a) x
      simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]
      rcases x with - | x
      · simp
      simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]
      by_cases x_vs_a : x = a
      · rw [x_vs_a, swap_apply_right]
        apply Option.some_ne_none
      have ne_1 : some x ≠ none := Option.some_ne_none _
      have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
      rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
      intro contra
      exact x_vs_a (h_opfp contra)

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card P ≤ Fintype.card L

Tactic:
by
  classical
  by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
  exact lt_irrefl _ this

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A * A) < 2 * #A

Tactic:
qify at h ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

pp: case neg
m : Multiset ℕ
this : ?m.115
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
· rw [← Finset.prod_erase_mul _ _ hm]
        rw [← Finset.prod_erase_mul _ _ hm]
        simp only [factorial_zero, one_pow, mul_one, zero_mul]
        exact this

Goal state after:
case neg
m : Multiset ℕ
this :
  (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
h : (fun x ↦ x + p) q = (fun x ↦ x + p) r
⊢ q = r

Tactic:
rw [DyckWord.ext_iff] at *; exact append_cancel_right h

Goal state after: