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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse ∘SL f = ContinuousLinearMap.id R M

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ (↑e).inverse ∘SL ↑e = ContinuousLinearMap.id R M
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
y : M
⊢ f.inverse (f y) = y

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
y : M
e : M ≃L[R] M₂
⊢ (↑e).inverse (↑e y) = y
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ Function.Bijective ⇑f

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ Function.Bijective ⇑↑e
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse.IsInvertible

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ (↑e).inverse.IsInvertible
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f.inverse.inverse = f

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ (↑e).inverse.inverse = ↑e
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j

Tactic:
dsimp [coneπApp]
    rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)

Tactic:
simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
    cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (hc.conePointUniqueUpToIso h.isLimitCone).hom
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
⊢ ∃ i g', π ≫ g = g' ≫ c.ι.app i ∧ iP ≫ g' = α.app i

Tactic:
choose j x h using fun i ↦ Types.jointly_surjective_of_isColimit hc' ((π ≫ g) (.X i))
    obtain ⟨i, ⟨hi⟩⟩ : ∃ i, Nonempty (∀ a, (j a ⟶ i)) := by
      have : ∃ i, ∀ a, Nonempty (j a ⟶ i) := by
        simpa using! IsFiltered.sup_objs_exists (Finset.univ.image j)
      simpa [← exists_true_iff_nonempty, Classical.skolem, -exists_const_iff] using! this
    refine ⟨i, CommRingCat.ofHom (MvPolynomial.eval₂Hom
      (α.app i).hom (F.map (hi _) <| x ·)), ?_, ?_⟩
    · ext1
      apply MvPolynomial.ringHom_ext
      · simpa using! fun x ↦ congr($(hg i).hom x)
      · intro i
        simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
          Functor.const_obj_obj, CommRingCat.hom_ofHom, MvPolynomial.coe_eval₂Hom,
          MvPolynomial.eval₂_X]
        exact (congr($(c.w (hi i)).hom (x i)).trans (h i)).symm
    · ext x
      simp [P, iP]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ P.underObj.IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
ObjectProperty.isClosedUnderColimitsOfShape_iff_op,

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ P.underObj.op.IsClosedUnderLimitsOfShape WalkingSpanᵒᵖ
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso ⋯) ≪≫
      limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun i ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun i ↦ pres.diag.obj { as := i } }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
underObj_iff,

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso ⋯) ≪≫
      limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun i ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun i ↦ pres.diag.obj { as := i } }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ Q) A.hom
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥((CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left)).equalizer
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag) ≪≫
      limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
underObj_iff,

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥((CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left)).equalizer
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag) ≪≫
      limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ Q) A.hom
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
← mul_one (ringChar R)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
⊢ tensorKerInv S M f ∘ₗ tensorKer S M f = id

Tactic:
ext m x
      apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype
        (ker f).injective_subtype)
      simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ Q (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯)

Tactic:
by
    apply Q.of_precomp (W' := Q)
    · exact Q.pushout_inl _ _ hQf
    · simpa using Q.of_isIso _

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ (Ideal.Quotient.mk (Ideal.span {↑↑n})) ↑↑n = ↑0

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ (Ideal.Quotient.mk (Ideal.span {↑↑n})) ↑↑n = 0
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
h_eq

Goal state after:
case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
get_append_right,

Goal state after:
case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ a.get p = (List.drop n x ++ₛ a).get (m + p)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
· simpa [length'_of_not_terminates h] using forall_not_of_not_exists h n

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ initsCore l s = l :: initsCore (l ++ [s.head]) s.tail

Tactic:
by
    unfold initsCore corecOn
    rw [corec_eq]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).Results b (n + 0)

Tactic:
exact h2

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ nil.append s = s

Tactic:
apply coinduction2; intro s
  dsimp [append]; rw [corec_eq]
  dsimp [append]
  cases s
  · trivial
  · rw [destruct_cons]
    dsimp
    exact ⟨rfl, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
s t u : Seq α
⊢ IsBisimulation fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)

Tactic:
rintro _ _ ⟨s, t, u, rfl, rfl⟩
    cases s with
    | nil =>
      cases t with
      | nil =>
        cases u with
        | nil => simp
        | cons _ u => simpa using ⟨nil, nil, u, by simp, by simp⟩
      | cons _ t => simpa using ⟨nil, t, u, by simp, by simp⟩
    | cons _ s => simpa using ⟨s, t, u, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' : Computation α
⊢ ∀ ⦃s₂ : Computation α⦄,
    (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s' s₂ → BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s₂.destruct

Tactic:
s

Goal state after:
α : Type u
c s' s : Computation α
⊢ (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s' s → BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' : Computation α
⊢ ∀ ⦃s₂ : Computation α⦄,
    (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s' s₂ → BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s₂.destruct

Tactic:
s

Goal state after:
α : Type u
c s' s : Computation α
⊢ (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s' s → BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
exact h2

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'

Tactic:
exact ab'

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab⟩ := h.left ma

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
⊢ R a b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')

Tactic:
by
  ext1 n
  cases n <;> simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ ∀ x ∈ cons hd tl, p x

Tactic:
simp only [mem_cons_iff, forall_eq_or_imp] at *

Goal state after:
α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ p hd ∧ ∀ a ∈ tl, p a
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
x y z : S
⊢ (X - C x) * (X - C y) * (X - C z) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly

Tactic:
rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ v - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices
      (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by
      rwa [g_finite_correctness]

Goal state after:
case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Semifield K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Surjective (MulSemiringAction.toAlgEquiv K (End K V))

Tactic:
by
  intro f
  have ⟨T, hT⟩ := f.eq_linearEquivConjAlgEquiv
  exact ⟨.ofLinearEquiv T, hT.symm⟩

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:
s

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
⊢ 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: 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), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
s

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
s : Finset R
⊢ μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ IsNilpotent ((trace R M) (f ∘ₗ n))

Tactic:
← Module.End.mul_eq_comp

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ IsNilpotent ((trace R M) (f * n))