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
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A

Tactic:
refine ⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩

Goal state after:
case refine_1
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ↑(#(A * S)) ∈ map Nat.castEmbedding (Icc (#S) (t * #S))

case refine_2
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ K * ↑(#A) ∈ K •> map Nat.castEmbedding (Icc 1 t)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case a
x : ℕ
hx : 9 ≤ x
⊢ (x - 3) / 6 ≤ x

Tactic:
· lia

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
y' : α
h : G.IsLink e x y
h' : G.IsLink e x y'
⊢ x = x ∧ y = y' ∨ x = y' ∧ y = x

pp: case inr
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' : α
h : G.IsLink e x y
h' : G.IsLink e x' x
⊢ x = x' ∧ y = x ∨ x = x ∧ y = x'

Tactic:
· simp [h.right_unique h']

Goal state after:
case inr
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
x' : α
h : G.IsLink e x y
h' : G.IsLink e x' x
⊢ x = x' ∧ y = x ∨ x = x ∧ y = x'
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : α
edgeSet : Set β
⊢ ∀ (e : β) (x : α), (banana u v edgeSet).Inc e x ↔ (banana v u edgeSet).Inc e x

Tactic:
simp [or_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G ≤s H
⊢ G.toSimpleGraph ≤ ⋯ ▸ H.toSimpleGraph

Tactic:
rintro u v hadj
  match G, H with
  | ⟨GV, GL, GE, _, _, _, _⟩, ⟨HV, HL, HE, _, _, _, _⟩ =>
    obtain ⟨hne, hadj⟩ := toSimpleGraph_adj .. ▸ hadj
    obtain ⟨hle, h⟩ := h
    simp only at h
    subst GV
    simp [toSimpleGraph_adj, hne, hadj.mono hle]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}

Tactic:
filter_upwards [hU]

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
⊢ (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D)

Tactic:
rw [← restrict_compl, isBase_restrict_iff]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥s
⊢ ↑(↑f ↑x) < Fintype.card ↥s

Tactic:
simp [← mem_prefixed.1 f.2 x]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E

Tactic:
dual_dual,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ M✶ ＼ C = M✶ ↔ Disjoint C M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶✶✶.IsBasis ((M✶✶.E \ I) \ B) (M✶✶✶.E \ I) ∧ B ⊆ M✶✶.E ↔ M✶.IsBase (M✶.E \ (B ∪ I)) ∧ B ∪ I ⊆ M✶.E)

Tactic:
dual_dual,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M✶✶.E \ I) \ B) (M✶.E \ I) ∧ B ⊆ M✶✶.E ↔ M✶.IsBase (M✶.E \ (B ∪ I)) ∧ B ∪ I ⊆ M✶.E)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M✶✶.E \ I) \ B) (M✶.E \ I) ∧ B ⊆ M✶✶.E ↔ M✶.IsBase (M✶.E \ (B ∪ I)) ∧ B ∪ I ⊆ M✶.E)

Tactic:
dual_dual,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → (M✶.IsBasis ((M.E \ I) \ B) (M✶.E \ I) ∧ B ⊆ M.E ↔ M✶.IsBase (M✶.E \ (B ∪ I)) ∧ B ∪ I ⊆ M✶.E)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) f =
    coeff (m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b)
      ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b)

Tactic:
coeff_mul_of_degree_add (m := m),

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) f =
    m.leadingCoeff ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) * m.leadingCoeff b
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
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
this : (rename ⇑e.symm) P = 0
that : Injective ⇑(rename ⇑e.symm)
⊢ P = 0

Tactic:
RingHom.injective_iff_ker_eq_bot

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
this : (rename ⇑e.symm) P = 0
that : RingHom.ker (rename ⇑e.symm) = ⊥
⊢ P = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree (b i * (monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) ≤
    m.toSyn (m.degree f)

Tactic:
degree_mul_le,

Goal state after:
case pos
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree (b i) + m.degree ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) ≤
    m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mpr
V : Type u_2
inst✝ : Quiver V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))
w : V
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
⊢ w = v

Tactic:
by_contra hw_ne

Goal state after:
case mpr
V : Type u_2
inst✝ : Quiver V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))
w : V
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
hw_ne : ¬w = v
⊢ False
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
⊢ q.length = 0

Tactic:
by
  have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h
  have : p.length + q.length = 0 := by
    simpa [length_comp] using hlen
  exact Nat.eq_zero_of_add_eq_zero_left this

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
ht'

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)

Tactic:
simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ (if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ (⇑e ∘ id) else ⊥) =
    if h : a ∈ upperClosure ↑s then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥
Module: Mathlib.Order.Irreducible

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
⊢ ∃ i ∈ s, f i = a

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
induction k generalizing t with
  | zero => simp
  | succ k ih =>
    simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]
    constructor
    · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
    · rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩
      rw [insert_subset_iff] at hut
      exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

Goal state after:
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ≤ lift b → a ≤ b

Tactic:
rintro ⟨_⟩

Goal state after:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a ≤ b
⊢ a ≤ b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ≤ comp b → b ≤ a

Tactic:
rintro ⟨_⟩

Goal state after:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b ≤ a
⊢ b ≤ a
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ≤ comp b → Disjoint a b

Tactic:
rintro ⟨_⟩

Goal state after:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a < lift b → a < b

Tactic:
rintro ⟨_⟩

Goal state after:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a < b
⊢ a < b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a < comp b → b < a

Tactic:
rintro ⟨_⟩

Goal state after:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b < a
⊢ b < a
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a < comp b → Disjoint a b

Tactic:
rintro ⟨_⟩

Goal state after:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ ⋯.choose ∧ 2 * #⋯.choose = 2 ^ Fintype.card α ∧ (↑⋯.choose).Intersecting

Tactic:
← Fintype.card_finset

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ ⋯.choose ∧ 2 * #⋯.choose = Fintype.card (Finset α) ∧ (↑⋯.choose).Intersecting
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:

Tactic:
_ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
by
  refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
  · simp
  · rfl
  intro a 𝒜 ih₀ ih₁
  set ℬ : Finset (Finset α) :=
    ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).image (insert a)
  have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) := by
    refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
    simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_ofPred_eq, and_imp,
      mem_shatterer]
    exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
  rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]
  refine (Nat.add_le_add ih₁ ih₀).trans ?_
  rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]
  swap
  · simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]
    rintro _ (hs | hs) s - rfl
    · exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _
    · exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _
  refine card_mono <| union_subset (union_subset ?_ <| shatterer_mono <| filter_subset _ _) ?_
  · simp only [subset_iff, mem_shatterer]
    rintro s hs t ht
    obtain ⟨u, hu, rfl⟩ := hs ht
    rw [mem_memberSubfamily] at hu
    refine ⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩
    obtain ⟨v, hv, hsv⟩ := hs.exists_inter_eq_singleton ha
    rw [mem_memberSubfamily] at hv
    rw [← singleton_subset_iff (a := a), ← hsv] at hv
    exact hv.2 inter_subset_right
  · refine forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_
    simp only [mem_inter, mem_shatterer] at hs
    rw [subset_insert_iff] at ht
    by_cases ha : a ∈ t
    · obtain ⟨u, hu, hsu⟩ := hs.1 ht
      rw [mem_memberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rw [← insert_inter_distrib, hsu, insert_erase ha]
    · obtain ⟨u, hu, hsu⟩ := hs.2 ht
      rw [mem_nonMemberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ G.Reachable x✝¹ x✝ ↔ Relation.ReflTransGen G.Adj x✝¹ x✝

Tactic:
exact reachable_iff_reflTransGen ..

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
⊢ ∀ (v : ↥C), C.toSimpleGraph.Reachable ⟨u, hu⟩ v

Tactic:
⟨v, hv⟩

Goal state after:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
v : V
hv : v ∈ C
⊢ C.toSimpleGraph.Reachable ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this✝ : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ b ∈ image Fin.val A, b < k

Tactic:
simp_rw [mem_image]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this✝ : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ (b : ℕ), (∃ a ∈ A, ↑a = b) → b < k
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hreach : G.Reachable u v
⊢ s(u, v) ∈ G.edgeSet

Tactic:
have : G.deleteEdges {s(u, v)} < G := deleteEdges_le _ |>.lt_of_ne <| by grind [isBridge_iff]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hreach : G.Reachable u v
this : G.deleteEdges {s(u, v)} < G
⊢ s(u, v) ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}

Tactic:
apply le_csInf (colorable_set_nonempty_of_colorable hc)

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ ∀ b ∈ {n | G.Colorable n}, Nat.succ 0 ≤ b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 0 u v

Tactic:
simp [IsEdgeReachable]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
rw [← hw, ← Walk.length_map (.ofLE h)]

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑(Walk.map (Hom.ofLE h) w✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ Set.univ.Nonempty

Tactic:
rw [dist_eq_sInf] at h
  simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using
    Nat.nonempty_of_pos_sInf h

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
rw [← hw, ← Walk.length_map (.ofLE h)]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ (Walk.map (Hom.ofLE h) w✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hl : w = p.snd
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨p, ⟨h, hl.symm, rfl⟩⟩

Goal state after: