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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
⊢ (Matroid.disjointSigma M h).E = ⋃ i, (M i).E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
I : Set α
⊢ (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
B : Set α
⊢ (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
I X : Set α
⊢ (Matroid.disjointSigma M h).IsBasis I X ↔
    (∀ (i : ι), (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
⊢ (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ C ⊆ M.E \ D

Tactic:
by

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

Goal state before:
pp: α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
by

Goal state after:
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
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ Polynomial.map (eval x) Q = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : σ →₀ ℕ
this : Q.coeff m = 0
⊢ coeff d (Q.coeff m) = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' I ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : α),
    x ∈ Sum.inl ⁻¹' X ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X

Tactic:
by

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

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

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
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
this :
  ∃ g' r',
    m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' I ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' X ↔
      x ∈
        (fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X

Tactic:
by

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

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.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ (M.sum N).IsBasis I X ↔ M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

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
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
hf'0 : m.subLTerm f = 0
⊢ m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) 0 + 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ (M.disjointSum N h).E = M.E ∪ N.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
⊢ (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

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
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
hf'0 : m.subLTerm f = 0
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
⊢ (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I X : Set α
⊢ (M.disjointSum N h).IsBasis I X ↔
    M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
⊢ M ＼ D ／ C ＼ D' = M ／ C ＼ (D ∪ D')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ M.disjointSum N h = N.disjointSum M ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
⊢ r 0 ≠ r 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : (M.disjointSum N h).IsBase B
⊢ ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Tactic:
by

Goal state after:
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 : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
hQ,

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 : σ →₀ ℕ
he : ¬coeff e (((optionEquivLeft R σ) P).coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ : f ![a, b] = f ![(fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0, (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1
⊢ (List.ofFn ![a, b]).Perm (List.ofFn ![b, a])

Tactic:
by

Goal state after:
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
⊢ Nonempty (Path r b)

Tactic:
by

Goal state after:
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 b : V} (a_1 : Path a b), height a ≤ height b

Tactic:
by

Goal state after:
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
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
this : ∀ (p q : Path r b), p = q
⊢ ∀ (a : Path r b), a = default

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
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] < f r

Tactic:
by

Goal state after:
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:
by

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)⦄ (a_1 : a ⟶ b),
    (shortestPath r a).length < (shortestPath r b).length

Tactic:
by

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 c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: 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
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ (fun i ↦ g (swap ![![a, b], ![b, a]] i)) ∈ ω.tt ![![a, b], ![b, a]]

Tactic:
by

Goal state after:
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
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

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

Goal state after:
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
g : (Fin 2 → D) → D
h✝ : g ∈ ω
this : (fun i ↦ g (swap ![![a, b], ![b, a]] i)) ∈ ω.tt ![![a, b], ![b, a]]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
⊢ IsStronglyConnected V

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v) ↔
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
⊢ IsStronglyConnected (Symmetrify V)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: 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
⊢ (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path i i₀
p₂ : Path j₀ j
p : Path i j := p₁.comp (e₀.toPath.comp p₂)
⊢ 0 < p.length

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
⊢ IsSStronglyConnected V

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
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b ↦ ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∀ b_1 ∈ {b}, IsUnit (m.leadingCoeff b_1)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: 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
⊢ 2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : ∀ (b_1 : ↑{b}), m.toSyn (m.degree (↑b_1 * g b_1)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ b ∈ {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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
h1 : m.toSyn (m.degree (↑⟨b, ⋯⟩ * g ⟨b, ⋯⟩)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ∀ b_1 ∈ {b}, ¬m.degree b_1 ≤ c
⊢ b ∈ {b}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: 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
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ 2 • (Multiset.map (fun x ↦ f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial σ R
S : σ → Finset R
Hdeg : ∀ (i : σ), degreeOf i P < #(S i)
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0
⊢ P = 0

Tactic:
by

Goal state after: