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

Goal state before:
pp: ⊢ StrictAntiOn pentagonal (Set.Iic 0)

Tactic:
apply strictAntiOn_of_add_one_lt Set.ordConnected_Iic

Goal state after:
⊢ ∀ (a : ℤ), ¬IsMax a → a ∈ Set.Iic 0 → a + 1 ∈ Set.Iic 0 → pentagonal (a + 1) < pentagonal a
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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto
    (fun n ↦ ∑ i ∈ Finset.range n, (powMulProdOneSubPow k i x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) i x))
    atTop (𝓝 (0 - aux k 0 x))

Tactic:
aux_sub_aux,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun n ↦ ∑ x_1 ∈ Finset.range n, (aux k (x_1 + 1) x - aux k x_1 x)) atTop (𝓝 (0 - aux k 0 x))
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
hK : K ≤ 1
hS : S.Nonempty
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
hA : #A ≤ #(A ∩ B)
⊢ #(A ∩ B) ≤ #B

Tactic:
by grw [inter_subset_right]

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

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

Tactic:
rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia

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

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

Tactic:
calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;>
      · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
        we need to re-enable model-based theory combination in `lia` for this to go through. -/
        lia +mbtc
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia

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

Goal state before:
pp: case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
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)
⊢ ↑(#((↑H).toFinset * S)) ≤ (2 / ε - 1) * ↑(#(↑H).toFinset)

Tactic:
← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])

Goal state after:
case hab
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)
⊢ (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))
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

Tactic:
simp [h.right_unique h']

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]

Goal state after:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_1
α : 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
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C (Sum.elim (↑p.line (some x)) (↑(map some l') (some x))) = p.color

Tactic:
Line.map_apply,

Goal state after:
case neg.refine_1
α : 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
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C (Sum.elim (↑p.line (some x)) (some ∘ ↑l' x)) = p.color
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M

pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, (Option.map ?refine_2 (l.idxFun i)).getD 0) = c

Tactic:
· exact fun m => m

Goal state after:
case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = 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
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
this : ∀ (p q : Path r b), p = q
⊢ ∀ (a : Path r b), a = default

Tactic:
intro p
        apply this

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case e'_2
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ : f ![a, b] = f ![(fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0, (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1
⊢ (fun j ↦ ![![a, b], ![b, a]] j 0) = ![a, b]

Tactic:
simp [Matrix.const_fin1_eq]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case e'_3
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ : f ![a, b] = f ![(fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0, (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1
⊢ (fun j ↦ ![![a, b], ![b, a]] j 1) = ![b, a]

Tactic:
simp [Matrix.const_fin1_eq]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : ∀ (b_1 : ↑{b}), m.toSyn (m.degree (↑b_1 * g b_1)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c

Tactic:
specialize h1 ⟨b, by simp⟩

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * g ⟨b, ⋯⟩)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
b v : V
p : Path v b
hv : v ∈ nil.vertices
⊢ nil = nil.comp nil

Tactic:
by simp only [comp_nil]

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ ∅
⊢ p 𝒜

Tactic:
subset_empty

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s = ∅
⊢ p 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case pos
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∈ B
⊢ n ∈ A + B

pp: case neg
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
⊢ n ∈ A + B

Tactic:
· exact ⟨0, hA, n, ⟨hnB, by simp⟩⟩

Goal state after:
case neg
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then {b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x else ⊤) = if a ≤ b then b else ⊤

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : a ≤ b
⊢ ({b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x) = b

case neg
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : ¬a ≤ b
⊢ ⊤ = ⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then {b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x else ⊥) = if b ≤ a then b else ⊥

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : b ≤ a
⊢ ({b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x) = b

case neg
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : ¬b ≤ a
⊢ ⊥ = ⊥
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
b c : α
ha : b ⊓ c = a
⊢ b = a ∨ c = a

Tactic:
by simpa [← ha] using h ha.le

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ (↑(card α) - ↑(#(if t ⊆ s then s else ⊤))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : t ⊆ s
⊢ (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))

case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : ¬t ⊆ s
⊢ (↑(card α) - ↑(#⊤)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) = 0
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s

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

Tactic:
· obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h
    rwa [Subsingleton.elim ⊥ a]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
by
  refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
  rw [Nat.two_mul, card_disjUnion, card_map]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s, insert a s}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s}

case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {insert a s}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ ∅
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ {s}, f x = f s + 0

case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ ∅, f x = 0 + 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t

case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_1
ι : 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 ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(s.biUnion f')

Tactic:
rw [coe_biUnion]

Goal state after:
case inr.cons.refine_1
ι : 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 ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsUpperSet (⋃ x ∈ ↑s, ↑(f' x))
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_3
ι : 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 ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]

Goal state after:
case inr.cons.refine_3
ι : 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 ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 ^ Fintype.card α + #(s.biUnion f')) ≤
    2 ^ Fintype.card α * (2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi))))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s

Tactic:
have : a ∉ U := fun H ↦ ha.not_gt ((le_max' _ _ H).trans_lt h)

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this✝ : a ∉ V
this : a ∉ U
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet ↑𝒜.shatterer

Tactic:
exact isLowerSet_shatterer _

Goal state after: