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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Finset α) → (a : ↥s) → β ↑a
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g t (Set.inclusion hst x)

Tactic:
have (a : α) : Nonempty (β a) := ⟨g {a} ⟨a, by simp⟩⟩
  let g' (s) (a : α) : β a := if ha : a ∈ s then g s ⟨a, ha⟩ else Classical.arbitrary (β a)
  have hg (s : Finset α) (x : s) : g s x = g' s x := by simp [g']
  simpa [hg] using Finset.rado_selection g'

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

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

Tactic:
obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)

Goal state after:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum
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
⊢ FiniteDimensional K ↥v.submodule

Tactic:
by
  rw [← v.mk_rep]
  change FiniteDimensional K (K ∙ v.rep)
  infer_instance

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 : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
⊢ v ⬝ᵥ w = 0

Tactic:
h,

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
⊢ v ⬝ᵥ 0 = 0
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : #s = 1
⊢ #s ≤ #(s.biUnion t)

Tactic:
obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
      obtain ⟨p, hl⟩ := exists_point (P := P) l
      rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
      exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f ↔ fixedPoints ⇑f = {a}

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ fixedPoints ⇑f = ∅

Tactic:
· rw [Set.eq_singleton_iff_unique_mem, and_comm]
        rfl

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ fixedPoints ⇑f = ∅
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : some ((removeNone F) x) = some x
⊢ x ∈ {a}

Tactic:
rcases Fx : F (some x) with - | y

Goal state after:
case mp.none
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : some ((removeNone F) x) = some x
Fx : F (some x) = none
⊢ x ∈ {a}

case mp.some
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : some ((removeNone F) x) = some x
y : α
Fx : F (some x) = some y
⊢ x ∈ {a}
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
simp_rw [Equiv.RemoveNone.fiber_some]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}} ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x)) / ↑n.factorial = (-1) ^ x / ↑x.factorial

Tactic:
intro k

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
⊢ k ∈ Finset.range (n + 1) → (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : (∃ y ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
obtain ⟨⟨z, hz, hzxwy⟩, w, hw, rfl⟩ := ht

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p + 0 = p

Tactic:
by ext1; exact append_nil _

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

Goal state before:
pp: case cons.nil
s : DyckStep
count_U_eq_count_D✝ : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

Tactic:
rename_i bal _
      cases s <;> simp at bal

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a

Tactic:
by
  refine subset_antisymm ?_ ?_
  · rw [subset_smul_finset_iff, ← op_inv]
    calc
      a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
  · rw [subset_smul_finset_iff]
    calc
      a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
      _ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by grw [op_smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
i : ℕ
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)

Tactic:
replace h := toList_ne_nil.mpr hn.1

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
this : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
⊢ ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
by
    calc
          (#Z : ℝ)
      _ = (Fintype.card H / #S : ℝ)⁻¹ := by simp [← card_H_mul_card_Z]
      _ ≤ (((φ - K) * (K - ψ) / ((2 - K) * K) * #S) / #S)⁻¹ := by gcongr
      _ = (2 - K) * K / ((φ - K) * (K - ψ)) := by
        have : (#S : ℝ) ≠ 0 := by positivity
        simp [this]

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

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

Tactic:
h,

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

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

Tactic:
h,

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

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

Tactic:
h,

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (zeta 𝕜).prod (zeta 𝕜) = zeta 𝕜

Tactic:
ext x y hxy; simp [hxy, hxy.1, hxy.2]

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

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (if p = 0 then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p

Tactic:
h,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (if False then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ (if p = 0 then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength

Tactic:
h,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ (if False then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.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:
simp_rw [aux, Finset.prod_range_succ, powMulProdOneSubPow]

Goal state after:
R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)) +
      x ^ (3 * k + 5) * (x ^ ((k + 1 + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + 1 + i + 1))) =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) *
        ((∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))) * (1 - x ^ (k + n + 2))) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
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
⊢ ∃ H x, IsAtom K S (↑H).toFinset

Tactic:
obtain ⟨N, hN⟩ := exists_isAtom hK hS

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
⊢ ∃ H x, IsAtom K S (↑H).toFinset
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
⊢ E(G) = ∅

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
⊢ E(noEdge V(G) β) = ∅
Module: Mathlib.Combinatorics.Hindman

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

Tactic:
apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
    · intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _
    · intro n
      exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
    · exact (ultrafilter_isClosed_basic _).isCompact
    · intro n
      apply ultrafilter_isClosed_basic

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ s.lines.card ≤ Fintype.card κ

Tactic:
← Multiset.card_map,

Goal state after:
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ (Multiset.map ?f s.lines).card ≤ Fintype.card κ

case f
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ AlmostMono C → ?m.268

α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ Type ?u.156
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inl
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
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
h,

Goal state after:
case H.inl
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
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ ∅, a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: 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ᶜ
x : X
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x

Tactic:
by
        by_cases hx : x ∈ s
        · have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
          simp [hx, this]
        · simp [hx]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ C).IsBasis (I \ C) (X \ C)

Tactic:
rw [hJC.contract_eq_contract_delete, delete_isBasis_iff]

Goal state after:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v ↦ C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ ∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e

Tactic:
use Fintype.equivFin _ i

Goal state after:
case h
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v ↦ C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) ((Fintype.equivFin ι) i) = Sum.inr e
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ I₀ ⊆ Sigma.mk i ⁻¹' I

Tactic:
h,

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ I₀ ⊆ Sigma.mk i ⁻¹' (I ∪ Sigma.mk i '' I₀)

case refine_1
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ ∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)
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
⊢ C ∪ M.closure (X ∪ C) \ C = M.E

Tactic:
h,

Goal state after:
α : 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
⊢ C ∪ M.E \ C = M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
⊢ M.Spanning (X \ C ∪ C ∩ M.E)

Tactic:
exact hX.superset (by tauto_set) (by tauto_set)

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

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

Tactic:
h,

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a : V
⊢ {v | v ∈ nil.vertices} = {a}

Tactic:
simp only [vertices_nil, mem_singleton, Set.ext_iff, Set.mem_singleton_iff]

Goal state after:
V : Type u_1
inst✝ : Quiver V
a : V
⊢ ∀ (x : V), x ∈ {v | v = a} ↔ x = a
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ a ∈ p.vertices

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

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

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

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

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

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

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

Goal state after:
Module: Mathlib.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:
compression,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ {s ∈ 𝒜 | s.erase a ∈ 𝒜}.disjUnion ({s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜}) ⋯ ↔
    s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(𝓓 a 𝒜) = #𝒜

Tactic:
compression,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜}.disjUnion ({s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜}) ⋯) = #𝒜