mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (mu' 𝕜) x b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
;

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (mu' 𝕜) x b = ∑ x ∈ Icc a b, (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (mu' 𝕜) x b = (mu' 𝕜) x b

Tactic:
;

Goal state after:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (mu' 𝕜) x b = (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case hbc
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 := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := ⋯
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ ↑(#A) ≤ (2 - K) * ↑l + (K - 1) * ↑(#S)

Tactic:
;

Goal state after:
case hbc
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 := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := ⋯
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ ↑(#A) ≤ (2 - K) * ↑l + (K - 1) * ↑(#S)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑{ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } ≠ []

Tactic:
;

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑{ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } ≠ []
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case a
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ (if x ≤ b then mud a x else 0) = mud a x

Tactic:
;

Goal state after:
case a
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ (if x ≤ b then mud a x else 0) = mud a x
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
rw [take_take, min_eq_left ub.le]

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

Goal state before:
pp: p : DyckWord
⊢ p.nest.take ((↑p).length + 1 + 1) ⋯ = p.nest

Tactic:
;

Goal state after:
p : DyckWord
⊢ p.nest.take ((↑p).length + 1 + 1) ⋯ = p.nest
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑(p.nest.take ((↑p).length + 1 + 1) ⋯) = ↑p.nest

Tactic:
;

Goal state after:
p : DyckWord
⊢ ↑(p.nest.take ((↑p).length + 1 + 1) ⋯) = ↑p.nest
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1

Tactic:
;

Goal state after:
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑(p.nest.drop ((↑p).length + 1 + 1) ⋯) = ↑0

Tactic:
;

Goal state after:
p : DyckWord
⊢ ↑(p.nest.drop ((↑p).length + 1 + 1) ⋯) = ↑0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case a
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≤ x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) (toDual x) (toDual x✝) = (mu 𝕜) x x✝

Tactic:
;

Goal state after:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≤ x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) (toDual x) (toDual x✝) = (mu 𝕜) x x✝
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q

Tactic:
;

Goal state after:
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ q

Tactic:
;

Goal state after:
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ q
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y

Tactic:
;

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ r + p

Tactic:
;

Goal state after:
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ r + p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y

Tactic:
;

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
x y : α × β
hxy : x ≤ y
⊢ ((zeta 𝕜).prod (zeta 𝕜)) x y = (zeta 𝕜) x y

Tactic:
;

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
x y : α × β
hxy : x ≤ y
⊢ ((zeta 𝕜).prod (zeta 𝕜)) x y = (zeta 𝕜) x y
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case a
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 := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
this : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))
⊢ A ∩ z⁻¹ •> A ∪ A ∩ w •> A ⊆ A

Tactic:
;

Goal state after:
case a
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 := ⋯
H : Subgroup G := ⋯
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
this : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))
⊢ A ∩ z⁻¹ •> A ∪ A ∩ w •> A ⊆ A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
this : #A ≤ #(A * S)
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
this : #A ≤ #(A * S)
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S ∅
⊢ False

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S ∅
⊢ False
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 ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ ∃ a ∈ s, a + 1 = i

Tactic:
refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 ∈ range d

case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 + 1 = i
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
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this✝ : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
this : connectivity K S ≤ expansion K S (A ∩ B)
⊢ expansion K S (A ∩ B) = connectivity K S

Tactic:
have := connectivity_le_expansion hK hS <| hAB.mono inter_subset_union

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this✝¹ : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
this✝ : connectivity K S ≤ expansion K S (A ∩ B)
this : connectivity K S ≤ expansion K S (A ∪ B)
⊢ expansion K S (A ∩ B) = connectivity K S
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case hbc
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⋯
A : Finset G
hA : t + 1 ≤ #A
⊢ (κ + 1) / (1 - K) < ↑t + 1

Tactic:
;

Goal state after:
case hbc
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⋯
A : Finset G
hA : t + 1 ≤ #A
⊢ (κ + 1) / (1 - K) < ↑t + 1
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (1 - K) * ↑(t + 1) ≤ (1 - K) * ↑(#A)

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (1 - K) * ↑(t + 1) ≤ (1 - K) * ↑(#A)
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k ≤ n
⊢ k < n + 1

Tactic:
;

Goal state after:
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k ≤ n
⊢ k < n + 1
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
;

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder + (n + 1).largeSchroder +
        (n + 1).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < (X ^ ((k + 1) * m) * ∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
grw [← le_order_mul, order_X_pow]

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < ↑((k + 1) * m) + (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ x ∈ Set.range Neg.neg

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ x ∈ Set.range Neg.neg
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ - -x = x

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ - -x = x
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ∀ (n : ℕ), (∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) → ∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
⊢ 1 - ε / 2 < 1

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
⊢ 1 - ε / 2 < 1
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
;

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

Goal state before:
pp: case a
n : ℕ
α : Type := ⋯
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Iio ⟨n, ⋯⟩ ⊆ univ

Tactic:
;

Goal state after:
case a
n : ℕ
α : Type := ⋯
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Iio ⟨n, ⋯⟩ ⊆ univ
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
;

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

Goal state before:
pp: x : ℕ
hx : 15 ≤ x
⊢ x ≤ 12 * ((x - 3) / 6)

Tactic:
;

Goal state after:
x : ℕ
hx : 15 ≤ x
⊢ x ≤ 12 * ((x - 3) / 6)