mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:

Tactic:
(∏ j : σ, (e a : σ → K) j ^ d j) =
        (e a : σ → K) i ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
      rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl
    _ = a ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
      rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
    _ = a ^ d i * ∏ j, x₀ j ^ d j := congr_arg _ (Fintype.prod_congr _ _ ?_)
    -- see below
    _ = (∏ j, x₀ j ^ d j) * a ^ d i := mul_comm _ _

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ∀ (a_1 : { j // j ≠ i }), ↑(e a) ↑a_1 ^ d ↑a_1 = x₀ a_1 ^ d ↑a_1
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ ∑ r ≤ Fintype.card α, #(𝒜 # r) = #𝒜

Tactic:
by
  let := Classical.decEq α
  rw [← card_biUnion, biUnion_slice]
  exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ toColex {a} ≤ toColex {b} ↔ a ≤ b

Tactic:
simp [toColex_le_singleton, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ v.submodule = K ∙ v.rep

Tactic:
conv_lhs => rw [← v.mk_rep]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬w.orthogonal v

Tactic:
by
  simp only [orthogonal_comm]
  exact exists_not_self_orthogonal v

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ⇑f ⊆ {a}} → f ∈ fiber (some a)

Tactic:
intro h_opfp

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ f ∈ fiber (some a)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)

Tactic:
intro x
      apply_fun fun x => Equiv.swap none (some a) x
      simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]
      rcases x with - | x
      · simp
      simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]
      by_cases x_vs_a : x = a
      · rw [x_vs_a, swap_apply_right]
        apply Option.some_ne_none
      have ne_1 : some x ≠ none := Option.some_ne_none _
      have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
      rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
      intro contra
      exact x_vs_a (h_opfp contra)

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a⁻¹ •> (A <• a) = A

Tactic:
rw [← smul_A_eq_A_smul ha, inv_smul_smul]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: ⊢ treesOfNumNodesEq 0 = {nil}

Tactic:
treesOfNumNodesEq

Goal state after:
⊢ {nil} = {nil}
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
treesOfNumNodesEq

Goal state after:
n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh ↦ pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * (c + 1)! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
rw [factorial_succ, pow_succ]; ring

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ i ≤ n, ∑ p, n.choose i * ((↑p).parts.erase (i + 1)).bell =
    ∑ x, n.choose (↑x.snd - 1) * (x.fst.parts.erase ↑x.snd).bell

Tactic:
rw [← Nat.range_succ_eq_Iic, Finset.sum_range, ← Fintype.sum_sigma']
    refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_
    simp [sigmaPartitionWithPartEquiv]

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

Goal state before:
pp: p : DyckWord
⊢ (if h : p.nest = 0 then 0 else (p.nest.take (p.nest.firstReturn + 1) ⋯).denest ⋯) = p

Tactic:
nest_ne_zero,

Goal state after:
p : DyckWord
⊢ (if h : False then 0 else (p.nest.take (p.nest.firstReturn + 1) ⋯).denest ⋯) = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.insidePart = p

Tactic:
simp_rw [insidePart, nest_ne_zero, dite_false, firstReturn_nest]

Goal state after:
p : DyckWord
⊢ (p.nest.take ((↑p).length + 1 + 1) ⋯).denest ⋯ = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ (if h : p.nest = 0 then 0 else p.nest.drop (p.nest.firstReturn + 1) ⋯) = 0

Tactic:
nest_ne_zero,

Goal state after:
p : DyckWord
⊢ (if h : False then 0 else p.nest.drop (p.nest.firstReturn + 1) ⋯) = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
have := semilength_insidePart_add_semilength_outsidePart_add_one h

Goal state after:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.insidePart.semilength < p.semilength
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
have := semilength_insidePart_add_semilength_outsidePart_add_one h

Goal state after:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.outsidePart.semilength < p.semilength
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

Tactic:
outsidePart_zero,

Goal state after:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0 ∨ m = 0
⊢ ↑p <:+: ↑0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0

Tactic:
outsidePart_zero,

Goal state after:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0 ∨ m = 0
⊢ p.semilength ≤ semilength 0
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun x ↦ ‖(↑x / 3 - 2) * ↑((x - 3) / 6) * rexp (-4 * √(Real.log ↑((x - 3) / 6)))‖) ≤ᶠ[atTop] fun n ↦
    ↑(ruzsaSzemerediNumberNat n)

Tactic:
filter_upwards [eventually_ge_atTop 6] with n hn

Goal state after:
n : ℕ
hn : 6 ≤ n
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
rintro l m hlm

Goal state after:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
⊢ l = m
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
cases h : l.idxFun (eι.symm i)

Goal state after:
case inl
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
val✝ : α
h : l.idxFun (eι.symm i) = Sum.inl val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

case inr
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
val✝ : η
h : l.idxFun (eι.symm i) = Sum.inr val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
rintro l m hlm

Goal state after:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
⊢ l = m
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D

Tactic:
exact ⟨h, hX⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ (M ＼ D).loops = M.loops \ D

Tactic:
by
  simp [loops]

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

Goal state before:
pp: α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)

Tactic:
by rw [contract_delete_contract_delete']

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
he : M.IsLoop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.IsLoop e

Tactic:
rw [← singleton_dep] at he ⊢

Goal state after:
α : Type u_1
M N : Matroid α
e : α
he : M.Dep {e}
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Dep {e}
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Tactic:
obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η
  refine ⟨Fintype.card ι, fun C ↦ ?_⟩
  obtain ⟨l, c, cl⟩ := hι fun v ↦ C (v ∘ (Fintype.equivFin _).symm)
  refine ⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩
  obtain ⟨i, hi⟩ := l.proper e
  use Fintype.equivFin _ i
  simpa using hi

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
⊢ M.closure (X ∪ C) = M.E

Tactic:
rwa [← union_sdiff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_sdiff_cancel]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
wlog hKi : M.Indep K generalizing K with aux

Goal state after:
case inr
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Module: Mathlib.Combinatorics.Matroid.Sum

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

Tactic:
by
  simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm,
    Equiv.sumCongr_apply, Equiv.symm_symm, sigma_isBasis_iff, Bool.forall_bool,
    Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]
  convert! Iff.rfl <;> exact ext <| by simp

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∑ i_1 ∈ S, m.degree (X i - C i_1) = single i #S

Tactic:
simp [Finset.sum_congr rfl (fun r _ ↦ m.degree_X_sub_C i r)]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j

Tactic:
mapDomain_of_notMem_range,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ 0 = (single i (e ())) j

case neg.h
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ j ∉ Set.range fun x ↦ i
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
i j : V
e : i ⟶ j
⊢ e.toPath.vertices = [i, j]

Tactic:
change (Path.nil.cons e).vertices = [i, j]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (image (fun x ↦ x.erase a) 𝒜) = ∅

Tactic:
simp [eq_empty_iff_forall_notMem,
    (ne_of_mem_of_not_mem' (mem_insert_self _ _) (notMem_erase _ _)).symm]

Goal state after:
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:
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.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this✝ : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
this : n.pred.succ ≤ n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m

Tactic:
Nat.succ_pred hn.ne'

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this✝ : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
this : n ≤ n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: 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
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ #(Ioo 0 n) < n

Tactic:
simp [Nat.card_Ioo, n]

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
hab

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((b ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a : α
ha : a ∈ ↑({a ∈ s | compress u v a ∉ s})
b : α
hb : b ∈ ↑({a ∈ s | compress u v a ∉ s})
⊢ compress u v a = compress u v b → a = b

Tactic:
hab

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
a : α
ha : a ∈ ↑({a ∈ s | compress u v a ∉ s})
b : α
hb : b ∈ ↑({a ∈ s | compress u v a ∉ s})
hab : compress u v a = compress u v b
⊢ a = b
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
⊢ ∀ (x : α),
    (∀ y < x, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) → ∃ s, s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
rintro a ih

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
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 α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v a

Tactic:
rw [← hba]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
simp_rw [← add_div, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : 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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
⊢ insert y s = ((insert x s).erase x ∪ v.erase x) \ v.erase y

Tactic:
erase_insert ‹x ∉ s›,

Goal state after:
α : 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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
⊢ insert y s = (s ∪ v.erase x) \ v.erase y
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

Tactic:
←
    card_sdiff_of_subset inter_subset_right,

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

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

Tactic:
hab

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

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

pp: case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

pp: case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
←
    card_sdiff_of_subset inter_subset_right,

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

case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ
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
⊢ 2 * #s = Fintype.card α

Tactic:
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
      rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]

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
⊢ s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯ = Finset.univ