mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
sub_mul,

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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    1 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath

Tactic:
rw [isPath_def, ← cons_tail_support, List.nodup_cons]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).penultimate = v

Tactic:
simp [concat_eq_append, getVert_append]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : ↑s ⊆ t
⊢ t ⊆ ↑s

Tactic:
by_contra hc
      have fint := ofFinite t
      have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]
      have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
      have hlt : #s < #t.toFinset :=
        card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
      exact lt_irrefl _ (lt_of_lt_of_le hlt hle)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) ≤ ↑(#(G.badVertices ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_le).trans ?_

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(∑ a ∈ G.badVertices ε s t, #(map { toFun := fun x ↦ (a, x), inj' := ⋯ } ({y ∈ t | G.Adj a y}))) ≤
    ↑(#(G.badVertices ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)
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 α
x : α
hx : x ∈ s
y z : α
hy : y ∈ t
xy : G.Adj x y
hz : z ∈ u
xz : G.Adj x z
yz : G.Adj y z
⊢ x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Tactic:
exact ⟨hx, hy, hz, xy, xz, yz⟩

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

Goal state before:
pp: case inl.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ↑(G.edgeDensity U V) ≤ 1

pp: case inl.refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ε ^ 5 / 50 ≤ ε ^ 5 / 25

Tactic:
· exact mod_cast G.edgeDensity_le_one _ _

Goal state after:
case inl.refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ε ^ 5 / 50 ≤ ε ^ 5 / 25
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:
by
  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
  linarith

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 α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ (1 - 2 * ε) * ↑(#s) ≤ ↑(#X')

Tactic:
sub_mul,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ 1 * ↑(#s) - 2 * ε * ↑(#s) ≤ ↑(#X')
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
⊢ a ∈ s'.mulSpan

Tactic:
have : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b := by
      rw [prod_erase_eq_div hat, htu.2.2, div_div_self']

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ a ∈ s'.mulSpan
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * ↑σₘ[A, B] = ↑(#(A * B))

Tactic:
norm_cast; exact card_mul_mulConst _ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 = (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2

Tactic:
← sum_card_fiberwise_eq_card_filter

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ j ∈ u, #({i ∈ s ×ˢ t | i.1 * i.2 = j})) ^ 2 = (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : toColex s ≤ toColex t
hts : toColex t ≤ toColex s
⊢ s ⊆ t

Tactic:
by
  intro a has
  by_contra hat
  have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat
  exact hb₂ hb₁

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ 0 = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
⊢ s ≤ t ∧ s ≠ t ↔ ∃ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t

Tactic:
le_iff_max'_mem

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
⊢ (∀ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t) ∧ s ≠ t ↔
    ∃ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![![w 0, w 1, w 2] 0 • v 0, ![w 0, w 1, w 2] 0 • v 1, ![w 0, w 1, w 2] 0 • v 2] = ![v 0 • w 0, v 0 • w 1, v 0 • w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ v 0 = 0
h21 :
  ![![w 0, w 1, w 2] 1 • v 0, ![w 0, w 1, w 2] 1 • v 1, ![w 0, w 1, w 2] 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ v 1 = 0
h22 :
  ![![w 0, w 1, w 2] 2 • v 0, ![w 0, w 1, w 2] 2 • v 1, ![w 0, w 1, w 2] 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
← hw'

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : ![w 0 • v 0, w 0 • v 1, w 0 • v 2] = ![v 0 • w 0, v 0 • w 1, v 0 • w 2] → -w 0 = 0 ∧ v 0 = 0
h21 : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
h22 : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝ • (w✝¹ • ↑x✝³ ⬝ᵥ ↑x✝²) = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
smul_dotProduct,

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝ • w✝¹ • (↑x✝³ ⬝ᵥ ↑x✝²) = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : b • (a • crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨b • (a • crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
LinearMap.smul_apply,

Goal state after:
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : b • a • (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨b • a • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ 0 = 0
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)

Tactic:
exact card_derangements_fin_eq_numDerangements

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ A * Bᵀ = 0

Tactic:
ext i j

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
i j : Fin 2
⊢ (A * Bᵀ) i j = 0 i j
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹

Tactic:
exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩

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

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

Tactic:
by
  rcases p with - | s; · tauto
  rw [head_cons]
  by_contra f
  rename_i _ nonneg
  simpa [s.dichotomy.resolve_left f] using nonneg 1

Goal state after:
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
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ -0 = 0

Tactic:
neg_zero

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ (n + 1) * p.parts.bell = (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell

Tactic:
mul_eq_mul_right_iff

Goal state after:
n : ℕ
p : (n + 1).Partition
⊢ n + 1 = ∑ a ∈ p.parts.toFinset, count a p.parts * a ∨ p.parts.bell = 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)

Tactic:
calc
            (#A : ℝ) * #A
        _ = #A * #A⁻¹ := by simp
        _ = #(A ×ˢ A⁻¹) := by simp
        _ = ∑ z ∈ S, ↑(r z) := by
          norm_cast
          exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2
        _ = ∑ z ∈ S with (K - 1) * #A < r z, ↑(r z) + ∑ z ∈ S with r z ≤ (K - 1) * #A, ↑(r z) := by
          norm_cast; simp_rw [← not_lt, sum_filter_add_sum_filter_not]
        _ ≤ ∑ z ∈ S with (K - 1) * #A < r z, ↑(#A)
          + ∑ z ∈ S with r z ≤ (K - 1) * #A, (K - 1) * #A := by
          gcongr with z hz z hz
          · exact convolution_le_card_left
          · simp_all
        _ = l * #A + (#S - l) * (K - 1) * #A := by
          simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]
        _ = ((2 - K) * l + (K - 1) * #S) * #A := by ring

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

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 + 1 < p.firstReturn + 1
⊢ count D (List.take (i - 1 + 1) ↑p) < count U (List.take (i - 1 + 1) ↑p)

Tactic:
Nat.add_lt_add_iff_right

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 < p.firstReturn
⊢ count D (List.take (i - 1 + 1) ↑p) < count U (List.take (i - 1 + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z = ∑ y ≥ x, ∑ z ≥ y, 1 x z * f z

Tactic:
simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
hrz : (K - 1) * ↑(#A) < ↑(r z)
w : G
hw : w ∈ S
⊢ (2 - K) * ↑(#A) ≤ ↑(r w)

Tactic:
simpa [card_mul_inv_eq_convolution_inv] using! le_card_mul_inv_eq hA₁ (by simpa)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), X ^ ((b + 1) * j)) * (1 - X ^ (b + 1))) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
pow_mul

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))) =
    ∏' (i : ℕ), (1 - (X ^ (i + 1)) ^ m)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun n ↦ aux k n x - aux k 0 x) atTop (𝓝 (0 - aux k 0 x))

Tactic:
apply Tendsto.sub_const

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ aux k x_1 x) atTop (𝓝 0)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)

Tactic:
sub_mul,

Goal state after:
case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ 1 * ↑(#((↑H).toFinset * S)) - K * ↑(#((↑H).toFinset * S)) ≤ (1 - ε / 2) * ↑(#(↑H).toFinset)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ K * ↑(#(↑H).toFinset) + ex (↑H).toFinset ≤ K * ↑(#(↑H).toFinset) + (1 - ε / 2) * ↑(#((↑H).toFinset * S))

Tactic:
grw [calc₁]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ K * ↑(#(↑H).toFinset) + (1 - ε / 2) * ↑(#S) ≤ K * ↑(#(↑H).toFinset) + (1 - ε / 2) * ↑(#((↑H).toFinset * S))