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 : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ w.orthogonal (v.cross w)

Tactic:
orthogonal_comm

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: 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
this : #s + Fintype.card L ≤ #(s.biUnion t) + Fintype.card L
⊢ #s ≤ #(s.biUnion t)

Tactic:
add_le_add_iff_right

Goal state after:
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
this : #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(derangements (Subtype p)) ≃ { f // ∀ a ∈ fixedPoints ⇑↑f, ¬p a }

Tactic:
refine (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => ?_, ?_⟩

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
⊢ False

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.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
⊢ #univ • ∑ x, lineCount L x = #univ • ∑ x, pointCount P x

Tactic:
Finset.card_univ,

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
⊢ Fintype.card L • ∑ x, lineCount L x = Fintype.card P • ∑ x, pointCount P x
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 : t ∈ x •> A ∩ y •> A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
simp only [mem_inter, mem_smul_finset, smul_eq_mul] at 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
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
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
⊢ 1 < order P L

Tactic:
cases nonempty_fintype { p : P // p ∈ l₂ }

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ 1 < order P L
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)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
mul_smul_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
← Finset.prod_erase_mul _ _ hm

Goal state after:
case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
← Finset.prod_erase_mul _ _ hm

Goal state after:
case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    (∏ x ∈ m.toFinset.erase 0, (x * count x m)!) * (0 * count 0 m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑(p + 0) = ↑p

Tactic:
exact append_nil _

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

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

Tactic:
· rw [← Nat.pos_iff_ne_zero]
    exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity)

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ zeta 𝕜 * mu 𝕜 = 1

Tactic:
by
  rw [mu_eq_mu', zeta_mul_mu']

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (p + q).outsidePart = p.outsidePart + q

Tactic:
simp_rw [outsidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
    DyckWord.ext_iff, drop]
  exact drop_append_of_le_length (firstReturn_lt_length h)

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Tactic:
← congrArg semilength (nest_insidePart_add_outsidePart h),

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

Goal state before:
pp: p : DyckWord
⊢ 0 < p ↔ p ≠ 0

Tactic:
by
  rw [ne_comm, iff_comm, ne_iff_lt_iff_le]
  exact DyckWord.zero_le p

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

Goal state before:
pp: ⊢ (ofTree BinaryTree.nil).toTree = BinaryTree.nil

Tactic:
by simp [ofTree, toTree]

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
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ #(A * S) ≤ t * #S

Tactic:
card_mul_le,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ #A * #S ≤ t * #S
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

Tactic:
simp only [deleteVerts, induce_isLink, mem_sdiff, and_congr_right_iff]
  exact fun h ↦ by simp [h.left_mem, h.right_mem]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
⊢ ↑(diagonal α ι) x = fun x_1 ↦ x

Tactic:
ext; simp [diagonal]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_4
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)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)

Tactic:
filter_upwards [hU n] with m hm

Goal state after:
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)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
⊢ ∃ a, FP a ⊆ s₀

Tactic:
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some

Goal state after:
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
⊢ ∃ a, FP a ⊆ s₀
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.some
α : 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
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
val✝ : α
⊢ C' (↑p.line (some val✝)) = p.color

Tactic:
apply p.has_color

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

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ #(prefixed s) = (#s)! * (Fintype.card X - #s)!

Tactic:
by
  simpa [-mem_prefixed] using Fintype.card_congr (prefixedEquiv s)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff,
    subset_sdiff, ← and_assoc, and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual,
    dual_dual, union_comm, dual_ground, union_subset_iff, and_iff_right hI.subset_ground,
    and_congr_left_iff, ← isBase_restrict_iff, sdiff_sdiff, Spanning.isBase_restrict_iff,
    and_iff_left (sdiff_subset_sdiff_right subset_union_left)]
  · simp
  rwa [← dual_ground, ← coindep_iff_compl_spanning, dual_coindep_iff]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
⊢ ∃ a b, (⟨a, b⟩ ∈ B₂ ∧ ⟨a, b⟩ ∉ B₁) ∧ ∀ (i_1 : ι), (M i_1).IsBase (Sigma.mk i_1 ⁻¹' insert ⟨a, b⟩ (B₁ \ {⟨i, e⟩}))

Tactic:
refine ⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' insert ⟨i, f⟩ (B₁ \ {⟨i, e⟩}))
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
simpa using hi

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : ¬(Disjoint X C ∧ M.Indep (C ∪ X)) ∧ X ⊆ (M ／ C).E
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False

Tactic:
and_iff_left hi

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_4
ι : 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✝ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
⊢ ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t

Tactic:
refine fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i,x⟩ hx ↦ ?_

Goal state after:
case refine_4
ι : 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✝¹ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
J : Set ((i : ι) × α i)
hJ : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
hJX : J ⊆ X
hIJ : I ⊆ J
x✝ : (i : ι) × α i
i : ι
x : α i
hx : ⟨i, x⟩ ∈ J
⊢ ⟨i, x⟩ ∈ I
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)

Tactic:
rcases hp : shortestPath r b with (_ | ⟨p, e⟩)

Goal state after:
case nil
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
hp : shortestPath r r = Path.nil
⊢ r = r ∨ ∃ a, Nonempty (a ⟶ r)

case cons
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
b✝ : V
p : Path r b✝
e : b✝ ⟶ b
hp : shortestPath r b = p.cons e
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
Module: Mathlib.Combinatorics.Nullstellensatz

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

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:
· rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]

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
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
ext ⟨v, f | g⟩ <;>
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyCostar]`
    simp only [Quiver.symmetrifyCostar, Function.comp_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inl f⟩)

case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj (φ.obj u)) (Hom (Symmetrify.of.obj (φ.obj u))))
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.costar u) (φ.star u)
      ((Equiv.sigmaSumDistrib (fun u_1 ↦ u_1 ⟶ Symmetrify.of.obj u) (Hom (Symmetrify.of.obj u))) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity (Set.ofPred Odd) = 2⁻¹

Tactic:
simp only [h]

Goal state after:
h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity {n | n % 2 = 1} = 2⁻¹
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ {a ∈ s | compress u v a ∈ s} ∪ {a ∈ image (compress u v) s | a ∉ s} ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
mem_union,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ {a ∈ s | compress u v a ∈ s} ∨ a ∈ {a ∈ image (compress u v) s | a ∉ s} ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ InfIrred s ↔ ∃ a, Ici a = s

Tactic:
by
  refine ⟨fun hs ↦ ?_, ?_⟩
  · obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal (coe_nonempty.2 hs.ne_top)
    exact ⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left
      (lt_erase.2 ha).ne'⟩
  · rintro ⟨a, rfl⟩
    exact infIrred_Ici _

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

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

Tactic:
by
  induction k generalizing 𝒜 s with
  | zero =>
    refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
    rintro ⟨t, ht, hst, hcard⟩
    rwa [← eq_of_subset_of_card_le hst hcard.ge]
  | succ k ih =>
    simp only [Function.comp_apply, Function.iterate_succ]
    refine ih.trans ?_
    clear ih
    constructor
    · rintro ⟨t, ht, hts, hcardst⟩
      obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
      refine ⟨u, hu, hut.trans hts, ?_⟩
      rw [← hcardst, hcardtu, add_right_comm]
      rfl
    · rintro ⟨t, ht, hts, hcard⟩
      obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
      refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
      rw [hu, ← hcard, add_right_comm]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ
hm : m = #𝒜
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
induction m using Nat.strongRecOn generalizing 𝒜 with | ind m ih => _

Goal state after:
case ind
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
ih :
  ∀ m_1 < m,
    ∀ {𝒜 : Finset (Finset α)}, 𝒜.Nonempty → univ ∉ 𝒜 → m_1 = #𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
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
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s

Tactic:
mem_union,

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
a : α
⊢ a ∈ ↑s ∨ a ∈ compl ⁻¹' ↑s
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
mem_union,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∨ s ∈ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Tactic:
constructor
  · rintro ⟨h⟩
    induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
  · intro h
    induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Goal state after: