mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (f x :: List.map f xs).prod (g x :: List.map g xs).prod

Tactic:
List.prod_cons,

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (f x * (List.map f xs).prod) (g x :: List.map g xs).prod
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f.genEigenspace μ) 1 ↔ f x = μ • x

Tactic:
genEigenspace_one,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f - μ • 1).ker ↔ f x = μ • x
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) 1 ≠ ⊥ ↔ ¬LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥

Tactic:
genEigenspace_one,

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f - μ • 1).ker ≠ ⊥ ↔ ¬LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
genEigenspace_one,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f - μ • 1).ker = ⊥
⊢ (f.genEigenspace μ) k = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Tactic:
exact (f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ LinearMap.restrict f ⋯ = μ • LinearMap.id

Tactic:
by
  ext x
  exact mem_eigenspace_iff.mp x.2

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₂) ↑((f.genEigenspace μ₂) ↑l) ↑((f.genEigenspace μ₂) ↑l)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ?m.260)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.275)

Tactic:
· apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯)

R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.275)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.275)

Tactic:
· apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂ : μ₁ ∉ insert μ₂ s
⊢ ?m.80

Tactic:
by rwa [Finset.mem_insert, not_or] at hμ₁₂

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : Nonempty m
⊢ (f x).trace = x.trace

pp: case neg
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).trace = x.trace

Tactic:
· exact Matrix.trace_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x

Goal state after:
case neg
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).trace = x.trace
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
⊢ DivisionRing α

Tactic:
let add_group_with_one := e.addGroupWithOne

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
⊢ DivisionRing α
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
⊢ Field α

Tactic:
let add_group_with_one := e.addGroupWithOne

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
⊢ Field α
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1.intro
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e : α
⊢ Quot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))

Tactic:
exact quot_mk_assoc_left _ _ _ _

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
⊢ reduce ((x, b) :: L1) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
dsimp
    cases r : reduce L1 with
    | nil =>
      dsimp; intro h
      exfalso
      have := congr_arg List.length h
      grind
    | cons hd tail =>
      obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ (s.lcm f).factorization p = s.sup fun a ↦ (f a).factorization p

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C ((map (algebraMap R K) q ^ m).leadingCoeff * a) = C a

Tactic:
(hq_monic.map _).pow m,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C (1 * a) = C a
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case a.s
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| univ

pp: case a.f
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| fun i ↦ (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i

Tactic:
· skip

Goal state after:
case a.f
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| fun i ↦ (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
by
  rw [isIntegrallyClosedIn_iff, and_iff_right (FaithfulSMul.algebraMap_injective _ _)]
  exact congr(∀ _ _, _ ∈ $Subtype.range_val)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap S K).comp (algebraMap R S)

Tactic:
by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), P.coeff x • Δ_[1]^[P.natDegree] fun i ↦ i ^ x) x = (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
Pi.smul_apply

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), P.coeff x • Δ_[1]^[P.natDegree] fun i ↦ i ^ x) x = P.leadingCoeff • ↑P.natDegree ! x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (P.coeff P.natDegree • ↑P.natDegree !) x = P.coeff P.natDegree • ↑P.natDegree ! x

pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
Pi.smul_apply

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ P.coeff P.natDegree • ↑P.natDegree ! x = P.coeff P.natDegree • ↑P.natDegree ! x

R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
n : ℕ
hP : P.natDegree < n
x : R
⊢ Δ_[1]^[n] (fun x ↦ eval x P) x = 0 x

Tactic:
by
  obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP
  rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
    P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]
  simp [fwdDiff_iter_eq_sum_shift]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ ∑ k ∈ range n, P k * r ^ k) = 0

Tactic:
simp_rw [← sum_apply _ _ (fun i x ↦ P i * x ^ i), fwdDiff_iter_finsetSum, sum_fn, ← smul_eq_mul,
    ← Pi.smul_def, fwdDiff_iter_const_smul, ← sum_fn]
  exact sum_eq_zero fun i hi ↦ smul_eq_zero_of_right _ <| fwdDiff_iter_pow_eq_zero_of_lt
    <| mem_range.mp hi

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ X.δ i.succ = 0

Tactic:
← Fin.castSucc_zero,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.castSucc 0) ≫ X.δ i.succ = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ X.δ 0 ≫ inv ⊤.arrow = 0

Tactic:
← Fin.castSucc_zero,

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.castSucc 0) ≫ X.δ 0 ≫ inv ⊤.arrow = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ X.δ 0 = 0

Tactic:
← Fin.castSucc_zero,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.castSucc 0) ≫ X.δ 0 = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).Factors
    ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌))

Tactic:
refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ≫ Y.δ i.succ = 0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
let I := of (Set.image f ⊤)
    let e : X ⟶ I := ofHom ⟨fun x => ⟨f x, ⟨x, by tauto⟩⟩, fun x₁ x₂ h => f.hom.hom.monotone h⟩
    let m : I ⟶ Y := ofHom ⟨fun y => y.1, by tauto⟩
    have : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩
    have : StrongEpi e := strongEpi_of_epi e
    have : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
    exact ⟨⟨I, m, e, rfl⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ P.p ≫ 0 ≫ Q.p = 0

Tactic:
rw [zero_comp, comp_zero]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
subst h
    simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
      Fin.zero_eta, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
      Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x = A.left.app x

Tactic:
refine WidePullback.hom_ext _ _ _ (fun j => ?_) ?_
      · simp
      · simpa using congr_app A.w.symm x

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
⊢ Function.LeftInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)

Tactic:
by
    intro A
    ext x : 2
    · rfl
    · refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_
      · dsimp
        simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right,
          SimplexCategory.len_mk, Arrow.cechConerve_map, colimit.ι_desc,
          WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
        rfl
      · dsimp
        rw [colimit.ι_desc]
        exact congr_app A.w x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤ ≤ (range f).preimage f

Tactic:
rw [← image_le_iff, image_top]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.preimage (inv f) = A.image f

Tactic:
ext _ x
  simp only [preimage_obj, NatIso.isIso_inv_app, Set.mem_preimage, image_obj, Set.mem_image]
  exact ⟨fun hx ↦ ⟨(inv f).app _ x, by simpa⟩, by rintro ⟨x, hx, rfl⟩; simpa⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
s : (⨆ i, A i).toSSet.N
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      s

Tactic:
obtain ⟨d, ⟨⟨s, h₁⟩, h₂⟩, rfl⟩ := s.mk_surjective

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      N.mk ↑⟨⟨s, h₁⟩, h₂⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ ∃ a, ∃ a_1 ∈ X.nonDegenerate a, x ∈ (ofSimplex a_1).obj (op ⦋n⦌)

Tactic:
exact ⟨n, x, hx, mem_ofSimplex_obj x⟩

Goal state after: