mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n

Tactic:
rw [eventually_atTop]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → v = (of v).convs b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
intro s

Goal state after:
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq

Goal state after:
case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
⊢ (squashSeq s n).get? m = s.get? m
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
exists N

Goal state after:
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∀ n ≥ N, |v - (of v).convs n| < ε
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
hf : Function.Injective ⇑f
⊢ CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp [completeOrthogonalIdempotents_iff, ← hf.eq_iff,
    OrthogonalIdempotents.map_injective_iff f hf]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
clear hn

Goal state after:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ M ∈ matrix n I.jacobson → M ∈ (matrix n I).jacobson

Tactic:
MI

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ M ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
⊢ M ∈ matrix n I → M ∈ matrix n J

Tactic:
MI

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
MI : M ∈ matrix n I
⊢ M ∈ matrix n J
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
⊢ ∀ {a b : R},
    (a ∈ Set.range fun x ↦ e * x * e) → (b ∈ Set.range fun x ↦ e * x * e) → a * b ∈ Set.range fun x ↦ e * x * e

Tactic:
rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
a b : R
⊢ (fun x ↦ e * x * e) a * (fun x ↦ e * x * e) b ∈ Set.range fun x ↦ e * x * e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
⊢ ∀ {a b : R},
    a ∈ (Subsemigroup.corner e).carrier → b ∈ (Subsemigroup.corner e).carrier → a + b ∈ (Subsemigroup.corner e).carrier

Tactic:
rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (fun x ↦ e * x * e) a + (fun x ↦ e * x * e) b ∈ (Subsemigroup.corner e).carrier
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalRing R
a : R
⊢ (fun x ↦ e * x * e) (-a) = -(fun x ↦ e * x * e) a

Tactic:
simp_rw [mul_neg, neg_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f * g * ↑f⁻¹) = (trace R M) g

Tactic:
by
  rw [trace_mul_comm]
  simp

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

Goal state before:
pp: case refine_2
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 : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ Submodule.map (g ^ l) (⨆ a ∈ s, (f.genEigenspace a) k) ≤ ⨆ a ∈ s, (f.genEigenspace a) k

Tactic:
Submodule.map_iSup (ι := R),

Goal state after:
case refine_2
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 : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ ⨆ i, Submodule.map (g ^ l) (⨆ (_ : i ∈ s), (f.genEigenspace i) k) ≤ ⨆ a ∈ s, (f.genEigenspace a) k
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case exact₁
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
g₀ : W₀ →ₗ[k] W₁ := ⋯
g₁ : W₁ →ₗ[k] W₂ := ⋯
g₂ : W₂ →ₗ[k] W₃ := ⋯
g₃ : W₃ →ₗ[k] W₄ := ⋯
g₄ : W₄ →ₗ[k] W₅ := ⋯
this :
  Exact ⇑g₀ ⇑g₁ →
    Exact ⇑g₁ ⇑g₂ →
      Exact ⇑g₂ ⇑g₃ →
        Exact ⇑g₃ ⇑g₄ →
          ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
⊢ Exact ⇑g₀ ⇑g₁

Tactic:
simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case exact₂
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
g₀ : W₀ →ₗ[k] W₁ := ⋯
g₁ : W₁ →ₗ[k] W₂ := ⋯
g₂ : W₂ →ₗ[k] W₃ := ⋯
g₃ : W₃ →ₗ[k] W₄ := ⋯
g₄ : W₄ →ₗ[k] W₅ := ⋯
this :
  Exact ⇑g₀ ⇑g₁ →
    Exact ⇑g₁ ⇑g₂ →
      Exact ⇑g₂ ⇑g₃ →
        Exact ⇑g₃ ⇑g₄ →
          ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
⊢ Exact ⇑g₁ ⇑g₂

Tactic:
simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case exact₃
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
g₀ : W₀ →ₗ[k] W₁ := ⋯
g₁ : W₁ →ₗ[k] W₂ := ⋯
g₂ : W₂ →ₗ[k] W₃ := ⋯
g₃ : W₃ →ₗ[k] W₄ := ⋯
g₄ : W₄ →ₗ[k] W₅ := ⋯
this :
  Exact ⇑g₀ ⇑g₁ →
    Exact ⇑g₁ ⇑g₂ →
      Exact ⇑g₂ ⇑g₃ →
        Exact ⇑g₃ ⇑g₄ →
          ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
⊢ Exact ⇑g₂ ⇑g₃

Tactic:
simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case exact₄
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ⋯
g₀ : W₀ →ₗ[k] W₁ := ⋯
g₁ : W₁ →ₗ[k] W₂ := ⋯
g₂ : W₂ →ₗ[k] W₃ := ⋯
g₃ : W₃ →ₗ[k] W₄ := ⋯
g₄ : W₄ →ₗ[k] W₅ := ⋯
this :
  Exact ⇑g₀ ⇑g₁ →
    Exact ⇑g₁ ⇑g₂ →
      Exact ⇑g₂ ⇑g₃ →
        Exact ⇑g₃ ⇑g₄ →
          ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
⊢ Exact ⇑g₃ ⇑g₄

Tactic:
simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.Algebra.Field.ZMod

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
by
  obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
  apply coe_mul_inv_eq_one
  apply Nat.Coprime.symm
  rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ x y : FreeMagma α
ih1 : (fun {α} ↦ η.app α) (traverse f x) = traverse ((fun {α} ↦ η.app α) ∘ f) x
ih2 : (fun {α} ↦ η.app α) (traverse f y) = traverse ((fun {α} ↦ η.app α) ∘ f) y
⊢ (fun {α} ↦ η.app α) (traverse f (x * y)) = traverse ((fun {α} ↦ η.app α) ∘ f) (x * y)

Tactic:
by simp only [traverse_mul, functor_norm, ih1, ih2]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F ({ head := hd, tail := tl } * { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
rw [ih]; simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
ih1 : (fun {α} ↦ η.app α) (traverse f (pure x)) = traverse ((fun {α} ↦ η.app α) ∘ f) (pure x)
ih2 : (fun {α} ↦ η.app α) (traverse f y) = traverse ((fun {α} ↦ η.app α) ∘ f) y
⊢ (fun {α} ↦ η.app α) (traverse f (pure x * y)) = traverse ((fun {α} ↦ η.app α) ∘ f) (pure x * y)

Tactic:
by simp only [traverse_mul, functor_norm, ih1, ih2]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ max (#α * 2) ℵ₀ = #α

Tactic:
max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),

Goal state after:
case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α * 2 = #α
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ (⇑Multiplicative.ofAdd ∘ countP' p) 1 = 1

Tactic:
by
    simp [countP'_one p]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
⊢ x ^ i ∈ 𝓟

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ i ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Group G
inst✝ : MulAction G X
f : Equidecomp X G
⊢ f.symm.source = ↑f.toPartialEquiv '' f.source

Tactic:
rw [image_source_eq_target, symm_source]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : n = f.natDegree
⊢ f.coeff n - f.leadingCoeff ∈ P

Tactic:
rw [hn, leadingCoeff, sub_self]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : n = f.natDegree
⊢ 0 ∈ P
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ s = a⁻¹ • univ ↔ s = univ

Tactic:
smul_finset_univ

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ s = univ ↔ s = univ
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: case inl
M : Type u_1
inst✝ : Semigroup M
s : Set M
x y : M
hy : y ∈ s
⊢ x • y ∈ s ∪ univ * s

pp: case inr
M : Type u_1
inst✝ : Semigroup M
s : Set M
x y z : M
hz : z ∈ s
⊢ x • (fun x1 x2 ↦ x1 * x2) y z ∈ s ∪ univ * s

Tactic:
· exact .inr <| mul_mem_mul (mem_univ _) hy

Goal state after:
case inr
M : Type u_1
inst✝ : Semigroup M
s : Set M
x y z : M
hz : z ∈ s
⊢ x • (fun x1 x2 ↦ x1 * x2) y z ∈ s ∪ univ * s
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
k : ℕ
y : M
⊢ (shiftₗ M G h ^ k) f y = f (y + k • h)

Tactic:
induction k generalizing f with
  | zero => simp
  | succ k IH => simp [pow_add, IH (shiftₗ M G h f), shiftₗ_apply, add_assoc, add_nsmul]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case inv
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x✝ x : M
hx : x ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, x⁻¹ = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨a, rfl⟩ := hx'

Goal state after:
case inv
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a_1.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
⊢ ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})

Tactic:
epi_iff_surjective

Goal state after:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (s : Fork (𝟙 X) p) →
    { l // l ≫ (Fork.ofι i ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }

Tactic:
intro s

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l // l ≫ (Fork.ofι i ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
e : X ⟶ I := ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom f) x, ⋯⟩, monotone' := ⋯ }
m : I ⟶ Y := ofHom { toFun := fun y ↦ ↑y, monotone' := ⋯ }
⊢ Epi e

Tactic:
epi_iff_surjective

Goal state after:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
e : X ⟶ I := ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom f) x, ⋯⟩, monotone' := ⋯ }
m : I ⟶ Y := ofHom { toFun := fun y ↦ ↑y, monotone' := ⋯ }
⊢ Function.Surjective ⇑(ConcreteCategory.hom e)
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
f g : P ⟶ Q
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f

Tactic:
rw [add_comp, comp_add, f.comm, g.comm]

Goal state after: