mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : s(d.toProd.1, d.toProd.2) = s(u', v')
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
Sym2.eq,

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'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : Sym2.Rel V (d.toProd.1, d.toProd.2) (u', v')
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
rw! [concat_cons, dropLast_cons_of_not_nil]

Goal state after:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

case hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
simp [isClique_map_iff_of_nontrivial ht, ht.not_subsingleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
⊢ (SimpleGraph.map (⇑f) G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
by
  obtain (ht | ht) := t.subsingleton_or_nontrivial
  · simp [IsClique.of_subsingleton, ht]
  simp [isClique_map_iff_of_nontrivial ht, ht.not_subsingleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ (SimpleGraph.map (⇑f) G).LocallyLinear

Tactic:
refine ⟨hG.1.map _, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ ∀ ⦃x y : β⦄, (SimpleGraph.map (⇑f) G).Adj x y → ∃ s, (SimpleGraph.map (⇑f) G).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : s(u, w) = s(u, p.snd) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd

Tactic:
Sym2.eq,

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : Sym2.Rel V (u, w) (u, p.snd) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

pp: case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ (G ⊔ edge v w).Adj x y

Tactic:
· obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
    · exact hv.mono le_sup_left hx hy hxy
    · exact hw.mono le_sup_left hx hy hxy

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ (G ⊔ edge v w).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (⇑f.toEmbedding '' Set.univ) ∧ Fintype.card β = Fintype.card β

Tactic:
Set.image_univ

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f.toEmbedding) ∧ Fintype.card β = Fintype.card β
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : t ∉ Set.range ⇑φ
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
simp_rw [Set.mem_range, not_exists, ← ne_eq] at mt

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : (induce s G).IsNClique (induce s G).cliqueNum t'
⊢ (induce s G).cliqueNum ≤ G.cliqueNum

Tactic:
rw [isNClique_induce_iff] at tc

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : G.IsNClique (induce s G).cliqueNum (map (Embedding.subtype fun x ↦ x ∈ s) t')
⊢ (induce s G).cliqueNum ≤ G.cliqueNum
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k + n < k * (n / k) + n

Tactic:
add_lt_add_iff_right

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k < k * (n / k)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : 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ε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
⊢ ↑(G.edgeDensity U V) ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 ≤
    ↑(G.edgeDensity U V) ^ 2 - ↑(G.edgeDensity U V) * ε ^ 5 / 25 + ε ^ 10 / 2500

Tactic:
gcongr; exact mod_cast G.edgeDensity_le_one ..

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

Goal state before:
pp: α : 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
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2

Tactic:
by
  obtain hGε | hGε := le_total (G.edgeDensity U V : ℝ) (ε ^ 5 / 50)
  · refine (sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)
    · exact mod_cast G.edgeDensity_nonneg _ _
    · exact mod_cast G.edgeDensity_le_one _ _
    · exact div_le_div_of_nonneg_left (by sz_positivity) (by simp) (by norm_num)
  rw [← sub_nonneg] at hGε
  have : 0 ≤ ε := by sz_positivity
  calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * ((↑m + 1) * ((1 - (↑m)⁻¹) / ↑m) / 4 ^ #P.parts) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
← mul_comm_div

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * ((↑m + 1) * ((1 - (↑m)⁻¹) / ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ b = y)

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
z : γ
hxyz : (a, b, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (a, b, z)
this : a = a → b = b → ¬c = z
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ c = z)

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
y : β
hxyz : (a, y, c) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (a, y, c)
this : a = a → b = y → ¬c = c
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(b = y ∧ c = z)

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
hxyz : (x, b, c) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, b, c)
this : a = x → b = b → ¬c = c
⊢ False
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
card_inv,

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

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

Tactic:
card_inv,

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ∏ j, ↑(e a) j ^ d j = ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
by
      rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl

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

Goal state before:
pp: case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : ↥s
a✝ : i ∈ univ
⊢ (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1

Tactic:
exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le

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

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree + (f₂ s a).totalDegree < 2 * p - 1

Tactic:
by
  calc
    _ ≤ (p - 1) + (p - 1) := by
      gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
      · exact (totalDegree_X_pow ..).le
      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le
    _ < 2 * p - 1 := by have := (Fact.out : p.Prime).two_le; lia

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ (∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) = 0 ∨ ∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ ≠ 0

Tactic:
sub_ne_zero,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ (∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) = 0 ∨ ∑ ψ ∈ u, ψ ≠ ∑ ψ ∈ t \ u, ψ
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A ∪ (a +ᵥ A.subsetSum))

Tactic:
rw [card_union_of_disjoint disjoint]

Goal state after:
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
a : α
has : a ∈ s
hat : a ∉ t
⊢ False

Tactic:
have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : toColex s ≤ toColex t
hts : toColex t ≤ toColex s
a : α
has : a ∈ s
hat : a ∉ t
_b : α
hb₁ : _b ∈ s
hb₂ : _b ∉ s
right✝ : a ≤ _b
⊢ False
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:
refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
⊢ toColex (s.erase a) ≤ toColex (t.erase (t.min' ht))

Tactic:
set m := min' t ht

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
⊢ toColex (s.erase a) ≤ toColex (t.erase m)
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ (Set.range fun x ↦ x • ↑v) = ↑H

Tactic:
refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
x : V
hx : x ∈ ↑H
⊢ x ∈ Set.range fun x ↦ x • ↑v
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case h.h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : w ≠ 0
⊢ (mk F v hv).orthogonal (mk F w hw) ↔ (mk F w hw).orthogonal (mk F v hv)

Tactic:
| h w hw =>

Goal state after:
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
⊢ (mk F v hv).cross (mk F w hw) = (mk F w hw).cross (mk F v hv)

Tactic:
| h w hw =>

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

Goal state before:
pp: case 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
⊢ ((mk F v hv).cross (mk F w hw)).orthogonal (mk F v hv)

Tactic:
| h w hw =>

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ ∑ p, lineCount L p = ∑ l, pointCount P l

Tactic:
classical
    simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
    apply Fintype.card_congr
    calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l

Goal state after:
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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2

Tactic:
← Finset.univ_product_univ,

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ i ∈ univ ×ˢ univ, lineCount L i.1 = ∑ i ∈ univ ×ˢ univ, pointCount P i.2
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.Nonempty

Tactic:
by
  by_contra! rfl
  simp at h

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

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + if U = D then 1 else 0
⊢ False

Tactic:
reduceCtorEq,

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + if False then 1 else 0
⊢ False
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take j (↑p ++ [D])) + 1 = count D (List.take j (↑p ++ [D])) + if U = D then 1 else 0) = false

Tactic:
reduceCtorEq,

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take j (↑p ++ [D])) + 1 = count D (List.take j (↑p ++ [D])) + if False then 1 else 0) = false
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.insidePart = p

Tactic:
simp_rw [insidePart, nest_ne_zero, dite_false, firstReturn_nest]
  convert! p.denest_nest; rw [DyckWord.ext_iff]; apply take_of_length_le
  simp_rw [nest, length_append, length_singleton]; lia

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
this : ∀ (i : ℕ), g i ≠ 0 → i ≠ 0
⊢ ∀ {i : ℕ}, i ∈ Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ } → 0 < i

Tactic:
by simpa [Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)

Tactic:
exact Int.two_mul_ediv_two_of_even (by grind)

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (n + 1).smallSchroder = 3 * n.smallSchroder + 2 * ∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder

Tactic:
by
  obtain _ | _ | n := n
  · simp at hn
  · simp at hn
  refine Nat.mul_left_cancel zero_lt_two ?_
  calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;>
      · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
        we need to re-enable model-based theory combination in `lia` for this to go through. -/
        lia +mbtc
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia

Goal state after: