mathlib-initiative/mathlib-tactics huggingface dataset:
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
x a : G
ha : a ∈ A
⊢ a •> x ∈ A ↔ a * x ∈ A

Tactic:
smul_eq_mul

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_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a * x ∈ A ↔ a * x ∈ A
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:
smul_eq_mul

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_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
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)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a c : G
ha : a ∈ A⁻¹ * A
⊢ c ∈ A⁻¹ * A → a * c ∈ A⁻¹ * A

Tactic:
hc

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)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a c : G
ha : a ∈ A⁻¹ * A
hc : c ∈ A⁻¹ * A
⊢ a * c ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1

Tactic:
obtain ⟨p, -⟩ := @exists_config P L _ _

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
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
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#(A ×ˢ A))

Tactic:
card_eq_sum_card_fiberwise h₂,

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
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) <
    ↑(∑ b ∈ A⁻¹ * A,
        #({a ∈ A ×ˢ A |
            (match a with
              | (x, y) => x * y⁻¹) =
              b}))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
apply append_assoc

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 *
      ((count a (a ::ₘ m))! * ∏ x ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count x (a ::ₘ m))!) =
    (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!

Tactic:
← hrest

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.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : AddCommMonoid 𝕜
inst✝ : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ ∑ x ∈ ∅, f a x * g x b = 0

Tactic:
sum_empty

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : AddCommMonoid 𝕜
inst✝ : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ 0 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddCommMonoid 𝕜
inst✝¹ : AddCommMonoid 𝕝
inst✝ : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
h : ¬a ≤ b
⊢ ∑ x ∈ ∅, f a x • g x b = 0

Tactic:
sum_empty

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddCommMonoid 𝕜
inst✝¹ : AddCommMonoid 𝕝
inst✝ : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
h : ¬a ≤ b
⊢ 0 = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
have u : p.nest.toList = U :: p.toList ++ [D] := rfl

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ p.nest.firstReturn = (↑p).length + 1
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case pos
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 + ∑' (i : ℕ), (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0

Tactic:
rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp]

Goal state after:
case pos
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 + ∑' (i : ℕ), (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0 + ∑' (i : ℕ), 0
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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a •> b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N

Tactic:
smul_eq_mul

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) (pentagonalSeries R)

Tactic:
pentagonal_injective.hasSum_iff fun n hn ↦ by simp [coeff_pentagonalSeries_eq_zero R hn]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case refine_3
⊢ (fun n ↦ rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦ rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
rw [isBigO_exp_comp_exp_comp]

Goal state after:
case refine_3
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop ((fun n ↦ -4 * √(Real.log ↑n)) - fun n ↦ -4 * √(Real.log ↑((n - 3) / 6)))
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ G.IsLink e x y → ((x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X)

Tactic:
exact fun h ↦ by simp [h.left_mem, h.right_mem]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → G.Adj ↑a✝ ↑b✝

Tactic:
exact id

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ G.Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)

Tactic:
exact id

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg
κ : Type (max v u)
inst✝ : Finite κ
h : ¬Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
· exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ ∅ = M

Tactic:
delete_eq_self_iff

Goal state after:
α : Type u_1
M : Matroid α
⊢ Disjoint ∅ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D ＼ X = M ＼ D

Tactic:
delete_eq_self_iff

Goal state after:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ Disjoint X (M ＼ D).E
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ N.E ⊆ M.E

Tactic:
obtain ⟨C, D, rfl⟩ := h
  exact sdiff_subset.trans sdiff_subset

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ X ⊆ M.E ∧ Disjoint X I

Tactic:
and_iff_left hXI

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
by
  rw [hI.contract_eq_contract_delete, delete_dep_iff, hI.indep.contract_dep_iff, and_comm,
    ← and_assoc, ← disjoint_union_right, sdiff_union_of_subset hI.subset, disjoint_comm, and_comm]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
⊢ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support → ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
hc

Goal state after:
case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ Nonempty (Path r b)

Tactic:
rcases show ∃ n, height b < n from ⟨_, Nat.lt_add_one _⟩ with ⟨n, hn⟩
      induction n generalizing b with
      | zero => exact False.elim (Nat.not_lt_zero _ hn)
      | succ n ih =>
      rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
      · exact ⟨Path.nil⟩
      · rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
        exact ⟨p.cons e⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ (b : WideSubquiver.toType V (geodesicSubtree r)), b = r ∨ ∃ a, Nonempty (a ⟶ b)

Tactic:
intro b
      rcases hp : shortestPath r b with (_ | ⟨p, e⟩)
      · exact Or.inl rfl
      · exact Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
hm : ∃ a, ¬coeff a (P S ()) = 0 ∧ mapDomain (fun x ↦ i) a = m
⊢ ∃ e ≤ #S, m = single i e

Tactic:
obtain ⟨e, he, hm⟩ := hm

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
⊢ ∃ e ≤ #S, m = single i e
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
hℬ : s ∉ upperClosure ↑ℬ
⊢ #⊥ + #((𝒜 ⊻ ℬ).truncatedInf s) = #⊥ + #⊥

Tactic:
truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
hℬ : s ∉ upperClosure ↑ℬ
⊢ #⊥ + #⊥ = #⊥ + #⊥
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False

Tactic:
exact
    h.2
      (eq_singleton_iff_unique_mem.2
        ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t →
    (t = s.erase (s.min' hs) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
      ∃ a ∉ t,
        #s = #(insert a t) ∧
          (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
rintro cards' (rfl | ⟨k, hks, hkt, z⟩)

Goal state after:
case mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ ∃ a ∉ s.erase (s.min' hs),
    #s = #(insert a (s.erase (s.min' hs))) ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))

case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #(insert a s) = k + 1

Tactic:
rw [card_insert_of_notMem ha, hs]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
· rw [← compress_sdiff_sdiff A B] at hAB hBA
      cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
h' : u = v
⊢ G.Reachable u v

Tactic:
exact h' ▸ Reachable.rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
⊢ w ∈ G.support

Tactic:
obtain ⟨y, hy⟩ := adj_of_mem_walk_support p hp hw

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
y : V
hy : y ∈ p.support ∧ G.Adj w y
⊢ w ∈ G.support
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r ↑𝒜
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r ↑ℬ
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
hℬ𝒞 : ℬ ⊆ 𝒞
⊢ ℬ = 𝒞

Tactic:
exact eq_of_subset_of_card_le hℬ𝒞 hcard.ge

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = c

Tactic:
simp only [← h]

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = G.connectedComponentMk v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = c

Tactic:
simp only [← h]

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = G.connectedComponentMk w
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : α
⊢ hs.piecewise f x ∈ ⋃ i, f i '' s i

Tactic:
exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ G.chromaticNumber ≤ ↑n

Tactic:
by
  rw [hc.chromaticNumber_eq_sInf]
  norm_cast
  apply csInf_le chromaticNumber_bddBelow
  exact hc

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
⊢ False

Tactic:
have hpq' := hb pwv.reverse

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.reverse.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : G.chromaticNumber ≠ ⊤
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
by
  rw [chromaticNumber_ne_top_iff_exists] at h
  obtain ⟨n, hn⟩ := h
  exact colorable_chromaticNumber hn

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
⊢ G'.Colorable m → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Tactic:
hc

Goal state after:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m