mathlib-initiative/mathlib-tactics huggingface dataset:
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.FarFromTriangleFree ε
h✝ : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ ↑(Fintype.card α) ^ 3

Tactic:
positivity

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.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
⊢ 0 < ε / 8

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * (↑(Fintype.card G) * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(Fintype.card G)
⊢ 0 < ↑(Fintype.card G) * ↑(Fintype.card G)

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ Fintype.card G ≠ 0

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : (triangleRemovalBound (ε / 9) * 27)⁻¹ < ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ 0 < triangleRemovalBound (ε / 9) * 27

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ 0 < ↑(Fintype.card G) ^ 2

Tactic:
positivity

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

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * (ε * ↑(Fintype.card α ^ 2))
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
replace k := lt_of_mul_lt_mul_left k zero_le_two

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : ↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) < ε * ↑(Fintype.card α ^ 2)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
P : Finpartition univ
ε✝ ε : ℝ
hε : 0 < ε
⊢ 0 < triangleRemovalBound ε

Tactic:
positivity

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)
⊢ 0 < ε / 9

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ ↑(#A) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A)

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ #(univ ×ˢ A) = #B

Tactic:
exact card_equiv ((Equiv.refl _).prodShear fun a ↦ Equiv.addLeft a) (by simp [B])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂]

Tactic:
by
  unfold mulEnergy; gcongr

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
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
positivity

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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ 4 / 5 * ε

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
positivity

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

Goal state before:
pp: case h₂.refine_1.ha
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ ↑(#(star hP G ε hU V))

Tactic:
positivity

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

Goal state before:
pp: case hb
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ 4 ^ #P.parts

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ 0 < ε / 3

Tactic:
positivity

Goal state after:
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:
rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]

Goal state after:
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 := ⋯ }
⊢ ↑(e a) (e' (Sum.inl default)) ^ d (e' (Sum.inl default)) * ∏ a₂, ↑(e a) (e' (Sum.inr a₂)) ^ d (e' (Sum.inr a₂)) =
    ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j
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 σ
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
  let S : Finset (σ → K) := {x | ∀ i ∈ s, eval x (f i) = 0}
  have hS (x : σ → K) : x ∈ S ↔ ∀ i ∈ s, eval x (f i) = 0 := by simp [S]
  /- The polynomial `F = ∏ i ∈ s, (1 - (f i)^(q - 1))` has the nice property
    that it takes the value `1` on elements of `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}`
    while it is `0` outside that locus.
    Hence the sum of its values is equal to the cardinality of
    `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}` modulo `p`. -/
  let F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
  have hF : ∀ x, eval x F = if x ∈ S then 1 else 0 := by
    intro x
    calc
      eval x F = ∏ i ∈ s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
      _ = if x ∈ S then 1 else 0 := ?_
    simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
    split_ifs with hx
    · apply Finset.prod_eq_one
      intro i hi
      rw [hS] at hx
      rw [hx i hi, zero_pow hq.ne', sub_zero]
    · obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by
        simpa [hS, not_forall, Classical.not_imp] using hx
      apply Finset.prod_eq_zero hi
      rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
  -- In particular, we can now show:
  have key : ∑ x, eval x F = Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 } := by
    rw [Fintype.card_of_subtype S hS, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one, ←
      Fintype.sum_extend_by_zero S, sum_congr rfl fun x _ => hF x]
  -- With these preparations under our belt, we will approach the main goal.
  change p ∣ Fintype.card { x // ∀ i : ι, i ∈ s → eval x (f i) = 0 }
  rw [← CharP.cast_eq_zero_iff K, ← key]
  change (∑ x, eval x F) = 0
  -- We are now ready to apply the main machine, proven before.
  apply F.sum_eval_eq_zero
  -- It remains to verify the crucial assumption of this machine
  show F.totalDegree < (q - 1) * Fintype.card σ
  calc
    F.totalDegree ≤ ∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree := totalDegree_finsetProd s _
    _ ≤ ∑ i ∈ s, (q - 1) * (f i).totalDegree := sum_le_sum fun i _ => ?_
    -- see ↓
    _ = (q - 1) * ∑ i ∈ s, (f i).totalDegree := (mul_sum ..).symm
    _ < (q - 1) * Fintype.card σ := by gcongr
  -- Now we prove the remaining step from the preceding calculation
  change (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
  calc
    (1 - f i ^ (q - 1)).totalDegree ≤
        max (1 : MvPolynomial σ K).totalDegree (f i ^ (q - 1)).totalDegree := totalDegree_sub _ _
    _ ≤ (f i ^ (q - 1)).totalDegree := by simp
    _ ≤ (q - 1) * (f i).totalDegree := totalDegree_pow _ _

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ⇑↑f } ≃ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f }

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∉ fixedPoints ⇑↑f } ≃ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f }

Tactic:
· exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∈ fixedPoints ·)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∉ fixedPoints ⇑↑f } ≃ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f }
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a * x ∈ ↑A

Tactic:
· norm_cast
      rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } := fun q ↦ ⟨mkLine ⋯, ⋯⟩
hf : Function.Injective f
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key'✝ : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } := fun q ↦ ⟨mkLine ⋯, ⋯⟩
hf : Function.Injective f
key' : Function.Surjective f
⊢ ∃ p ∈ l₁, p ∈ l₂
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ ∏ i ∈ m.toFinset, (i * count i m)! ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h = U

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✝ } ≠ []
⊢ (↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head
      h =
    U

Tactic:
· tauto

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✝ } ≠ []
⊢ (↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head
      h =
    U
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False

Tactic:
dropLast_eq_take,

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

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

Tactic:
· tauto

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

Goal state before:
pp: m : Multiset ℕ
⊢ 0 < ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
positivity

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)
⊢ 0 < K

Tactic:
positivity

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 : 0 < K
⊢ 0 < K

Tactic:
positivity

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
⊢ 0 < K * (2 - K) / ((φ - K) * (K - ψ))

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : ↑(#(∅⁻¹ * ∅)) ≤ K * ↑(#∅)
hA₂ : ↑(#(∅ * ∅⁻¹)) ≤ K * ↑(#∅)
⊢ 0 ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
positivity

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

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
⊢ 0 < a !

Tactic:
positivity

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

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
⊢ 0 < rest

Tactic:
positivity

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

Goal state before:
pp: case cons.cons
q : DyckWord
i : ℕ
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ :
  ∀ (i : ℕ), count D (List.take i (s :: head✝ :: tail✝)) ≤ count U (List.take i (s :: head✝ :: tail✝))
hn :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
l1 :
  List.take 1
      ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
          count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h]
⊢ (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).length -
      1 =
    (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
                count_D_le_count_U := count_D_le_count_U✝ }).length -
          1 -
        1 +
      1

Tactic:
· tauto

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

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (1 + i) (↑p).dropLast)) ≤ count U (List.drop 1 (List.take (1 + i) (↑p).dropLast))

Tactic:
dropLast_eq_take,

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (1 + i) (List.take ((↑p).length - 1) ↑p))) ≤
    count U (List.drop 1 (List.take (1 + i) (List.take ((↑p).length - 1) ↑p)))
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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
⊢ ↑(#S) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
simp [hn]

Goal state after: