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

Goal state before:
pp: case refine_2
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ (Subgraph.comap f H').Adj v w

Tactic:
simp only [H.adj_sub hvw, comap_adj, true_and]
    exact h.2 ⟨v, w, hvw, rfl, rfl⟩

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : Fintype V
inst✝¹ : Fintype W
inst✝ : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ G.labelledCopyCount H = 1

Tactic:
convert! Fintype.card_unique

Goal state after:
case convert_2
V : Type u_1
W : Type u_2
inst✝² : Fintype V
inst✝¹ : Fintype W
inst✝ : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ Unique (H.Copy G)
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
⊢ #(B \
        {A ∈
                (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
                  else equitabilise ⋯).parts |
              A ⊆ B}.biUnion
          id) ≤
    m

Tactic:
split_ifs with h₁

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m

case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ e ∈ {s(v, w)}

Tactic:
refine e.ind ?_

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ s(x, y) ∈ {s(v, w)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Adj u v
⊢ G \ edge u v = G

Tactic:
simp [disjoint_edge, h]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : p.darts ≠ []
⊢ p.darts.head hnil = p.firstDart ⋯

Tactic:
by
  grind [firstDart_eq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj v' w
⊢ p.IsSubwalk (q.concat h)

Tactic:
by
  obtain ⟨r₁, r₂, rfl⟩ := hpq
  exact ⟨r₁, r₂.concat h, by rw [append_concat]⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges

Tactic:
rw [isSubwalk_toWalk_iff_mem_darts, isSubwalk_toWalk_iff_mem_darts, edges, List.mem_map]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts ↔
    ∃ a ∈ p.darts, a.edge = s(u', v')
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
⊢ ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x✝ ≠ y → G.Adj x✝ y

Tactic:
_

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
⊢ (∃ (x : y✝ ∈ F), ⟨y✝, ⋯⟩ ∈ A) → x✝ ≠ y✝ → G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
hx : x✝ ∈ s \ {v}
⊢ ∀ ⦃y : α⦄, y ∈ s \ {v} → x✝ ≠ y → G.Adj x✝ y

Tactic:
_

Goal state after:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
hx : x✝ ∈ s \ {v}
y✝ : α
⊢ y✝ ∈ s \ {v} → x✝ ≠ y✝ → G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝ : β
h : f w✝ = x✝
⊢ ∀ ⦃y : α⦄, y ∈ Set.range ⇑f → x✝ ≠ y → G.Adj x✝ y

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝ : β
h : f w✝ = x✝
y✝ : α
⊢ y✝ ∈ Set.range ⇑f → x✝ ≠ y✝ → G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
hle : n ≤ 1
⊢ (SimpleGraph.map (⇑f) G).CliqueFree n ↔ G.CliqueFree n

Tactic:
obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 0 ≤ 1
⊢ (SimpleGraph.map (⇑f) G).CliqueFree 0 ↔ G.CliqueFree 0

case inl.inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 1 ≤ 1
⊢ (SimpleGraph.map (⇑f) G).CliqueFree 1 ↔ G.CliqueFree 1
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {a, b, c}.sym2

Tactic:
by simpa using And.intro hg₁ hh₁

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} n ↔ 1 < n

Tactic:
obtain _ | _ | n := n

Goal state after:
case zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} 0 ↔ 1 < 0

case succ.zero
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} (0 + 1) ↔ 1 < 0 + 1

case succ.succ
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
⊢ ∃ s, G.IsMaximumClique s

Tactic:
obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
snc : G.IsNClique G.cliqueNum s
⊢ ∃ s, G.IsMaximumClique s
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)) ≤
    ↑(#(interedges G.Adj x y)) *
      ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))))

Tactic:
refine le_mul_of_one_le_right (cast_nonneg _) ?_
    rw [div_mul_eq_mul_div, one_le_div]
    · refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)
      · rw [sq, mul_mul_mul_comm, mul_comm (_ / (m : ℝ)), mul_comm (_ / (m : ℝ))]
        gcongr
        exacts [sum_card_subset_chunk_parts_le (by sz_positivity) hA hx,
          sum_card_subset_chunk_parts_le (by sz_positivity) hB hy]
      · exact_mod_cast _root_.zero_le
    rw [← cast_mul, cast_pos]
    apply mul_pos <;> rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]
    · exact ⟨_, hx, nonempty_of_mem_parts _ (hA hx)⟩
    · exact ⟨_, hy, nonempty_of_mem_parts _ (hB hy)⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ False

Tactic:
simp_rw [mem_neighborSet] at nind

Goal state after:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x, G.Adj v x ∧ ∃ y, G.Adj v y ∧ x ≠ y ∧ G.Adj x y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
⊢ ∀ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
_

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
⊢ H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
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}))
⊢ ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))

Tactic:
refine le_trans ?_ hxY

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}))
⊢ ↑(#t) * ε ≤ ↑(#t) * (↑(G.edgeDensity s t) - ε)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
calc
    _ ≤ card α / (2 * #P.parts : ℝ) := by gcongr
    _ ≤ ↑(card α / #P.parts) :=
      (div_le_iff₀' (by positivity)).2 <| mod_cast (aux ‹_› P.card_parts_le_card).le
    _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX

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

Goal state before:
pp: case ha
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⋯
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ 0 ≤ triangleRemovalBound ε

Tactic:
exact (triangleRemovalBound_pos hε).le

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
⊢ ∀ [inst : DecidableRel G'.Adj],
    G' ≤ G → G'.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)

Tactic:
_

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
inst✝ : DecidableRel G'.Adj
⊢ G' ≤ G → G'.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#(B⁻¹ * A⁻¹⁻¹)) / ↑(#A) = ↑(#(A / B)) / ↑(#A)

Tactic:
inv_inv,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#(B⁻¹ * A)) / ↑(#A) = ↑(#(A / B)) / ↑(#A)
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #({x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) = Eₘ[t, s]

Tactic:
← Finset.card_map (Equiv.prodComm _ _).toEmbedding,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #(map (Equiv.prodComm (α × α) (α × α)).toEmbedding ({x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2})) =
    Eₘ[t, s]
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
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
← CharP.cast_eq_zero_iff K,

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))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }) = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : 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:
have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu

Goal state after:
case neg
α : 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
d : α
hdu : d ∈ ofColex (toColex u)
hdt : d ∉ ofColex (toColex t)
hcd : c ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ toColex {a} ≤ toColex {b} ↔ a ≤ b

Tactic:
by
  simp [toColex_le_singleton, eq_comm]

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
D D' : ℙ K V
⊢ LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'

Tactic:
rw [LinearIndependent.pair_iff' (rep_nonzero _)]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
⊢ (∀ (a : K), a • D.rep ≠ D'.rep) ↔ D ≠ D'
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ StrictMono fun s ↦ ∑ k ∈ ofColex s, n ^ k

Tactic:
intro s t hst
  rw [Colex.lt_iff_exists_forall_lt] at hst
  obtain ⟨a, hat, has, ha⟩ := hst
  rw [← sum_sdiff_lt_sum_sdiff]
  exact (Nat.geomSum_lt hn <| by simpa).trans_le <| single_le_sum (fun _ _ ↦ by lia) <|
    mem_sdiff.2 ⟨hat, has⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
a₁✝ : Finset ℕ
⊢ ∀ ⦃a₂ : Finset ℕ⦄, (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ = (fun s ↦ ∑ i ∈ s, n ^ i) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
⊢ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ = (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n i : ℕ
h : i ≤ n
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)

Tactic:
have l₁ : (i : ℚ) + 1 ≠ 0 := by norm_cast

Goal state after:
n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
v w : ℙ K (Fin 3 → K)
⊢ v ≠ w → ℙ K (Fin 3 → K)

Tactic:
_

Goal state after:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
v w : ℙ K (Fin 3 → K)
a✝ : v ≠ w
⊢ ℙ K (Fin 3 → K)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ s = U

Tactic:
by_contra f

Goal state after:
case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
f : ¬s = U
⊢ False
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
⊢ (↑p).getLast h = D

Tactic:
by_contra f

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
⊢ False
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
⊢ c • 0 = 0

Tactic:
ext; exact smul_zero _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a ↑x

Tactic:
muFun

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (if a = b then 1
    else
      -∑ x ∈ (Ico a b).attach,
          have h := ⋯;
          have this := ⋯;
          muFun 𝕜 a ↑x) =
    if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a ↑x
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
h : ¬∑ x ∈ (Ico a b).attach, muFun 𝕜 a ↑x = 0
⊢ a ≤ b

Tactic:
obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h

Goal state after:
case neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
h : ¬∑ x ∈ (Ico a b).attach, muFun 𝕜 a ↑x = 0
x : α
hx : x ∈ Ico a b
⊢ a ≤ b
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
⊢ (p.parts.erase a).sum + a = n + 1

Tactic:
simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (cons_erase (mem_dedup.mp ha))

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
h : ¬∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b ↑x = 0
⊢ a ≤ b

Tactic:
obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h

Goal state after:
case neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
h : ¬∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b ↑x = 0
x : α
hx : x ∈ Ioc a b
⊢ a ≤ b