mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
· exact div_mul_cancel₀ _ (by positivity)

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
· exact div_mul_cancel₀ _ (by positivity)

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ False

Tactic:
exact hx₁x₂ <| by simpa using this.symm

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ False

Tactic:
have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
    rintro a ha
    have := hAn ha
    simp at this
    lia

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
this : ↑A = Fin.val '' Nat.cast '' ↑A
⊢ False
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : ((a₁ * c₁, a₁ * b₁), b₁, c₁) = ((a₂ * c₂, a₂ * b₂), b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Tactic:
Prod.ext_iff

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: 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 := ⋯ }
⊢ ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j = a ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
Equiv.subtypeEquivCodomain_symm_apply_eq

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 ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j = a ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: n : ℕ
⊢ (2 * n).bitIndices = map (fun x ↦ x + 1) n.bitIndices

Tactic:
← bitIndices_bit_false,

Goal state after:
n : ℕ
⊢ (2 * n).bitIndices = (bit false n).bitIndices
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ (∃ s, #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
⊢ ∀ (a : α), f a ≠ a ↔ (e.permCongr f) (e a) ≠ e a

Tactic:
by
    intro b; simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ False

Tactic:
refine hf ⟨a, ha⟩ (Subtype.ext ?_)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ False

pp: case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
⊢ (∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a) → f ∈ derangements (Subtype p)

Tactic:
· refine hf ⟨a, ha⟩ (Subtype.ext ?_)
        simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
        Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
        assumption

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
⊢ (∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a) → f ∈ derangements (Subtype p)
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
apply HasSum.tendsto_sum_nat

Goal state after:
s : ℕ → ℝ := ⋯
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i ↦ (-1) ^ i / ↑i.factorial) (Real.exp (-1))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ count U ↑p + p.semilength = (↑p).length

Tactic:
p.count_U_eq_count_D,

Goal state after:
p : DyckWord
⊢ count D ↑p + p.semilength = (↑p).length
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ ((algebraMap 𝕜 𝕝) c + (algebraMap 𝕜 𝕝) d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
add_smul

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' + count U ↑p = count D r' + count D ↑p
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
p.count_U_eq_count_D,

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' + count D ↑p = count D r' + count D ↑p
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
rcases mq with hm | hm

Goal state after:
case tail.inr.inl
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ powMulProdOneSubPow k n x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) n x = aux k (n + 1) x - aux k n x

Tactic:
aux,

Goal state after:
R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ powMulProdOneSubPow k n x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) n x =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 2)) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) * ∏' (i : ℕ), (1 - X ^ (i + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)]

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ ∏' (b : ℕ), (if ¬m ∣ b + 1 then ∑' (j : ℕ), X ^ ((b + 1) * j) else 1) * (1 - X ^ (b + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2

Tactic:
stirlingSecond_self,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
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)
⊢ K * ↑(#(↑H).toFinset) + ex (↑H).toFinset ≤ K * ↑(#(↑H).toFinset) + (1 - ε / 2) * ↑(#((↑H).toFinset * S))

Tactic:
by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : z ≠ y
hy : G.IsLink e y z
⊢ False

Tactic:
rw [← h.eq_of_inc hy.inc_left, ← h.eq_of_inc hy.inc_right] at hyz

Goal state after:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : x ≠ x
hy : G.IsLink e y z
⊢ False
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case h
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 = m

Tactic:
have absorbing_eq_self : N ∩ { m' | m' * m = m } = N := by
      apply hN.eq_of_subset
      · refine ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_const_mul m)), ?_, ?_⟩
        · rwa [← scaling_eq_self] at hm
        · rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
          refine ⟨N_mul _ mem'' _ mem', ?_⟩
          rw [Set.mem_ofPred_eq, mul_assoc, eq', eq'']
      apply Set.inter_subset_left

Goal state after:
case h
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
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
⊢ ∃ m ∈ s, m * m = m

Tactic:
by
  let M' := { m // m ∈ s }
  let : Semigroup M' :=
    { mul := fun p q => ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩
      mul_assoc := fun p q r => Subtype.ext (mul_assoc _ _ _) }
  have : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
  have : Nonempty M' := nonempty_subtype.mpr snemp
  have : ∀ p : M', Continuous (· * p) := fun p =>
    ((continuous_const_mul p.1).comp continuous_subtype_val).subtype_mk _
  obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
  exact ⟨m, hm, Subtype.ext_iff.mp idem⟩

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.ht0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}

Tactic:
exact (ultrafilter_isClosed_basic _).isCompact

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

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

Tactic:
rw [← restrict_compl, ← restrict_compl, sdiff_inter_self_eq_sdiff]

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

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

Tactic:
by
  rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  apply_fun (M.E \ Matroid.E ·) at h
  simp_rw [delete_ground, sdiff_sdiff_cancel_left inter_subset_right] at h
  assumption

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

pp: case inr
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)
hsn : #s ≤ ↑n
⊢ (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:
case inr
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)
hsn : #s ≤ ↑n
⊢ (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
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js

Tactic:
· rw [← univ_sigma_preimage_mk X]
      exact sigma_mono rfl.subset fun i ↦ (hJs i).1.subset

Goal state after:
case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
⊢ (M ／ C).Finitary

Tactic:
hJ.contract_eq_contract_delete

Goal state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
⊢ (M ／ J ＼ (C \ J)).Finitary
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv
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
⊢ (rename ⇑e.symm) P = 0

Tactic:
apply h _ (fun i ↦ S (e i))

Goal state after:
case of_equiv.Hdeg
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
⊢ ∀ (i : σ), degreeOf i ((rename ⇑e.symm) P) < #(S (e i))

case of_equiv.Heval
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
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (e i)) → (eval x) ((rename ⇑e.symm) P) = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ C \ K ⊂ C

Tactic:
by rwa [sdiff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]

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

Goal state before:
pp: case succ
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)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < n + 1
⊢ Nonempty (Path r b)

Tactic:
rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)

Goal state after:
case succ.inl
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)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
hn : height r < n + 1
⊢ Nonempty (Path r r)

case succ.inr
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)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < n + 1
a : V
e : a ⟶ b
⊢ Nonempty (Path r b)
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
by
  simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := s ∉ 𝒜)]
  refine
    or_congr_right
      (and_congr_left fun hs =>
        ⟨?_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)
  rintro ⟨t, ht, rfl⟩
  rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]

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}
⊢ n ≤ (n - 1) / m * m + m

Tactic:
have := @Nat.lt_div_mul_add n.pred m hm'

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.pred < n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
left✝ : compress u v b ∉ s
⊢ compress u v (compress u v b) ∈ s ∧ compress u v (compress u v b) ∈ s ∨
    compress u v (compress u v b) ∉ s ∧ ∃ b_1 ∈ s, compress u v b_1 = compress u v (compress u v b)

Tactic:
exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
clear ih

Goal state after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s