mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Tactic:
roots,

Goal state after:
R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).toPoly.roots = (Polynomial.map φ P.toPoly).roots
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
roots,

Goal state after:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.toPoly.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3

Tactic:
roots,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).toPoly.roots.card = 3
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ (f ^ 0) v = μ ^ 0 • v

Tactic:
simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

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

Goal state before:
pp: case succ
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
n✝ : ℕ
a✝ : (f ^ n✝) v = μ ^ n✝ • v
⊢ (f ^ (n✝ + 1)) v = μ ^ (n✝ + 1) • v

Tactic:
simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
⊢ a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
has

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
⊢ (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * 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
k : ℕ∞
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

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
k : ℕ∞
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ⊤) ↑((f.genEigenspace μ) ⊤)
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Goal state after:
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 μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

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.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)
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 ∈ (NonUnitalSubsemiring.corner e).carrier

Tactic:
exact ⟨-a, by simp_rw [mul_neg, neg_mul]⟩

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
⊢ (↑fe).1 (inl a).fst + (↑fe).1 (inl a).snd * (↑fe).2 = (↑fe).1 a

Tactic:
fst_inl,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
⊢ (↑fe).1 a + (↑fe).1 (inl a).snd * (↑fe).2 = (↑fe).1 a
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
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
⊢ ∃ l, ∃ (_ : ↑l ≤ k), ((t • f - (t * μ) • 1) ^ l) m = 0

Tactic:
peel hm with l hlk hl

Goal state after:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - (t * μ) • 1) ^ l) m = 0
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
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
⊢ False

Tactic:
have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩

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
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ False
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
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (g x ⊓ g y) (g (x + y))

Tactic:
apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))

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
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := ⋯
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (g (x + y))
Module: Mathlib.Algebra.Group.MinimalAxioms

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a

Tactic:
by
      have mul_inv_cancel : ∀ a : G, a * a⁻¹ = 1 := fun a =>
        calc a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
          _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by
            rw [inv_mul_cancel]
          _ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by
            simp only [assoc]
          _ = 1 := by
            rw [inv_mul_cancel, one_mul, inv_mul_cancel]
      rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ ((fun h ↦ h y) <$> pure fun x2 ↦ x * x2) = pure (x * y)

Tactic:
map_pure

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ pure ((fun x2 ↦ x * x2) y) = pure (x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ ((fun h ↦ h (f <$> y)) <$> pure fun x2 ↦ f <$> x * x2) = pure (f <$> x * f <$> y)

Tactic:
map_pure

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ pure ((fun x2 ↦ f <$> x * x2) (f <$> y)) = pure (f <$> x * f <$> y)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ Function.Injective toWord

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩

Goal state after:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ ((fun h ↦ h y) <$> pure fun x2 ↦ of x * x2) = pure (of x * y)

Tactic:
map_pure

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ pure ((fun x2 ↦ of x * x2) y) = pure (of x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ ((fun h ↦ h (f <$> y)) <$> pure fun x2 ↦ f <$> of x * x2) = pure (f <$> of x * f <$> y)

Tactic:
map_pure

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ pure ((fun x2 ↦ f <$> of x * x2) (f <$> y)) = pure (f <$> of x * f <$> y)
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeSemigroup α
⊢ toFreeMonoid x ≠ 1

Tactic:
by
  induction x with simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t) • x = s • t • x

Tactic:
ext <;> exact smul_assoc _ _ _

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
natDegree_scaleRoots,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < p.natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ ∀ {x : U}, IsIntegral R x ↔ ∃ y, (algebraMap S U) y = x

Tactic:
intro x
    refine ⟨fun h ↦ ?_, ?_⟩
    · obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
      rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
      obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
      exact ⟨x, IsScalarTower.algebraMap_apply ..⟩
    · rintro ⟨x, rfl⟩
      rw [IsScalarTower.algebraMap_apply S T U]
      exact ((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ a ^ n ∣ b ^ n ∧ b ^ n ∣ a ^ n ↔ a ∣ b ∧ b ∣ a

Tactic:
pow_dvd_pow_iff hn

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(normSq a) ↔ star a = -a

Tactic:
· rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

Goal state after:
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 g : M → G
n : ℕ
⊢ Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g

Tactic:
by
  simpa only [coe_fwdDiffₗ_pow] using map_add (fwdDiffₗ M G h ^ n) f g

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:
rw [sum_apply, sum_range_succ, sum_eq_zero (fun i hi ↦ ?_), zero_add,
    fwdDiff_iter_eq_factorial, leadingCoeff, Pi.smul_apply]

Goal state after:
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.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
rw [div_eq_mul_inv, ← natCard_inv t]; exact natCard_mul_le

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ 1 (f x) = 1 x

Tactic:
rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero]

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ f x ≠ 0
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp }.p ≫ p.f ≫ P.p = p.f

Tactic:
rw [comp_p p, hp]

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

Goal state before:
pp: case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

Tactic:
rw [← ε.functor.map_comp, h₁, ε.functor.map_id]

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
hi'' : ↑i' = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
i i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i' = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < ↑i
hi'' : ↑i = ↑i' + j
⊢ X.σ₀Iter j ⋯ ≫ X.δ i = X.δ i' ≫ X.σ₀Iter j ⋯

Tactic:
simp only [σ₀Iter, δ, ← Functor.map_comp, ← op_comp,
    SimplexCategory.δ_σ₀Iter' i j i']

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

Goal state before:
pp: case zero
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : ↑j = ↑j' + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j' + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ j ≫ SimplexCategory.σ₀Iter i hi).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op

Tactic:
SimplexCategory.σ_σ₀Iter ..

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n m : ℕ
h : n + 0 = m
⊢ σ₀Iter (0 + 1) ⋯ = σ 0 ≫ σ₀Iter 0 h

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
h : n + 0 = n
⊢ σ₀Iter (0 + 1) ⋯ = σ 0 ≫ σ₀Iter 0 h
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp hθ
  use i
  exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Epi θ

Tactic:
grind [→ le_of_epi]

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + 0 = n
hi' : 0 < ↑i
hi'' : ↑i = ↑i' + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
i : Fin (n + 2)
hi' : 0 < ↑i
i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i = ↑i' + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + 0 = m
hj : ↑j = ↑j' + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
j' j : Fin (n + 1)
hi : n + 0 = n
hj : ↑j = ↑j' + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n m : ℕ
hi : n + 0 = m
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌

Tactic:
obtain rfl : n = m := by lia

Goal state after:
case zero
n : ℕ
hi : n + 0 = n
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
A B : X.Subcomplex
⊢ A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
d : ℕ
hd : (Finset.image φ ⊤).max = ↑d
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.image φ ⊤
⊢ x✝¹ < d + 1

Tactic:
grind [WithBot.coe_le_coe, → Finset.le_max]

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
⊢ Y.Finite

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite
  have := hasDimensionLT_of_epi f d
  refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)
  have : Finite (Y _⦋i⦌) := by
    rw [NatTrans.epi_iff_epi_app] at hf
    simp only [epi_iff_surjective] at hf
    exact Finite.of_surjective _ (hf _)
  infer_instance

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
i : Fin (n + 1)
s : nerve X _⦋n⦌
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) s).obj i.castSucc =
    ((ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) s).obj i.succ

Tactic:
simp [-nerve_obj, nerve.σ_obj]

Goal state after: