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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ (k + 1 + 1) * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ (k + 1) * x ^ 1 * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ (k + 1) * x ^ 1 * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ k * x ^ 1 * x ^ 1 * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc]

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

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)

Tactic:
← neg_injective.hasSum_iff (fun x hx ↦ by absurd hx; use -x; simp)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (pentagonalSeries R)
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
simp only [Set.toFinset_card, SetLike.coe_sort_coe]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)

Tactic:
exact he.right_mem

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)

Tactic:
exact he.right_mem

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
⊢ (map f G).Inc e (f v)

Tactic:
obtain ⟨w, hw⟩ := h
  exact ⟨f w, hw.map f⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht.refine_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ N ∩ {m' | m' * m = m}

Tactic:
refine ⟨N_mul _ mem'' _ mem', ?_⟩

Goal state after:
case ht.refine_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ {m' | m' * m = m}
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ : Type u_4
l✝ : Line α✝ ι✝
i : ι✝
a x : α✝
α : Type ?u.19
α' : Type ?u.22
ι : Type ?u.18
f : α → α'
l : Line α ι
⊢ Option.map f (l.idxFun ⋯.choose) = none

Tactic:
by simp only [l.proper.choose_spec, Option.map_none]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hns : ↑n < #s
⊢ (fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s))
      ((fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩)) n) =
    n

Tactic:
simp [hns]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M✶ ／ X = M✶✶✶ ／ X

Tactic:
dual_dual

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶ ／ X = M✶ ／ X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ＼ X)✶✶ = M✶ ＼ X

Tactic:
dual_dual

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M✶✶ = M

Tactic:
dual_dual

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M = M
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
dual_dual

Goal state after:
α : Type u_1
M : Matroid α
⊢ M = M
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.left
σ : 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
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)

Tactic:
intro j
      by_cases hj : j = i
      · apply le_trans degree_mul_le
        simp only [hj, hb0, Finsupp.single_eq_same, zero_add]
        apply le_of_eq
        simp only [EmbeddingLike.apply_eq_iff_eq]
        apply degree_smul_of_isRegular (Units.isRegular _)
      · simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]
        apply bot_le

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

Tactic:
simp only [Matroid.sum, mapEquiv_isBase_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
    Equiv.symm_symm, sigma_isBase_iff, Bool.forall_bool]

Goal state after:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ M.IsBase
        ((fun a ↦ Equiv.ulift a) ''
          Sigma.mk false ⁻¹'
            (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B) ∧
      N.IsBase
        ((fun a ↦ Equiv.ulift a) ''
          Sigma.mk true ⁻¹'
            (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B) ↔
    M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case e'_3
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 : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
hm : n ∈ P.support
⊢ d = n none

Tactic:
exact hn.1.symm

Goal state after:
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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
hf'0 : m.subLTerm f = 0
⊢ ∃ g' r',
    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

pp: case neg
σ : 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
hf'0 : ¬m.subLTerm f = 0
⊢ ∃ g' r',
    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

Tactic:
· refine ⟨0, 0, by simp [hf'0], ?_, by simp⟩
      intro b
      simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
      exact bot_le

Goal state after:
case neg
σ : 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
hf'0 : ¬m.subLTerm f = 0
⊢ ∃ g' r',
    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
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length < (shortestPath r b).length

Tactic:
simp_rw [h, Path.length_cons, Nat.lt_succ_iff]

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length ≤ p.length
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

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

Tactic:
intro h_no_bidir w h_same_scc

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
⊢ w = v
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.vertices ≠ []
⊢ p.vertices.getLast h = b

Tactic:
by
  induction p with
  | nil => simp only [vertices_nil, getLast_singleton]
  | cons p' e ih => simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j : V
p : Path i j
⊢ 0 < weight (fun {i j} ↦ w) p

Tactic:
induction p with
  | nil =>
      simp
  | cons p e ih =>
      have he : 0 < w e := hw e
      simpa [weight_cons] using mul_pos ih he

Goal state after:
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: case mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a

Tactic:
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩

Goal state after:
case mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: case mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩

Goal state after:
case mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Tactic:
rw [le_antisymm_iff, and_iff_right schnirelmannDensity_le_one]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
by
  rw [schnirelmannDensity_eq_one_iff]
  constructor
  · refine fun h => Set.eq_univ_of_forall fun x => ?_
    rcases eq_or_ne x 0 with rfl | hx
    · exact hA
    · exact h hx
  · rintro rfl
    exact Set.subset_univ {0}ᶜ

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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure (↑s ∪ ↑t)

Tactic:
upperClosure_union

Goal state after:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ t ⊼ sᶜˢ = t \\ s

Tactic:
infs_compls_eq_diffs

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ t \\ s = t \\ s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r + 1) ↑(∂⁺ 𝒜)

Tactic:
intro A h
  obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
  rw [card_insert_of_notMem hi, h𝒜 hA]

Goal state after:
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ a \ (c \ b) ≤ a ⊓ b ⊔ a \ c

Tactic:
rw [sdiff_sdiff_right', sup_comm]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ (b ⊔ u) \ v ∈ s

Tactic:
hvu hva,

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ (b ⊔ ⊥) \ v ∈ s
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ #{∅} * #{∅} ≤ 2 ^ #∅ * #({∅} ∩ {∅})

Tactic:
simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
        le_refl]

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

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ toColex t ≤ toColex (s.erase (s.min' hs))

Tactic:
simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)

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

Goal state before:
pp: case e'_4
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Tactic:
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
      exact Or.inl (mul_comm _ _)

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

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (V.erase (V.min' hV)).Nonempty

Tactic:
rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
⊢ x = y

Tactic:
by
    let h := @le_antisymm (Setoid α) _ _ _ hx hy
    rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]

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

Goal state before:
pp: case mp
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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
this : ∃ u, B ⊆ u ∧ u ⊆ range'k ∧ #u = i + #B
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
obtain ⟨C, BsubC, hCrange, hcard⟩ := this

Goal state after:
case mp
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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = i + #B
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ i, s i)
⊢ Bijective g

Tactic:
← bijOn_univ,

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ i, s i)
⊢ BijOn g univ univ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Tactic:
exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
e : Sym2 V
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Tactic:
by induction p <;> simp [*]

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

Goal state before:
pp: case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
· exact Or.inr hv

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

Goal state before:
pp: V : Type u_1
u v : V
h : u ≠ v
⊢ ⊥.edist u v = ⊤

Tactic:
rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h

Goal state after: