mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ #A + #A.subsetSum < #(insert a A).subsetSum

Tactic:
calc #A + #A.subsetSum
    _ < #A + 1 + #A.subsetSum := by gcongr; exact Nat.lt_add_one _
    _ = #(insert 0 A) + #A.subsetSum := by rw [card_insert_of_notMem fun h => (hA 0 h).false]
    _ = #(insert 0 A) + #(a +ᵥ A.subsetSum) := by simp [vadd_finset_def, card_image_of_injOn]
    _ = #((insert 0 A) ∪ (a +ᵥ A.subsetSum)) := by rw [card_union_of_disjoint disjoint]
    _ ≤ #(insert a A).subsetSum := by grw [union_subset insert_subset vadd_subset]

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
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ 16 ^ #P.parts = ↑((4 * 4) ^ #P.parts)

Tactic:
;

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
⊢ 16 ^ #P.parts = ↑((4 * 4) ^ #P.parts)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: k : ℕ
⊢ map (fun x ↦ x + k) (bitIndices 1) = [k]

Tactic:
;

Goal state after:
k : ℕ
⊢ map (fun x ↦ x + k) (bitIndices 1) = [k]
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: b : Bool
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
i : ℕ
⊢ ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) i = 2 * 2 ^ i

Tactic:
;

Goal state after:
b : Bool
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
i : ℕ
⊢ ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) i = 2 * 2 ^ i
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ x - (a + 1) + (a + 1) = x

Tactic:
;

Goal state after:
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ x - (a + 1) + (a + 1) = x
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) x = 2 ^ a * (2 * 2 ^ x)

Tactic:
;

Goal state after:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) x = 2 ^ a * (2 * 2 ^ x)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ 2 ^ x * 2 ^ a * 2 = 2 ^ a * (2 * 2 ^ x)

Tactic:
;

Goal state after:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ 2 ^ x * 2 ^ a * 2 = 2 ^ a * (2 * 2 ^ x)
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case h₁
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
⊢ 2 ≤ 2 * m - k

Tactic:
;

Goal state after:
case h₁
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
⊢ 2 ≤ 2 * m - k
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case hcd
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
⊢ #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t

Tactic:
;

Goal state after:
case hcd
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
⊢ #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)

Tactic:
simp_rw [cross_apply, vec3_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0] =
    ![![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 +
        (v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 -
          v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1),
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 +
        (v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 -
          v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2),
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 +
        (v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 -
          v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)]
Module: Mathlib.Combinatorics.Colex

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

Tactic:
;

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

Goal state before:
pp: α : 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

Tactic:
;

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.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
α : Type u_3
f : { v // v ≠ 0 } → α
hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b
x : ℙ K V
w : V
hw : w ≠ 0
t inv✝ : K
val_inv✝ : t * inv✝ = 1
inv_val✝ : inv✝ * t = 1
hv : (fun m ↦ m • ↑⟨w, hw⟩) { val := t, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ≠ 0
⊢ f ⟨(fun m ↦ m • ↑⟨w, hw⟩) { val := t, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, hv⟩ = f ⟨w, hw⟩

Tactic:
;

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
α : Type u_3
f : { v // v ≠ 0 } → α
hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b
x : ℙ K V
w : V
hw : w ≠ 0
t inv✝ : K
val_inv✝ : t * inv✝ = 1
inv_val✝ : inv✝ * t = 1
hv : (fun m ↦ m • ↑⟨w, hw⟩) { val := t, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ≠ 0
⊢ f ⟨(fun m ↦ m • ↑⟨w, hw⟩) { val := t, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, hv⟩ = f ⟨w, hw⟩
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
⊢ IsInitSeg (initSeg s) #s

Tactic:
refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
b : α
⊢ f b ≠ b ↔ (e.permCongr f) (e b) ≠ e b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
b : α
⊢ f b ≠ b ↔ (e.permCongr f) (e b) ≠ e b
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A

Tactic:
have smul_A {a} (ha : a ∈ A) : a •> A = A * A :=
    eq_of_subset_of_card_le (smul_finset_subset_mul ha) (by simpa)

Goal state after:
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 •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A
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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)

Tactic:
;

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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
this : 2 * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A)) + ↑(#(B * A))
⊢ (2 - K) * ↑(#A) ≤ ↑(#(a •> A ∩ b •> 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
a b : G
hA : ↑(#(B * A)) < K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
this : 2 * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A)) + ↑(#(B * A))
⊢ (2 - K) * ↑(#A) < ↑(#(a •> A ∩ b •> A))

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) < K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
this : 2 * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A)) + ↑(#(B * A))
⊢ (2 - K) * ↑(#A) < ↑(#(a •> A ∩ b •> A))
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
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
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2} ↔ p.1 ∈ {p_1 | p_1 ∈ p.2}

Tactic:
;

Goal state after:
case h
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
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2} ↔ p.1 ∈ {p_1 | p_1 ∈ p.2}
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
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
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2} ↔ p.2 ∈ {l | p.1 ∈ l}

Tactic:
;

Goal state after:
case h
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
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2} ↔ p.2 ∈ {l | p.1 ∈ l}
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι✝ : Type u_2
κ✝ : ι✝ → Type u_2
f : (a : ι✝) → κ✝ a → Digraph V
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝

Tactic:
;

Goal state after:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι✝ : Type u_2
κ✝ : ι✝ → Type u_2
f : (a : ι✝) → κ✝ a → Digraph V
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G✝ : Digraph V
a b : V
inst✝ : IsEmpty V
G : Digraph V
⊢ G.Adj = ⊥.Adj

Tactic:
;

Goal state after:
ι : Sort u_1
V : Type u_2
G✝ : Digraph V
a b : V
inst✝ : IsEmpty V
G : Digraph V
⊢ G.Adj = ⊥.Adj
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 * A)) < 2 * ↑(#A)

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n + 1

Tactic:
;

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).1 ≤ n
⊢ (↑ijh).1 < n + 1

Tactic:
;

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).1 ≤ n
⊢ (↑ijh).1 < n + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n + 1

Tactic:
;

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).2 ≤ n
⊢ (↑ijh).2 < n + 1

Tactic:
;

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).2 ≤ n
⊢ (↑ijh).2 < n + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: ⊢ treesOfNumNodesEq 0 = {nil}

Tactic:
rw [treesOfNumNodesEq]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
rw [treesOfNumNodesEq]

Goal state after:
n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh ↦ pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
;

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! *
      ((∏ x_1 ∈ Finset.range c, (x_1 * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1)) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)

Tactic:
;

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! *
      ((∏ x_1 ∈ Finset.range c, (x_1 * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1)) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
;

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ ((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
          ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        (map (fun j ↦ j !) m).prod *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    m.sum !

Tactic:
rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)]

Goal state after:
m : Multiset ℕ
⊢ (∏ i ∈ m.toFinset, (i * count i m)!) *
      (((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
            ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
          (map (fun j ↦ j !) m).prod *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
⊢ ↑(p + q + r) = ↑(p + (q + r))

Tactic:
;

Goal state after:
p q r : DyckWord
⊢ ↑(p + q + r) = ↑(p + (q + r))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑(0 + p) = ↑p

Tactic:
;

Goal state after:
p : DyckWord
⊢ ↑(0 + p) = ↑p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑(p + 0) = ↑p

Tactic:
;

Goal state after:
p : DyckWord
⊢ ↑(p + 0) = ↑p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
h : ↑((fun x ↦ p + x) q) = ↑((fun x ↦ p + x) r)
⊢ ↑q = ↑r

Tactic:
;

Goal state after:
p q r : DyckWord
h : ↑((fun x ↦ p + x) q) = ↑((fun x ↦ p + x) r)
⊢ ↑q = ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
h : ↑((fun x ↦ x + p) q) = ↑((fun x ↦ x + p) r)
⊢ ↑q = ↑r

Tactic:
;

Goal state after:
p q r : DyckWord
h : ↑((fun x ↦ x + p) q) = ↑((fun x ↦ x + p) r)
⊢ ↑q = ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0

Tactic:
;

Goal state after:
p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0