mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) (c + d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
rw [map_add, add_smul]

Goal state after:
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 ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hg' : g ∉ Set.range toFinsuppAntidiag
this : ∃ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0
⊢ ∏ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0

Tactic:
obtain ⟨i, hi, hi'⟩ := this

Goal state after:
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
hg' : g ∉ Set.range toFinsuppAntidiag
i : ℕ
hi : i ∈ s
hi' : (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0
⊢ ∏ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 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))
this : ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) ≤ ↑(#A)
⊢ 0 < ↑(#(z⁻¹ •> A ∩ w •> A))

Tactic:
have :
          (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) + #((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) =
            #(A ∩ z⁻¹ •> A) + #(A ∩ w •> A) := mod_cast card_inter_add_card_union ..

Goal state after:
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))
this✝ : ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) ≤ ↑(#A)
this : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) + ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) = ↑(#(A ∩ z⁻¹ •> A)) + ↑(#(A ∩ w •> A))
⊢ 0 < ↑(#(z⁻¹ •> A ∩ w •> A))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0

Tactic:
tsum_eq_single (Multiset.count i p.parts - 1) ?_

Goal state after:
case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0

Tactic:
· rw [mul_comm]
      simp [Nat.sub_add_cancel (Multiset.one_le_count_iff_mem.mpr hi)]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
⊢ E(H) ⊆ E(G)

Tactic:
by
  intro e he
  obtain ⟨x, y, h'⟩ := exists_isLink_of_mem_edgeSet he
  exact (h'.mono h).edge_mem

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ E(G) ∩ F₁ ∩ F₂ = E(G) ∩ (F₁ ∩ F₂)

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ E(G) ∩ F₁ ∩ F₂ = E(G) ∩ F₁ ∩ F₂
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : (bouquet v E(G)).Inc e x
⊢ G.Inc e x

Tactic:
simp only [bouquet_inc] at h

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
⊢ G.Inc e x
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
← delete_inter_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ (Dᶜ ∩ M.E)) ∧ Disjoint (X ∩ (Dᶜ ∩ M.E)) D ↔ M.IsBasis' I (X \ D)

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ Dᶜ ∩ M.E) ∧ Disjoint (X ∩ Dᶜ ∩ M.E) D ↔ M.IsBasis' I (X \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) ∩ Dᶜ ∩ M.E = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
refine Or.inr (mono_of_mono ⟨p.line, p.color, ?_⟩)

Goal state after:
case pos
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ ∀ (x : Option α), C' (↑p.line x) = p.color
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ＼ D

Tactic:
← delete_inter_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ＼ (D ∩ M.E)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Tactic:
classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X \ I) = M ／ I ＼ ((X ∩ M.E) \ I)

Tactic:
← delete_inter_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X \ I ∩ (M ／ I).E) = M ／ I ＼ ((X ∩ M.E) \ I)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
⊢ M ／ X = M ＼ X

Tactic:
rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
⊢ P = C (constantCoeff P)

Tactic:
ext m

Goal state after:
case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
⊢ coeff m P = coeff m (C (constantCoeff P))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
⊢ (M ／ C).Spanning (X \ C)

Tactic:
have hXE := hX.subset_ground
  rw [contract_spanning_iff', and_iff_left disjoint_sdiff_left]
  exact hX.superset (by tauto_set) (by tauto_set)

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ ((optionEquivLeft R σ) P).coeff d = 0

Tactic:
ext m

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
⊢ coeff m (((optionEquivLeft R σ) P).coeff d) = coeff m 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
rw [delete_eq_restrict, delete_eq_restrict, contract_ground, sdiff_sdiff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_sdiff])]

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path i i₀
⊢ ∃ p, 0 < p.length

Tactic:
obtain ⟨p₂⟩ := h_sc j₀ j

Goal state after:
V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path i i₀
p₂ : Path j₀ j
⊢ ∃ p, 0 < p.length
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
rintro rfl

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ : V
pPrev : Path a b✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
e : b✝ ⟶ v
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔ s ∈ image (fun s ↦ s.erase a) 𝒜

Tactic:
simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) ≤ ↑k - 1

Tactic:
← Nat.cast_pred hk',

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) ≤ ↑(k - 1)
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A

Tactic:
rintro rfl

Goal state after:
case mpr
inst✝ : DecidablePred fun x ↦ x ∈ Set.univ
hA : 0 ∈ Set.univ
⊢ {0}ᶜ ⊆ Set.univ
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ (s.erase a).erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
erase_idem

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → t.Nonempty

Tactic:
by
  simp_rw [Finset.Nonempty, mem_disjSups]
  exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupIrred a
⊢ a ≠ ⊥

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupIrred ⊥
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupPrime a
⊢ a ≠ ⊥

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
a : α
inst✝ : OrderTop α
ha : InfIrred a
⊢ a ≠ ⊤

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfIrred ⊤
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
a : α
inst✝ : OrderTop α
ha : InfPrime a
⊢ a ≠ ⊤

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfPrime ⊤
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜

Tactic:
rw [← Hcomp.eq] at ht

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
insert_eq,

Goal state after:
case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum ({s} ∪ 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
h : {⊥}.Intersecting
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

Tactic:
rintro rfl
    exact intersecting_singleton.1 h rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
  · rintro rfl
    exact intersecting_singleton.1 h rfl
  have := h.1.eq ha hb (Classical.not_not.2 hab)
  rw [this, disjoint_self] at hab
  rw [hab] at hb
  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.Intersecting

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
⊢ ∅ ≠ {⊥}
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(ℬ ∩ 𝒜) ≤ #𝒜 * #ℬ

Tactic:
mul_comm #𝒜

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
have : DecidableEq ι := by
    classical
    infer_instance

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ a ≠ ⊥

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ ↑s ∧ ⊥ᶜ ∉ ↑s
⊢ False
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False