mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : 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
⊢ ∃ 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_cases hf0 : f = 0

Goal state after:
case pos
σ : 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
⊢ ∃ 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

case neg
σ : 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
⊢ ∃ 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
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case e'_2.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' I = Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' I

pp: case e'_2.e'_4
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' X = Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' X

Tactic:
<;>

Goal state after:
case e'_2.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' I = Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' I

case e'_2.e'_4
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' X = Sigma.mk a✝ ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' X
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I

pp: case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I

Tactic:
<;>

Goal state after:
case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I

case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B

pp: case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B

Tactic:
<;>

Goal state after:
case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B

case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case e'_2
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
⊢ (fun j ↦ ![![a, b], ![b, a]] j 0) = ![a, b]

pp: case e'_3
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
⊢ (fun j ↦ ![![a, b], ![b, a]] j 1) = ![b, a]

Tactic:
<;>

Goal state after:
case e'_2
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
⊢ (fun j ↦ ![![a, b], ![b, a]] j 0) = ![a, b]

case e'_3
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
⊢ (fun j ↦ ![![a, b], ![b, a]] j 1) = ![b, a]
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ a = a

pp: case refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ ⟨e, ⋯⟩ ≍ ⟨e, ⋯⟩

Tactic:
<;>

Goal state after:
case refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ a = a

case refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ ⟨e, ⋯⟩ ≍ ⟨e, ⋯⟩
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case refine_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.star v)

pp: case refine_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.costar v)

Tactic:
<;>

Goal state after:
case refine_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.star v)

case refine_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.costar v)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: 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 : u ⟶ v
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)) ⟨v, Sum.inl f⟩

pp: 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 : v ⟶ u
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)) ⟨v, Sum.inr g⟩

Tactic:
<;>

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 : u ⟶ v
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar 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 : v ⟶ u
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)) ⟨v, Sum.inr g⟩
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a : V
⊢ nil.length = 0 ↔ nil = nil

pp: case cons
V : Type u_1
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
⊢ (a✝¹.cons a✝).length = 0 ↔ a✝¹.cons a✝ = nil

Tactic:
<;>

Goal state after:
case nil
V : Type u_1
inst✝ : Quiver V
a : V
⊢ nil.length = 0 ↔ nil = nil

case cons
V : Type u_1
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
⊢ (a✝¹.cons a✝).length = 0 ↔ a✝¹.cons a✝ = nil
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: 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 : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)

pp: 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 : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)

Tactic:
<;>

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 : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ 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 : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: 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 : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

pp: 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 : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)

Tactic:
<;>

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 : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

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 : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ (p'.cons e).length
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n

Tactic:
rw [length_cons] at hn

Goal state after:
case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: 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
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)) ⟨v, Sum.inl f⟩

pp: 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
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)) ⟨v, Sum.inr g⟩

Tactic:
<;>

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
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar 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
⊢ (⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)) ⟨v, Sum.inr g⟩
Module: Mathlib.Combinatorics.Quiver.Covering

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

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

Tactic:
<;>

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.Quiver.Covering

Goal state before:
pp: 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
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

pp: 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
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)

Tactic:
<;>

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
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

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
⊢ Sum.map (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.costar u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case refine_1
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.star u)

pp: case refine_2
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.costar u)

Tactic:
<;>

Goal state after:
case refine_1
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.star u)

case refine_2
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.costar u)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case fst
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u v : U
f : v ⟶ u
⊢ (φ.costar u ⟨v, f⟩).fst = ((⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm) ⟨v, f⟩).fst

pp: case snd
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u v : U
f : v ⟶ u
⊢ (φ.costar u ⟨v, f⟩).snd ≍ ((⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm) ⟨v, f⟩).snd

Tactic:
<;>

Goal state after:
case fst
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u v : U
f : v ⟶ u
⊢ (φ.costar u ⟨v, f⟩).fst = ((⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm) ⟨v, f⟩).fst

case snd
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u v : U
f : v ⟶ u
⊢ (φ.costar u ⟨v, f⟩).snd ≍ ((⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm) ⟨v, f⟩).snd
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s ↦ s.erase a) ↑({s ∈ 𝒜 | a ∈ s})

Tactic:
apply (erase_injOn' _).mono

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ↑({s ∈ 𝒜 | a ∈ s}) ⊆ {s | a ∈ s}
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case empty.inl
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p ∅

pp: case empty.inr
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p {∅}

Tactic:
<;>

Goal state after:
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p ∅

case empty.inr
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p {∅}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ A + B = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ ∀ (x : ℕ), x ∈ A + B
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : a ≤ b
⊢ ({b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x) = b

pp: case neg
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : ¬a ≤ b
⊢ ⊤ = ⊤

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : a ≤ b
⊢ ({b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x) = b

case neg
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
h✝ : ¬a ≤ b
⊢ ⊤ = ⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
⊢ a ≤ s.truncatedSup a

Tactic:
rw [truncatedSup]

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
⊢ a ≤ if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤