mathlib-initiative/mathlib-tactics huggingface dataset:
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))
x : σ → K
hx : x ∉ S
⊢ ∃ i ∈ s, (eval x) (f i) ≠ 0

Tactic:
simpa using

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))
x : σ → K
hx : x ∉ S
⊢ ∃ i ∈ s, ¬(eval x) (f i) = 0
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
inst✝ : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i, (f i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), (eval x) (f i) = 0 }

Tactic:
simpa using

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
inst✝ : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i, (f i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), (eval x) (f i) = 0 }
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_1
α : 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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ x ∈ star hP G ε hU V ×ˢ star hP G ε hV U, ↑(G.edgeDensity x.1 x.2)) /
          ↑(#(star hP G ε hU V) * #(star hP G ε hV U)) -
        (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2)) / ↑((4 * 4) ^ #P.parts)|

Tactic:
simpa using

Goal state after:
case refine_1
α : 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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ x ∈ star hP G ε hU V ×ˢ star hP G ε hV U, ↑(G.edgeDensity x.1 x.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2)) / 16 ^ #P.parts|
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_nonneg : ∀ x ∈ A, 0 ≤ x
⊢ ∀ x ∈ A.subsetSum, 0 ≤ x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_nonneg : ∀ x ∈ A, 0 ≤ x
⊢ ∀ a ⊆ A, 0 ≤ ∑ b ∈ a, b
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
this : ∀ x ∈ A.subsetSum, 0 ≤ x
⊢ Disjoint (insert 0 A) (a +ᵥ A.subsetSum)

Tactic:
simpa using

Goal state after:
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
this : ∀ x ∈ A.subsetSum, 0 ≤ x
⊢ (∀ x ∈ A.subsetSum, ¬a + x = 0) ∧ ∀ a_1 ∈ A, ∀ x ∈ A.subsetSum, ¬a + x = a_1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
case refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ (∑ x_1 ∈ s.attach, if ↑x x_1 = 0 then 0 else a ↑x_1) = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ℤ
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Tactic:
simpa using

Goal state after:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ℤ
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case one
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 1 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 1 ∧ ↑1 ∣ ∑ i ∈ t, a i

Tactic:
simpa using

Goal state after:
case one
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 1 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 1
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
⊢ ↑(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) ^ 2) / 16 ^ #P.parts

Tactic:
apply (edgeDensity_chunk_aux (hP := hP) hPα hPε hU hV).trans
  have key : (16 : ℝ) ^ #P.parts = #((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts) := by
    rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]; norm_cast
  simp_rw [key]
  convert! sum_div_card_sq_le_sum_sq_div_card (α := ℝ)

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

Goal state before:
pp: a n : ℕ
ha : a ∈ n.bitIndices
⊢ n.testBit a = true

Tactic:
simpa using

Goal state after:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ n.testBit a = true
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Finset α) → (a : ↥s) → β ↑a
this : ∀ (a : α), Nonempty (β a)
g' : Finset α → (a : α) → β a := fun s a ↦ if ha : a ∈ s then g s ⟨a, ha⟩ else Classical.arbitrary (β a)
hg : ∀ (s : Finset α) (x : ↥s), g s x = g' s ↑x
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g t (Set.inclusion hst x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Finset α) → (a : ↥s) → β ↑a
this : ∀ (a : α), Nonempty (β a)
g' : Finset α → (a : α) → β a := fun s a ↦ if ha : a ∈ s then g s ⟨a, ha⟩ else Classical.arbitrary (β a)
hg : ∀ (s : Finset α) (x : ↥s), g s x = g' s ↑x
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ a ∈ s, χ a = g' t a
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl
      -- By induction hypothesis on `m`, find a subfamily `ℬ` of size `m` such that the sum over
      -- `t ∈ ℬ` of `(∑ i ∈ t, a i) / n` is divisible by `m`.
      obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
      -- We are done.
      refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
      · rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
      rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]
      · exact fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact dvd_sum fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact h𝒜disj.mono hℬ𝒜

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
h : t₀ ∈ 𝒜
⊢ n = 0

Tactic:
simpa using

Goal state after:
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
h : t₀ ∈ 𝒜
⊢ n = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t
Module: Mathlib.Combinatorics.Colex

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : toColex s ≤ toColex t
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ (s ∆ t).max' ⋯ ∈ s
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ ofColex (toColex s)

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ s
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
n : ℕ
s : Finset ι
a : ι → ZMod n
hs : 2 * n - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
n : ℕ
s : Finset ι
a : ι → ZMod n
hs : 2 * n - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * ?m.31 - 1 ≤ #s.toEnumFinset

Tactic:
simpa using

Goal state after:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * ?m.31 ≤ s.card + 1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ (Multiset.map Prod.fst t.val).card = n ∧ ↑n ∣ (Multiset.map Prod.fst t.val).sum

Tactic:
simpa using

Goal state after:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ #t = n ∧ ↑n ∣ ∑ a ∈ t, a.1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
simpa using

Goal state after:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n ≤ s.card + 1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (Multiset.map Prod.fst t.val).sum = 0

Tactic:
simpa using

Goal state after:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ #t = n ∧ ∑ a ∈ t, a.1 = 0
Module: Mathlib.Combinatorics.Colex

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

Tactic:
exact (erase_le_erase ha <| min'_mem _ _).2 <| min'_le _ _ <| ha

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

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D = D'
⊢ LinearIndepOn K id {D.rep, D'.rep}

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D = D'
⊢ ¬D'.rep = 0
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : LinearIndepOn K id (Set.range ![D'.rep, D.rep])
⊢ LinearIndepOn K id {D.rep, D'.rep}

Tactic:
simpa using

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : LinearIndepOn K id (Set.range ![D'.rep, D.rep])
⊢ LinearIndepOn K id {D.rep, D'.rep}
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : LinearIndependent K ![D'.rep, D.rep]
⊢ Function.Injective ![D'.rep, D.rep]

Tactic:
simpa using

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : LinearIndependent K ![D'.rep, D.rep]
⊢ ¬D'.rep = D.rep
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
a : Finset α
ha : a ∈ 𝒜
⊢ toColex a ∈ ⇑ofColex ⁻¹' ↑𝒜

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
a : Finset α
ha : a ∈ 𝒜
⊢ a ∈ 𝒜
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ (Perm.ofSubtype f) a = a

Tactic:
Perm.ofSubtype_apply_of_mem _ ha,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ ↑(f ⟨a, ha⟩) = a
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * ↑(#A) ≤ ↑(A.convolution A⁻¹ (a⁻¹ * b))

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * ↑(#A) ≤ ↑(A.convolution A⁻¹ (a⁻¹ * b))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
hA : ↑(#(B * A)) < K * ↑(#A)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * ↑(#A) < ↑(A.convolution A⁻¹ (a⁻¹ * b))

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
hA : ↑(#(B * A)) < K * ↑(#A)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * ↑(#A) < ↑(A.convolution A⁻¹ (a⁻¹ * b))
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) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ (x •> A ∩ y •> A).Nonempty

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ (x •> A ∩ y •> A).Nonempty
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) < 2 * #A
⊢ A * A⁻¹ ⊆ A⁻¹ * A

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ ⊆ A⁻¹ * A
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) < 2 * #A
⊢ #(A⁻¹ * A⁻¹) < 2 * #A⁻¹

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ #(A * A) < 2 * #A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y✝ : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ↑(#(A * ?m.78)) < ?m.77 * ↑(#?m.78)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y✝ : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ↑(#(A * ?m.78)) < ?m.77 * ↑(#?m.78)
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
h : (fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w

Tactic:
simpa using

Goal state after:
V : Type u_1
adj adj' : V → V → Bool
h : (fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ 2 < lineCount L p

Tactic:
simpa using

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ 1 < order P L
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l : L
⊢ 2 < pointCount P l

Tactic:
simpa using

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l : L
⊢ 1 < order P L
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ b⁻¹⁻¹ ∈ A

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ b ∈ A
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
a : G
ha : a ∈ A⁻¹ * A
⊢ ↑(#(A * ?m.103)) < ?m.102 * ↑(#?m.103)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
⊢ ↑(#(A * ?m.103)) < ?m.102 * ↑(#?m.103)