mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
⊢ ∀ (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂

Tactic:
s'

Goal state after:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
⊢ (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
    ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)

Tactic:
cases s₂.get? n

Goal state after:
case none.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) = Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none none

case none.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : β
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (some val✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) (s₂.get? n)

Tactic:
cases s₂.get? n

Goal state after:
case some.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) none

case some.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ g (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝¹) (some val✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))

Tactic:
cases s₂.get? n

Goal state after:
case none.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)

case none.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val✝))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) (s₂.get? n))

Tactic:
cases s₂.get? n

Goal state after:
case some.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) none)

case some.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝¹) (some val✝))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
obtain ⟨pred_conts, pred_conts_eq⟩ := IH (n + 1) <| lt_add_one (n + 1)
        -- invoke the IH
        rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
        -- option.none
        · use pred_conts
          have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
            contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
          simp only [g, this, pred_conts_eq]
        -- option.some
        · -- invoke the IH a second time
          obtain ⟨ppred_conts, ppred_conts_eq⟩ :=
            IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1
          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
            of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq
          -- finally, unfold the recurrence to obtain the required rational value.
          simp only [g, a_eq_one, b_eq_z,
            contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
          use nextConts 1 (z : ℚ) ppred_conts pred_conts
          cases ppred_conts; cases pred_conts
          simp [nextConts, nextNum, nextDen]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
⊢ (basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
ext
  simp [basisAux, ← Algebra.commutes, Algebra.smul_def]

Goal state after:
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:
by
  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
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₁ : S
he : e₁ ∈ f.range
he₁ : IsIdempotentElem e₁
e₂ : R
he₂ : IsIdempotentElem e₂
he₁e₂ : e₁ * f e₂ = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0

Tactic:
by
  obtain ⟨e₁, rfl⟩ := he
  cases subsingleton_or_nontrivial R
  · exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩
  let a := e₁ - e₁ * e₂
  have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero]
  have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self]
  have hx' : a - a ^ 2 ∈ RingHom.ker f := by
    simp [RingHom.mem_ker, pow_two, ha, he₁.eq]
  obtain ⟨n, hn⟩ := h _ hx'
  refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
  · rcases n with - | n
    · simp at hn
    simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq,
      he₁.one_sub.pow_succ_eq, sub_sub_cancel]
  · obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n
    apply_fun MulOpposite.unop at hk
    have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
    rw [this, mul_assoc]
    rcases n with - | n
    · simp at hn
    rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case e'_1
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ M i p * x - M i p * x * z * M q p * x + -(M i p * x * z) = -(M i p * x * (z * M q p * x + z - 1))

Tactic:
simp [sub_add, mul_add, mul_sub, mul_assoc]

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
⊢ ∏ i, (1 - e i) = 0

Tactic:
by
  rw [he.1.prod_one_sub, he.complete, sub_self]

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✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]
  exact (f.genEigenspace μ).monotone le_top

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ r ∈ Set.range fun x ↦ e * x

Tactic:
simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: 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

Tactic:
exact ⟨a + b, by simp_rw [mul_add, add_mul]⟩

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x ↦
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst✝³ : Semigroup G₁
inst✝² : Semigroup G₂
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i : ι), DecompositionMonoid (G i)
a b c : (i : ι) → G i
h : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
simp_rw [pi_dvd_iff] at h ⊢

Goal state after:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst✝³ : Semigroup G₁
inst✝² : Semigroup G₂
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i : ι), DecompositionMonoid (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
⊢ ∃ a₁ a₂, (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (⁅f, g⁆ * h) = (trace R M) (f * ⁅g, h⁆)

Tactic:
by
  simp only [Ring.lie_def, sub_mul, mul_sub, map_sub, mul_assoc]
  rw [trace_mul_comm R g (f * h), mul_assoc]

Goal state after:
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
  let neg := e.Neg
  let inv := e.Inv
  let div := e.div
  let mul := e.mul
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  let nnratCast := e.nnratCast
  let ratCast := e.ratCast
  let nnqsmul := e.smul ℚ≥0
  let qsmul := e.smul ℚ
  apply e.injective.field _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord

Tactic:
exact FreeGroup.reduce.red

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
simp [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq,
    MonoidAlgebra.cardinalMk_eq_lift_of_fintype]

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(FreeAbelianGroup α) = max #α ℵ₀

Tactic:
rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]
  simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀

Tactic:
have H := mk_range_le_lift (f := FreeAlgebra.lift R ((↑) : s → A))
  rw [lift_umax, lift_id'.{v, u}] at H
  rw [Algebra.adjoin_eq_range_freeAlgebra_lift]
  exact H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

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
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
n : ℕ
hn : n < f.natDegree
⊢ f.coeff n ∈ span {p}

Tactic:
by simpa using hf.mem hn

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B

Tactic:
by
  refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
  rintro ⟨y, rfl⟩
  exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im ^ 2 = -↑(normSq a.im)

Tactic:
simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]

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 ≤ normSq a

Tactic:
normSq_def'

Goal state after:
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
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ (normSq 0)⁻¹ • star 0 = 0

Tactic:
star_zero,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ (normSq 0)⁻¹ • 0 = 0
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✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
⊢ v i ≠ 1 → 1 < f (v i)

Tactic:
refine closure_induction (by simp_all) (by simp) (fun x y _ _ hx hy _ ↦ ?_) hi

Goal state after:
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
⊢ 1 < f (x * y)
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' := ⋯ }
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
have : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩

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' := ⋯ }
this : Epi e
⊢ Nonempty (StrongEpiMonoFactorisation f)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂

Tactic:
rintro ⟨i, j⟩ hij ⟨i', j'⟩ hij' h

Goal state after:
case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (obj X).d (n + 1) n = ∑ i, (-1) ^ ↑i • X.δ i

Tactic:
simp [obj]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ j.succ ≫ X.δ (i.castLT ⋯) = X.δ i ≫ X.δ j

Tactic:
by
  dsimp [δ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt H]

Goal state after:
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 : ℕ
hi : n + i = m
⊢ X.σ₀Iter i hi ≫ X.δ₀Iter i hi = 𝟙 (X _⦋n⦌)

Tactic:
simp [σ₀Iter, δ₀Iter, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ (H.h j ≫ p.app (op ⦋n✝ + 1⦌)) ≫ Y'.σ i.castSucc = X.σ i ≫ H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌)

Tactic:
simpa using H.h_comp_σ_castSucc_of_le i j hij =≫ p.app _

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j

Tactic:
obtain rfl : j = k.val := by grind [dsimp% Fin.lt_def.1 hk']
      rw [Fin.succAbove_of_castSucc_lt _ _ (by lia),
        σ₀Iter_coe_eq_of_lt .., tsub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ x ∈ G.obj X → ofSection x ≤ G

Tactic:
rintro hx U _ ⟨f, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : x ∈ G.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ (ConcreteCategory.hom (F.map f)) x ∈ G.obj U
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))

Tactic:
obtain ⟨x, rfl⟩ := opObjEquiv.symm.surjective x
    rintro ⟨f, _, y, rfl⟩
    exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv.symm y, by simp [op_map]⟩

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
y₁ : ↑(X.nonDegenerate m)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : X _⦋m⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
hf₁ : SplitEpi f₁
⊢ g hf₁ f₂ = 𝟙 ⦋m⦌

Tactic:
have := mono_g hf₁ hy₁ hy₂
  apply SimplexCategory.eq_id_of_mono

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
⊢ (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝ ↔ ∃ x_1 ∈ A.obj x✝, (ConcreteCategory.hom (f.app x✝)) x_1 = x

Tactic:
exact ⟨fun hx ↦ ⟨(inv f).app _ x, by simpa⟩, by rintro ⟨x, hx, rfl⟩; simpa⟩

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
· exact ⟨(alternatingConstHomologyDataEvenNEZero X _ h hn), isZero_zero C⟩

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n