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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
have := f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 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
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥

Tactic:
rw [eq_bot_iff]
  intro x hx
  simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 : LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S = LinearMap.id
b : Basis (Unit × Unit) R (End R S) :=
  ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h)).map (dualTensorHomEquiv R S S)
h2 : (↑f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id
⊢ Function.Bijective ⇑(algebraMap R S)

Tactic:
let eq : R ≃ₗ[R] End R S := .ofLinearMap (f ∘ₗ Algebra.linearMap R S) (.trace R S) h2 h1

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 : LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S = LinearMap.id
b : Basis (Unit × Unit) R (End R S) :=
  ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h)).map (dualTensorHomEquiv R S S)
h2 : (↑f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id
eq : R ≃ₗ[R] End R S := LinearEquiv.ofLinearMap (↑f ∘ₗ Algebra.linearMap R S) (LinearMap.trace R S) h2 h1
⊢ Function.Bijective ⇑(algebraMap R S)
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_1
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V 0)) = ↑(finrank k ↥(f 0).range)

Tactic:
aesop

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

Goal state before:
pp: 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₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let W₁ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₁

Goal state after:
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₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
⊢ Red tl1 (reduce tl1) →
    Red (hd1 :: tl1)
      (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        (reduce tl1))

Tactic:
generalize htl : reduce tl1 = TL

Goal state after:
case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
⊢ Red tl1 TL →
    Red (hd1 :: tl1)
      (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        TL)
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) ≤ max #α ℵ₀

pp: case a
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)

Tactic:
· apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
    simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).le
    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα

Goal state after:
case a
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case coe
α : Type u_1
a : FreeSemigroup α
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑a) = ↑a

Tactic:
induction a with

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
⊢ ⇑f ∘ ⇑(algebraMap R A) = ⇑(algebraMap R B)

Tactic:
aesop

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
hx : IsIntegral R x✝
y : R
fx_eq : (algebraMap R B) y = f x✝
⊢ ∃ y, (algebraMap R A) y = x✝

Tactic:
aesop

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

Goal state before:
pp: ⊢ ∀ {a b : PUnit.{?u.2 + 1}}, a ≠ 0 → b ≠ 0 → 1 = 1 * 1

Tactic:
by subsingleton

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

Goal state before:
pp: ⊢ ∀ (u : PUnit.{?u.2 + 1}ˣ), 1 = u⁻¹

Tactic:
by subsingleton

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

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ x✝¹ = unit * unit

Tactic:
by subsingleton

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

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ x✝ = unit * unit

Tactic:
by subsingleton

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

Goal state before:
pp: x✝⁴ x✝³ x✝² : PUnit.{?u.2 + 1}
x✝¹ : x✝⁴ ∣ x✝²
x✝ : x✝⁴ ∣ x✝³
⊢ unit = x✝⁴ * unit

Tactic:
by subsingleton

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

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ unit * unit * ↑1 = x✝¹ * x✝

Tactic:
by subsingleton

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

Goal state before:
pp: ⊢ ∀ (a : PUnit.{?u.2 + 1}), unit = 0

Tactic:
by subsingleton

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

Goal state before:
pp: ⊢ ∀ (a b : PUnit.{?u.2 + 1}), normalize unit = unit

Tactic:
by subsingleton

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ r * (C h.leadingCoeff * q ^ n)

Tactic:
simp only [← mul_assoc]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ r * C h.leadingCoeff * q ^ n
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ r * C h.leadingCoeff * q ^ n

Tactic:
exact (dvd_pow_self q hn).mul_left _

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| x * star x * ↑(y * star y).re

Tactic:
x.mul_star_eq_coe,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| ↑(x * star x).re * ↑(y * star y).re
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
a n : ℕ
⊢ (∃ y ∈ s, a + y = n) ↔ a ≤ n ∧ n - a ∈ s

Tactic:
aesop

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

Goal state before:
pp: case zero
R : Type u_3
inst✝ : CommRing R
j : ℕ
h : j < 0
⊢ (Δ_[1]^[0] fun r ↦ r ^ j) = 0

Tactic:
aesop

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

Goal state before:
pp: case zero
R : Type u_3
inst✝ : CommRing R
⊢ (Δ_[1]^[0] fun r ↦ r ^ 0) = ↑0!

Tactic:
aesop

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ (Δ_[1]^[n + 1] fun r ↦ r ^ (n + 1)) = ↑(n + 1)!

Tactic:
simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ ((∑ x ∈ range n, (n + 1).choose x • Δ_[1]^[n] fun r ↦ r ^ x) + (n + 1).choose n • Δ_[1]^[n] fun r ↦ r ^ n) = ↑(n + 1)!
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)

Tactic:
exact prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ ∀ {x : G}, x ∈ (M ⊓ M⁻¹).carrier → x⁻¹ ∈ (M ⊓ M⁻¹).carrier

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝³ : Subgroup G
x✝² : Submonoid G
x✝¹ : x✝³.toSubmonoid ≤ x✝²
x✝ : G
⊢ x✝ ∈ x✝³ → x✝ ∈ x✝².mulSupport

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ M.IsMulPointed → M.mulSupport = ⊥

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
x : G
h : (x ∈ M.mulSupport) = (x ∈ ⊥)
⊢ x ∈ M → x⁻¹ ∈ M → x = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hM : M.IsMulSpanning
a : G
⊢ a ∈ M ∨ a⁻¹ ∈ M

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M N : Submonoid G
hM : M.IsMulSpanning
h : M ≤ N
⊢ N.IsMulSpanning

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ s ∈ f, ↑s
hy : b✝ ∈ ⋂ s ∈ f, ↑s
⊢ a✝ * b✝ ∈ ⋂ s ∈ f, ↑s

Tactic:
rw [Set.mem_iInter₂] at *

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : Monoid M
v : ι → M
s : Set ι
⊢ {i | IsMulIndecomposable v s i} ⊆ s

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hi' : v j⁻¹ = 1 ∨ v k⁻¹ = 1
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ v j = 1 ∨ v k = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
⊢ f (v j) < f (v i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
hj' : v j ∈ closure (v '' t)
⊢ f (v k) < f (v i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
ext; simp only [mem_inv', ne_eq, MulOpposite.op_eq_zero_iff, not_false_eq_true, ←
      inv_smul_mem_iff₀, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_inv, MulOpposite.unop_op,
      inv_eq_zero, inv_inv, smul_eq_mul, mul_inv_rev, ha]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ∀ (x y : A),
    (if h : f (x * y) = 0 then 0 else ↑⟨Units.mk0 (f (x * y)) h, ⋯⟩) =
      (if h : f x = 0 then 0 else ↑⟨Units.mk0 (f x) h, ⋯⟩) * if h : f y = 0 then 0 else ↑⟨Units.mk0 (f y) h, ⋯⟩

Tactic:
aesop

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
⊢ WithZero.recZeroCoe 0 Units.val
      ((WithZero.map' f.valueGroup.subtype) (if h : f a = 0 then 0 else ↑⟨Units.mk0 (f a) h, ⋯⟩)) =
    f a

Tactic:
aesop

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hax : f a * ↑y = f x
⊢ f x ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) ((Fintype.equivFin X.obj).symm x.down) =
    (Fintype.equivFin Y.obj).symm
      ((ULift.up ∘
            ⇑(Fintype.equivFin Y.obj) ∘ ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down)
          x).down

Tactic:
aesop

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

Goal state before:
pp: a b : SimplexCategory
x✝² x✝¹ : a ⟶ b
x✝ : (fun f ↦ (Hom.toOrderHom f).toFun) x✝² = (fun f ↦ (Hom.toOrderHom f).toFun) x✝¹
⊢ x✝² = x✝¹

Tactic:
aesop

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

Goal state before:
pp: ⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
aesop

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

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

Goal state before:
pp: n : ℕ
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : ⟨i, isLt✝¹⟩ ≤ ⟨j, isLt✝⟩
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc < ⟨j, isLt✝⟩.succ then
        (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc < ⟨i, isLt✝¹⟩.castSucc then
        (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).succ)

Tactic:
rcases k with ⟨k, _⟩

Goal state after:
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
⊢ ↑(if
          (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc <
            ⟨j, isLt✝¹⟩.succ then
        (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc
      else (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).succ) =
    ↑(if
          (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc <
            ⟨i, isLt✝²⟩.castSucc then
        (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc
      else (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).succ)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
ext k : 3
  dsimp [σ, δ]
  rcases le_or_gt i k with (hik | hik)
  · rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik),
    Fin.succ_predAbove_succ, Fin.succAbove_of_le_castSucc]
    rcases le_or_gt k (j.castSucc) with (hjk | hjk)
    · rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]
    · rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]
      exact H.trans_lt hjk
  · rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hik)]
    have hjk := H.trans_lt' hik
    rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
      (hjk.trans Fin.castSucc_lt_succ).le),
      Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_castPred]
    rwa [Fin.castSucc_castPred]

Goal state after: