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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False

Tactic:
· simp at h

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : w 0 • v = v 0 • w → -w 0 = 0 ∧ v 0 = 0
h21 : w 1 • v = v 1 • w → -w 1 = 0 ∧ v 1 = 0
h22 : w 2 • v = v 2 • w → -w 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
hv',

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : w 0 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 0 • w → -w 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 : w 1 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 1 • w → -w 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 : w 2 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 2 • w → -w 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
hv',

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬![v 0, v 1, v 2] = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

Tactic:
simp_rw [← sdiff_eq_empty_iff_subset]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ \ 𝒜₂ = ∅ ∨ 𝒜₂ \ 𝒜₁ = ∅
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) ⋯

Tactic:
cross_mk_of_cross_ne_zero

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ mk F ((crossProduct v) w) ?h = mk F ((crossProduct v) w) ⋯

case h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (crossProduct v) w ≠ 0
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
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
⊢ a * x ∈ ↑A ↔ x ∈ ↑H

Tactic:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Goal state after:
case refine_1
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 : a * x ∈ ↑A
⊢ x ∈ ↑H

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
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:
← mul_mem_A_comm ha,

Goal state after:
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
⊢ x * a ∈ A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ #(a •> A ∪ b •> A) ≤ #(B * A)

Tactic:
gcongr

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ∪ b •> A ⊆ B * A
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphInclusive.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∨ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
by tauto

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphStrict.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∧ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
by tauto

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

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G✝ : Digraph V
a b : V
G : Digraph V
v w : V
x✝ : (Digraph.completeDigraph V).Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
by tauto

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
hc : 0 < a ! * c
hq :
  (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ∏ j ∈ (a ::ₘ m).toFinset.erase 0, (count j (a ::ₘ m))! =
    (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!

Tactic:
rw [← Finset.mul_prod_erase _ _ (a := a) (by simp [*]), ← hrest] at hq

Goal state after:
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
hc : 0 < a ! * c
hq : (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ((count a (a ::ₘ m))! * rest) = (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!
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)
⊢ (↑(Fintype.card ↥H) / ↑(#S))⁻¹ ≤ ((φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) / ↑(#S))⁻¹

Tactic:
gcongr

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
i : ℕ
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)

Tactic:
replace h := toList_ne_nil.mpr hn.1
    have l1 : p.toList.take 1 = [p.toList.head h] := by rcases p with - | - <;> tauto
    have l3 : p.toList.length - 1 = p.toList.length - 1 - 1 + 1 := by
      rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
      · tauto
      · rename_i bal _
        cases s <;> simp at bal
      · tauto
    rw [← drop_one, take_drop, dropLast_eq_take, take_take]
    have ub : min (1 + i) (p.toList.length - 1) < p.toList.length :=
      (min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos_iff.mpr h).ne'))
    have lb : 0 < min (1 + i) (p.toList.length - 1) := by omega
    have eq := hn.2 lb ub
    set j := min (1 + i) (p.toList.length - 1)
    rw [← (p.toList.take j).take_append_drop 1, count_append, count_append, take_take,
      min_eq_left (by lia), l1, head_eq_U] at eq
    simp only [count_singleton', ite_true] at eq
    lia

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

Goal state before:
pp: case pos
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : a ≤ b
⊢ f a b = g a b

pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b

Tactic:
· exact h _ _ hab

Goal state after:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ↑(#(Icc a b))

Tactic:
card_eq_sum_ones,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ↑(∑ x ∈ Icc a b, 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
⊢ (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn

Tactic:
split_ifs with h; · simp [h]
  have u : (p + q).toList = p.toList ++ q.toList := rfl
  rw [firstReturn, findIdx_eq]
  · simp_rw [u, decide_eq_true_eq, getElem_range]
    have v := firstReturn_lt_length h
    constructor
    · rw [take_append, show p.firstReturn + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil, count_take_firstReturn_add_one h]
    · intro j hj
      rw [take_append, show j + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil]
      simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'
  · rw [length_range, u, length_append]
    exact Nat.lt_add_right _ (firstReturn_lt_length h)

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

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

Tactic:
have := p.count_D_le_count_U j

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
this : count D (List.take j ↑p) ≤ count U (List.take j ↑p)
⊢ decide (count U (List.take j ↑p) + 1 = count D (List.take j ↑p) + 0) = false
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
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ K * ↑(#A) ≤ K * ((2 - K) * ↑l + (K - 1) * ↑(#S))

Tactic:
gcongr

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.Partition.GenFun

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : x ∉ s
⊢ x ∣ g x

Tactic:
suffices g x = 0 by simp [this]
    contrapose! hx
    exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 <| by simpa using hx

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

Goal state before:
pp: p : DyckWord
⊢ p.nest.outsidePart = 0

Tactic:
by
  simp_rw [outsidePart, nest_ne_zero, dite_false, firstReturn_nest]
  rw [DyckWord.ext_iff]; apply drop_of_length_le
  simp_rw [nest, length_append, length_singleton]; lia

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

Goal state before:
pp: case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q

Tactic:
have := semilength_outsidePart_lt h
    exact (le_add_self p.outsidePart q).trans
      (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))

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

Goal state before:
pp: case inr.intro.calc_2
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
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
⊢ ↑(#({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})) ≤ ↑(#(↑H).toFinset)

Tactic:
gcongr

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 ∈ S | (K - 1) * ↑(#A) < ↑(r z)} ⊆ (↑H).toFinset
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: ⊢ StrictMonoOn pentagonal (Set.Ici 0)

Tactic:
apply strictMonoOn_of_lt_add_one Set.ordConnected_Ici

Goal state after:
⊢ ∀ (a : ℤ), ¬IsMax a → a ∈ Set.Ici 0 → a + 1 ∈ Set.Ici 0 → pentagonal a < pentagonal (a + 1)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, p i_1 then 1 else 0)) =
    PowerSeries.mk fun n ↦ ∑ p_1, ∏ x ∈ (Multiset.toFinsupp p_1.parts).support, if p x then 1 else 0

Tactic:
prod_boole

Goal state after:
case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, p i_1 then 1 else 0)) =
    PowerSeries.mk fun n ↦ ∑ x, if ∀ i ∈ (Multiset.toFinsupp x.parts).support, p i then 1 else 0
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
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
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))
⊢ ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))

Tactic:
gcongr

Goal state after:
case h
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))
⊢ A ∩ z⁻¹ •> A ⊆ z⁻¹ •> A

case h'
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))
⊢ A ∩ w •> A ⊆ w •> A
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0)) =
    PowerSeries.mk fun n ↦
      ∑ p, ∏ x ∈ (Multiset.toFinsupp p.parts).support, if (Multiset.toFinsupp p.parts) x < m then 1 else 0

Tactic:
prod_boole

Goal state after:
case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0)) =
    PowerSeries.mk fun n ↦
      ∑ x, if ∀ i ∈ (Multiset.toFinsupp x.parts).support, (Multiset.toFinsupp x.parts) i < m then 1 else 0
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
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
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:
gcongr

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
this : #A ≤ #(A * S)
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)

Tactic:
gcongr

Goal state after:
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) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * (↑t + 1)

Tactic:
gcongr

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