mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ map LinearMap.id ⋯ = id

Tactic:
ext ⟨v⟩
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : DivisionRing F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
g : W →ₛₗ[τ] U
hg : Function.Injective ⇑g
hgf : Function.Injective ⇑(g ∘ₛₗ f)
⊢ map (g ∘ₛₗ f) hgf = map g hg ∘ map f hf

Tactic:
ext ⟨v⟩
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v w : ℙ F (m → F)
⊢ v.orthogonal w ↔ w.orthogonal v

Tactic:
by
  induction v with | h v hv => induction w with | h w hw =>
  rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F v hv).cross (mk F w hw) = (mk F w hw).cross (mk F v hv)

Tactic:
rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

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

Tactic:
tsub_eq_zero_iff_le,

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

Goal state before:
pp: case neg
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
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ¬#sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: ⊢ catalan 2 = 2

Tactic:
by
  norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: ⊢ catalan 3 = 5

Tactic:
by
  norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

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

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

Tactic:
← mul_assoc,

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

Goal state before:
pp: case e_a.a
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) = (x * count x m)!

Tactic:
← mul_assoc,

Goal state after:
case e_a.a
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ! ^ count x m * (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) = (x * count x m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
← mul_assoc,

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f + ⇑g) a b = 0

Tactic:
by simp_rw [Pi.add_apply, apply_eq_zero_of_not_le h, zero_add]

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
⊢ f • 0 = 0

Tactic:
ext; exact sum_eq_zero fun x _ ↦ smul_zero _

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) (c + d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
map_add,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ ((algebraMap 𝕜 𝕝) c + (algebraMap 𝕜 𝕝) d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
← mul_assoc,

Goal state after:
case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * n ! ^ m * m !
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ 1 * (zeta 𝕜) x b = 1

Tactic:
zeta_of_le hx.2,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ 1 * 1 = 1
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = if a = b then 1 else 0

Tactic:
split_ifs with hab
  · simp [hab]
  by_cases hab : a ≤ b
  · simp [Icc_eq_cons_Ioc hab, mu'_eq_sum_Ioc_of_ne ‹_›]
  · exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 0

Tactic:
map_add,

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 + (coeff (g x)) (∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) = (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))

Tactic:
map_add,

Goal state after:
case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    (coeff (p.toFinsuppAntidiag i)) 1 + (coeff (p.toFinsuppAntidiag i)) (∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
| fun n ↦ x ^ (n + 1 + 1) * ∏ n ∈ Finset.range (n + 1), (1 - x ^ (n + 1))

Tactic:
ext k
      rw [pow_add, pow_add, mul_assoc (x ^ k), mul_comm (x ^ k), mul_assoc (x ^ 1 * x ^ 1)]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ 1 * x ^ 1 * (x ^ k * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1)))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : (A ∩ B).Nonempty
⊢ A = B

Tactic:
replace hAB := hA.isFragment.inter hK hS hB.isFragment hAB
  replace hA := hA.2 hAB <| by grw [inter_subset_left]
  replace hB := hB.2 hAB <| by grw [inter_subset_right]
  replace hA := eq_of_subset_of_card_le inter_subset_left hA
  replace hB := eq_of_subset_of_card_le inter_subset_right hB
  exact hA.symm.trans hB

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
u v : α
e f : β
X Y : Set α
inst✝ : G.Simple
V : Set α
⊢ ∀ (e : β) (x : α), ¬(noEdge V β).IsLoopAt e x

Tactic:
simp [IsLoopAt]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)

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

Goal state before:
pp: 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)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)

Tactic:
filter_upwards [hV (n' + 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)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ 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
s : Set M
hs : s ∈ U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U

Tactic:
by rwa [← U_idem] at hs

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

Tactic:
mem_prefixed.1 f.2

Goal state after:
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)
⊢ ↑(↑f ((Equiv.symm ↑f) ⟨↑n, ⋯⟩)) < #s
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:
mem_prefixed.1 f.2

Goal state after:
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ᶜ)
⊢ ¬↑(↑f ((Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩)) < #s
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
  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.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 f - m.degree b + m.degree b

Tactic:
ext d
      rw [tsub_add_cancel_of_le hbf]

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) f = m.leadingCoeff b * (↑hb.unit⁻¹ * m.leadingCoeff f)

Tactic:
← mul_assoc,

Goal state after:
σ : 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) f = m.leadingCoeff b * ↑hb.unit⁻¹ * m.leadingCoeff f
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    (Finsupp.linearCombination (MvPolynomial σ R) b)
        (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) +
      r'

Tactic:
map_add,

Goal state after:
case h.left
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    (Finsupp.linearCombination (MvPolynomial σ R) b) g' +
        (Finsupp.linearCombination (MvPolynomial σ R) b)
          (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) +
      r'
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree (b i) + m.degree ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) ≤
    m.toSyn (m.degree f)

Tactic:
map_add,

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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ m.toSyn (m.degree (b i)) +
      m.toSyn (m.degree ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) ≤
    m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  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
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∈ r'.support
⊢ ¬m.degree (b i) ≤ c

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
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  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
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
⊢ ¬m.degree (b i) ≤ c

Tactic:
· exact H'.2.2 c hc' i

Goal state after:
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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  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
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
⊢ ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ M.Indep
        ((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) ∧
      N.Indep
        ((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) ↔
    M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
convert! Iff.rfl <;>
    simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ M.IsBase
        ((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) ∧
      N.IsBase
        ((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) ↔
    M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

Tactic:
convert! Iff.rfl <;>
    simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

Goal state after:
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
⊢ φ.symmetrify.star u =
    ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
by
  rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyStar (φ.obj u))]
  ext ⟨v, f | g⟩ <;>
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyStar]`
    simp only [Quiver.symmetrifyStar, Function.comp_apply] <;>
    erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
    simp

Goal state after: