mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ (mk F v hv).cross (mk F w hw) = mk F v hv

Tactic:
by
  rw [cross_mk, dif_pos h]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ Injective fun s ↦ ∑ i ∈ s, n ^ i

Tactic:
by
  intro _ _ h
  rwa [le_antisymm_iff, geomSum_le_geomSum_iff_toColex_le_toColex hn,
    geomSum_le_geomSum_iff_toColex_le_toColex hn, ← le_antisymm_iff] at h

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

pp: case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
· simp [pointCount]

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ Fintype.card ↑{p | p ∈ l} • lineCount L (f l) = Fintype.card ↑{l_1 | f l ∈ l_1} • lineCount L (f l)

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ Nat.card ↑{p | p ∈ l} • lineCount L (f l) = Nat.card ↑{l_1 | f l ∈ l_1} • lineCount L (f l)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {l₁ l₂ : ℙ K (Fin 3 → K)} → l₁ ≠ l₂ → ℙ K (Fin 3 → K)

Tactic:
intro v w _
      exact cross v w

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {p₁ p₂ : ℙ K (Fin 3 → K)} → p₁ ≠ p₂ → ℙ K (Fin 3 → K)

Tactic:
intro v w _
      exact cross v w

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

Goal state before:
pp: m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity)

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

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq : count D [U] + count D (List.drop 1 (List.take j ↑p)) < count U [U] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
simp only [count_singleton', ite_true] at eq

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq : (if U = D then 1 else 0) + count D (List.drop 1 (List.take j ↑p)) < 1 + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case hi
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case hj
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case left_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case right_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case h
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

Tactic:
rw! [← p.cons_tail_dropLast_concat h]

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide
          (count U (List.take (0 + 1) (U :: (↑p).dropLast.tail ++ [D])) =
            count D (List.take (0 + 1) (U :: (↑p).dropLast.tail ++ [D]))) =
        true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U
                (List.take ((range (U :: (↑p).dropLast.tail ++ [D]).length)[j] + 1) (U :: (↑p).dropLast.tail ++ [D])) =
              count D
                (List.take ((range (U :: (↑p).dropLast.tail ++ [D]).length)[j] + 1) (U :: (↑p).dropLast.tail ++ [D]))) =
          false)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ n.succ * p.parts.bell = (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell

Tactic:
succ_eq_add_one,

Goal state after:
n : ℕ
p : (n + 1).Partition
⊢ (n + 1) * p.parts.bell = (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
p : (n + 1).Partition
a✝ : p ∈ Finset.univ
⊢ ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = p.parts.bell

Tactic:
rw [bell_eq_sum_erase p]

Goal state after:
case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
p : (n + 1).Partition
a✝ : p ∈ Finset.univ
⊢ ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case hi
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun z ↦ Icc x z

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case hj
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun y ↦ Ici y

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case left_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case right_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case h
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (if a.fst ≤ a.snd then (mu 𝕜) x a.fst * f a.snd else 0) =
      if
          (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd ≤
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst then
        (mu 𝕜) x
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd *
          f
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst
      else 0

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K ≤ 1
hS : S.Nonempty
r : ℝ
⊢ r ≤ connectivity K S ↔ ∀ ⦃A : Finset G⦄, A.Nonempty → r ≤ expansion K S A

Tactic:
by
  have : Nonempty {A : Finset G // A.Nonempty} := ⟨{1}, by simp⟩
  simp [connectivity, le_ciInf_iff, bddBelow_expansion, *]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K ≤ 1
hS : S.Nonempty
r : ℝ
this : Nonempty { A // A.Nonempty }
⊢ connectivity K S < r ↔ ∃ A, A.Nonempty ∧ expansion K S A < r

Tactic:
simp [connectivity, ciInf_lt_iff, bddBelow_expansion, *]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: n : ℕ
⊢ #(restricted n fun x ↦ ¬2 ∣ x) = #(countRestricted n 2)

Tactic:
exact card_restricted_eq_card_countRestricted n (by norm_num)

Goal state after:
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) ∘ Neg.neg) (pentagonalSeries R)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    ↑↑(-↑k).negOnePow * X ^ pentagonal (-↑k) + ↑↑(↑k + 1).negOnePow * X ^ pentagonal (↑k + 1)

Tactic:
Int.negOnePow_add

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)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    ↑↑(-↑k).negOnePow * X ^ pentagonal (-↑k) + ↑↑((↑k).negOnePow * Int.negOnePow 1) * X ^ pentagonal (↑k + 1)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
⊢ E(H) ⊆ E(G)

Tactic:
intro e

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
⊢ e ∈ E(H) → e ∈ E(G)
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)

Tactic:
inter_comm F₁ᶜ,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

Tactic:
simp only [Inc, banana_isLink, exists_and_left, and_congr_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ e ∈ edgeSet → ((∃ x_1, x = u ∧ x_1 = v ∨ x = v ∧ x_1 = u) ↔ x = u ∨ x = v)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ B ⊆ M.E \ D

Tactic:
simp [subset_sdiff, h.1.subset_ground, h.2]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ a.get i ∈ FP a

Tactic:
induction i generalizing a with

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:
rw [← dual_delete_dual, dual_dual]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_5
α : 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
⊢ {
          lines :=
            { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
              Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines,
          focus := Sum.elim s.focus (↑(map some l') none), is_focused := ⋯, distinct_colors := ⋯ }.lines.card =
    r + 1

Tactic:
rw [Multiset.card_cons, Multiset.card_map, sr]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
⊢ ∃ B, (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) ∧ I ⊆ B

Tactic:
choose Bs hBs using fun i ↦ (h i).exists_isBase_superset

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
⊢ ∃ B, (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) ∧ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ∪ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I

Tactic:
rw [union_subset_iff] at hKJ

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
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
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
⊢ ∀ (b : σ →₀ ℕ), ¬coeff b (Q.coeff m) = 0 → b i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
intro e

Goal state after:
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
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
⊢ ¬coeff e (Q.coeff m) = 0 → e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: 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)

pp: 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)

Tactic:
· exact ⟨Path.nil⟩

Goal state after:
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.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
⊢ ∀ (a : Path r b), a = default

Tactic:
have height_le : ∀ {a b}, Path a b → height a ≤ height b := by
        intro a b p
        induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))

Goal state after:
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
⊢ ∀ (a : Path r b), a = default
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case hlt
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
· obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ Function.LeftInverse
    (fun x_1 ↦
      match x_1 with
      | ⟨fst, s⟩ => ⟨(ι s)⁻¹ • x, ⟨s, ⋯⟩⟩)
    ((labelling V ι).costar x)

Tactic:
rintro ⟨v, s, hs⟩
    simp only [Prefunctor.costar_apply, labelling_map]
    have : (ι s)⁻¹ • x = v := by rw [← hs, inv_smul_smul]
    subst this; rfl

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

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

Tactic:
· rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
    exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ 1 - 1 / ↑k

Tactic:
one_sub_div (Nat.cast_pos.2 hk').ne'

Goal state after:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ (↑k - 1) / ↑k
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
h : a ∉ upperClosure ↑s
⊢ ⊥ ≤ a

Tactic:
· exact bot_le

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t

Tactic:
· rintro ⟨v, hv, w, hw, rfl⟩
    exact inter_subset_inter hv hw

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

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
⊢ sᶜˢᶜˢ = s

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s t : Finset α
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ

Tactic:
by rw [← compls_subset_compls, compls_compls]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
⊢ univᶜˢ = univ

Tactic:
ext; simp

Goal state after: