mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset

Tactic:
have h := congrArg Finset.card (map_edgeFinset_induce (s := (↑s : Set V)) (G := G))

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(map (Embedding.subtype fun x ↦ x ∈ ↑s).sym2Map (induce (↑s) G).edgeFinset) = #(G.edgeFinset ∩ (↑s).toFinset.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case inr.H
α : 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
⊢ ∃ 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

Tactic:
by_cases hab : a = 0 ∧ b = 0

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 : a = 0 ∧ b = 0
⊢ ∃ 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

case neg
α : 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 : ¬(a = 0 ∧ b = 0)
⊢ ∃ 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
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 : b ≤ a
X : C
⊢ (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) ≫ (t.eTruncLTLTIsoLT a b hab).inv.app X =
    𝟙 ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

Tactic:
by
  simpa using (t.eTruncLTLTIsoLT a b hab).hom_inv_id_app X

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

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
suffices 1 ≤ ε / 4 * #P.parts by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 1 ≤ ε / 4 * ↑(#P.parts)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ δ✝ : 𝕜
u v : Finset α
ε δ : 𝕜
a b : α
⊢ (G.Adj a b ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, a ∈ U ∧ b ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V)) →
    G.Adj b a ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, b ∈ U ∧ a ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V)

Tactic:
rintro ⟨ab, U, UP, V, VP, xU, yV, UV, GUV, εUV⟩
    refine ⟨ab.symm, V, VP, U, UP, yV, xU, UV.symm, GUV.symm, ?_⟩
    rwa [edgeDensity_comm]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  G.Adj x y →
    ∀ x_1 ∈ P.parts,
      ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
replace h' := h' h

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ (G.deleteEdges (G.incidenceSet x)).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
deleteEdges_adj,

Goal state after:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ s(v₁, v₂) ∉ G.incidenceSet x ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
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) → G.Adj v w

Tactic:
by
        rintro a b ⟨G', -, hab⟩
        exact G'.adj_sub hab

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

Goal state before:
pp: case mp
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ Set.range toSubgraph → H' ∈ {B' | Nonempty (A ≃g B'.coe)}

Tactic:
rintro ⟨f, hf, rfl⟩
    simpa [toSubgraph] using ⟨f.isoToSubgraph⟩

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

Goal state before:
pp: case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ H' ∈ Set.range toSubgraph

Tactic:
refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩

Goal state after:
case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ { toHom := H'.hom.comp e.toHom, injective' := ⋯ }.toSubgraph = H'
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : ⊥.Free G
⊢ G.killCopies ⊥ = G

Tactic:
exact killCopies_bot _

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

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G

Tactic:
exact (killCopies_eq_left hH).2 hHG

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ Subgraph.coeSubgraph H' ≤ H

Tactic:
constructor
  · simp
  · rintro v w ⟨_, _, h, rfl, rfl⟩
    exact H'.adj_sub h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑p.support + ↑p'.support.tail = {u} + ↑p.support.tail + ↑p'.support.tail

Tactic:
coe_support

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ↑p'.support.tail
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 α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) * ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) ≤
    ↑(#(G.interedges x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B)))

Tactic:
rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), le_div_iff₀, mul_assoc]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) *
      ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))) ≤
    ↑(#(G.interedges x y))

α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.drop n).getVert m = p.getVert (n + m)

Tactic:
by
  induction p generalizing n <;> cases n <;> simp [*, drop, add_right_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
⊢ w.length ≤ G.edgeFinset.card

Tactic:
classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this

Goal state after:
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 ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ (cons h q).length

Tactic:
by rw [length_cons]; lia

Goal state after:
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 ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ (cons h q).length

Tactic:
by rw [length_cons]; lia

Goal state after:
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}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ (cons h q).length

Tactic:
by rw [length_cons]; lia

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 α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B))) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), div_le_iff₀, mul_assoc]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) ≤
    ↑(#(interedges G.Adj x y)) *
      ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))))

α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
⊢ (c.takeUntil w h).IsPath

Tactic:
by
  by_cases hvw : v = w
  · subst hvw
    simp
  rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc
  exact (c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
        (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y}))))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))

Tactic:
push_cast at this

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
      (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, toTriangle x = s

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · rw [is3Clique_iff] at h
    obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h
    obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz
    refine ⟨(a, b, c), ?_, habc⟩
    obtain ⟨c', hc'⟩ := in₀₁_iff.1 hab
    obtain ⟨b', hb'⟩ := in₀₂_iff.1 hac
    obtain ⟨a', ha'⟩ := in₁₂_iff.1 hbc
    obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc' <;> assumption
  · rintro ⟨x, hx, rfl⟩
    exact toTriangle_is3Clique hx

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A)
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ ↑(#A) = ↑(#(image (Prod.map Nat.cast Nat.cast) A))

Tactic:
rw [card_image_of_injOn]
      have : Set.InjOn Nat.cast (range n) :=
        (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; lia)
      exact (this.prodMap this).mono hAn

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
by
  obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
  calc
    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
    _ = _ := by rw [← mulConst_mul_card]; ring

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

Goal state before:

Tactic:
_ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
    _ = _ := by rw [← divConst_mul_card]; ring

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: 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
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
let F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))

Goal state after:
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))
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ p ∣ #{a_1 | ↑x a_1 ≠ 0}

Tactic:
rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1).bitIndices = 0 :: map (fun x ↦ x + 1) n.bitIndices

Tactic:
← bitIndices_bit_true,

Goal state after:
n : ℕ
⊢ (2 * n + 1).bitIndices = (bit true n).bitIndices
Module: Mathlib.Data.Nat.BitIndices

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

pp: case refine_1.H
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b

Tactic:
← Pairwise.and_mem

Goal state after:
case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ List.Pairwise LT.lt L

case refine_1.H
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : toColex s ≤ toColex t
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∈ t

Tactic:
set m := (s ∆ t).max' (symmDiff_nonempty.2 hst)
    by_contra hmt
    have hms : m ∈ s := by
      simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst
    have ⟨b, hbt, hbs, hmb⟩ := h hms hmt
    exact lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <|
      mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩

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

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : L
ha : a • f v = f u
⊢ f (τ a • v) = f u

Tactic:
rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]

Goal state after: