mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ ↑n < Fintype.card X - #s

Tactic:
by

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
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ (Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩ ∈ sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ N.E ⊆ M.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M = M ／ ∅ ＼ ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M₁ M₂ M₃ : Matroid α
h : M₁ ≤m M₂
h' : M₂ ≤m M₃
⊢ M₁ ≤m M₃

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
⊢ M = N

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
x✝ : N ≤m M ∧ N.E ⊂ M.E
h : N ≤m M
hss : N.E ⊂ M.E
h' : M ≤m N
⊢ N.E = M.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
I : Set α
hI : N.Indep I
hNM : N ≤m M
⊢ M.Indep I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤m M
⊢ M.IsNonloop e

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
f : ↥(prefixed s)
⊢ Function.LeftInverse (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩

Tactic:
by

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
f : ↥(prefixed s)
⊢ Function.RightInverse (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩

Tactic:
by

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
hx : x ∉ s
⊢ x ∈ sᶜ

Tactic:
by

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
hx : x ∉ s
⊢ Fintype.card ↥sᶜ + #s = Fintype.card X

Tactic:
by

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ᶜ
n : Fin (Fintype.card X)
hn : ↑n < #s
⊢ ↑n < Fintype.card ↥s

Tactic:
by

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ᶜ
n : Fin (Fintype.card X)
hn : ¬↑n < #s
⊢ ↑n - #s < Fintype.card ↥sᶜ

Tactic:
by

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
hx : x ∈ s
⊢ ↑(g ⟨x, hx⟩) < #s

Tactic:
by

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

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ᶜ
n : Fin (Fintype.card X)
⊢ (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:
by

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:
by

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:
by

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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₂ ／ C₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ／ X ＼ Y)✶ = M✶ ＼ X ／ Y

Tactic:
by

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
⊢ x ∈ s ↔
    ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ＼ X ／ Y)✶ = M✶ ／ X ＼ Y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ C = M ↔ Disjoint C M.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ e ∉ M✶.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M ／ {e} = M

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ／ ∅ = M

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

Tactic:
by

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
f : ↥(prefixed s)
⊢ (fun x ↦
        match x with
        | (g, g') =>
          ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
              invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
              left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
      ((fun f ↦
          ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ },
            { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }))
        f) =
    f

Tactic:
by

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
g : Numbering ↥s × Numbering ↥sᶜ
⊢ (fun f ↦
        ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ },
          { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }))
      ((fun x ↦
          match x with
          | (g, g') =>
            ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
                invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
                left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
        g) =
    g

Tactic:
by

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

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).dens = (↑((Fintype.card X).choose #s))⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
⊢ Disjoint (prefixed s) (prefixed t)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
⊢ Disjoint (prefixed s) (prefixed t)

Tactic:
by
  simp only [Finset.disjoint_left, mem_prefixed]
  intro f hs ht
  obtain hst' | hts' := Nat.le_total #s #t
  · exact hst <| hs.subset_of_card_le_card ht hst'
  · exact hts <| ht.subset_of_card_le_card hs hts'

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f)

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ m.subLTerm f ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
x✝ : Disjoint J I ∧ ∃ B, M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.IsBase (B \ I ∪ I)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) < m.toSyn (m.degree f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsNonloop e
⊢ (M ／ {e}).Indep I ↔ e ∉ I ∧ M.Indep (insert e I)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ (M ／ I).Indep (J \ I)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ Disjoint {e} I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ (M✶ ＼ I).coloops

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M ／ X = M ／ I ＼ (X \ I)

Tactic:
by

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)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk i ⁻¹' I ⊆ Bs i
i : ι
⊢ (M i).IsBase (Sigma.mk i ⁻¹' univ.sigma Bs)

Tactic:
by

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)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) ↔ ∃ B, (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) ∧ I ⊆ B

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B : (i : ι) → Set (α i)
hB : ∀ (i : ι), (M i).IsBase (B i)
⊢ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' univ.sigma B)

Tactic:
by

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

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

Tactic:
by

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₂
⊢ e ∉ Sigma.mk i ⁻¹' B₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) (m.reduce hb f) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: ⊢ ∀ {α : Type u} [Fintype α],
    (∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) →
      ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift.{u, v} κ
hc : ∀ (x : α), (ULift.up ∘ C) (↑l x) = c
x : α
⊢ C (↑l x) = c.down

Tactic:
by

Goal state after:
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 ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ M.Indep (K \ I ∪ I)

Tactic:
by

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₁
j : ι
hne : i ≠ j
⊢ ⟨i, e⟩ ∉ range (Sigma.mk j)

Tactic:
by

Goal state after:
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 ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ K ⊆ I ∪ X

Tactic:
by

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₁
j : ι
hne : i ≠ j
⊢ ⟨i, f⟩ ∉ range (Sigma.mk j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : (M ／ I).IsBasis J X
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
this : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
by

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₂
⊢ ∀ a ∈ B₁ \ B₂, ∃ b ∈ B₂ \ B₁, (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) (insert b (B₁ \ {a}))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.reduce hb f)) < m.toSyn (m.degree f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
K : Set α
hJK : Disjoint K J
hKJi : M.Indep (K ∪ J)
hKX : K ⊆ X
hIJK : I ⊆ K ∪ J
⊢ K ⊆ I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) X

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) ((X ∩ M.E) \ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
inter_eq_self_of_subset_left hIX.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) (X \ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ (M ／ I).IsBasis (J \ I) (Y \ X)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis' (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis' J X

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis J X

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ X = M ／ I ＼ (X \ I)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
by

Goal state after: