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

Goal state before:
pp: case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb ↦ (bil fb.1) fb.2) = fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
this : ContinuousAdd C
⊢ Continuous fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : StrongDual R M
hf : f ≠ 0
x : M
hx : f x ≠ 0
y : M
⊢ Continuous[inst✝⁷, inst✝³] fun a ↦ y + (a - f y) • (f x)⁻¹ • x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ∀ (x y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0

Tactic:
intro x y hy e

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x y : ↑S.X₂.toModuleCat
hy : (ConcreteCategory.hom S.g) y = 0
e : (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x
⊢ (ConcreteCategory.hom S.g) x = 0
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
hF : IsEventuallyConstant F
inst✝ : IsFiltered J
j : J
h : F.IsEventuallyConstantFrom j
⊢ HasColimit F

Tactic:
exact h.hasColimit

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
e : F✝ ≅ G✝
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsCardinalAccessible κ
inst✝ : G.IsCardinalAccessible κ
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
e : F✝ ≅ G✝
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsCardinalAccessible κ
inst✝ : G.IsCardinalAccessible κ
this : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
⊢ (F ⋙ G).IsCardinalAccessible κ
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∀ {X_1 Y : C'} (f : X_1 ⟶ Y),
    (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y).trans Equiv.ulift.symm)).toIso.hom =
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X X_1).trans Equiv.ulift.symm)).toIso.hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
by
        intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Tactic:
· intro
    constructor
    intro A _ F hA
    rw [hasCardinalLT_aleph0_iff] at hA
    have := ((Arrow.finite_iff A).1 hA).some
    exact ⟨IsFiltered.cocone F⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ((piRightInv R S N M) fun i ↦ x ⊗ₜ[R] m i) = x ⊗ₜ[R] m

Tactic:
simp only [piRightInv, lsum_apply, coe_sum, coe_comp, coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, AlgebraTensorModule.map_tmul, id_coe, id_eq, coe_single]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ∑ c, x ⊗ₜ[R] Pi.single c (m c) = x ⊗ₜ[R] m
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
⊢ Continuous[instTopologicalSpaceHom, instTopologicalSpaceProd] fun f ↦
    (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
p : ↑(of (MvPolynomial σ ↑A))
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun a ↦
    ∑ d ∈ MvPolynomial.support p, (Hom.hom a.1) (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a.2 i ^ d i

Tactic:
fun_prop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
⊢ ∀ {X_1 Y_1 : BinaryFan (Over.mk f) (Over.mk g)} (f_1 : X_1 ⟶ Y_1),
    ({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f_1 ≫
        (BinaryFan.ext
            (Over.isoMk
              (Iso.refl
                (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                            map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                            map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ }).obj
                      Y_1).pt.left)
              ⋯)
            ⋯ ⋯).hom =
      (BinaryFan.ext
            (Over.isoMk
              (Iso.refl
                (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                            map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                            map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ }).obj
                      X_1).pt.left)
              ⋯)
            ⋯ ⋯).hom ≫
        (𝟭 (BinaryFan (Over.mk f) (Over.mk g))).map f_1

Tactic:
by intros; ext; simp [BinaryFan.ext]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : addOrderOf r • r = 0
⊢ False

Tactic:
rw [hr, nsmul_eq_mul] at hr₁

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
⊢ False
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)

Tactic:
rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
⊢ Function.Injective (map f)

Tactic:
intro _ _ h
  rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

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

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
· simp only [length'_of_not_terminates h, ENat.natCast_lt_top, Option.mem_def, true_iff]
    rw [not_terminates_iff] at h
    rw [← Option.isSome_iff_exists]
    exact h n

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partDens.get? n = none ↔ none = none

Tactic:
simp [partDens, s_nth_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partDens.get? n = none ↔ some val✝ = none

Tactic:
simp [partDens, s_nth_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partDens.get? n = some gp.b

Tactic:
simp [partDens, s_nth_eq]

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

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

Tactic:
have := h1.mem; revert m
  apply memRecOn this _ fun s IH => _
  · intro _ h1
    rw [ret_bind]
    rw [h1.len_unique (results_pure _)]
    exact h2
  · intro _ h3 _ h1
    rw [think_bind]
    obtain ⟨m', h⟩ := of_results_think h1
    obtain ⟨h1, e⟩ := h
    rw [e]
    exact results_think (h3 h1)

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

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

Tactic:
rw [mem_unique ma h2]; exact h1

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

Goal state before:
pp: case cons.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rcases o with e' | IH

Goal state after:
case cons.inr.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

case cons.inr.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (map f1 s1) (map f2 s2)

Tactic:
by
  rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1; simpa

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

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = S.join.append T.join

Tactic:
apply
    eq_of_bisim fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))

Goal state after:
case bisim
α : Type u
S T : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)

case r
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ s S_1 T_1,
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
init : β
f : β → α → β
⊢ nil.fold init f = cons init nil

Tactic:
by
  unfold fold
  simp [corec_nil]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 2 + 1) - fib (n + 2)

Tactic:
add_right_comm,

Goal state after:
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1 + 2) - fib (n + 2)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m))

Tactic:
gcd_comm (fib m) _

Goal state after:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib (n % m)).gcd (fib m)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
⊢ ∃ q, v = ↑q

Tactic:
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates
  obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convs n = (↑q : K) := exists_rat_eq_nth_conv v n
  have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
  use q, this

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.d = Q.d

Tactic:
← coeff_eq_d,

Goal state after:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.toPoly.coeff 0 = Q.d
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.natDegree = 1

Tactic:
by
  rw [of_b_eq_zero ha hb, natDegree_linear hc]

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

Goal state before:
pp: case inr.ha
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
this : 0 < b
⊢ 0 < b * (of v).dens n * (of v).dens n

Tactic:
apply_rules [mul_pos]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

Tactic:
refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : 0 ∣ 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
zero_dvd_iff,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2 = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
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
μ : R
k : ℕ
⊢ f.genEigenrange μ ↑k = ((f - μ • 1) ^ k).range

Tactic:
by
  ext x
  simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]
  constructor
  · intro h
    exact h _ le_rfl
  · rintro ⟨x, rfl⟩ i hi
    have : k = i + (k - i) := by lia
    rw [this, pow_add]
    exact ⟨_, rfl⟩

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
f : End R M
⊢ f.eigenspace 0 = LinearMap.ker f

Tactic:
simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]

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

Goal state before:
pp: 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
inj : Injective ⇑(f 0)
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
surj : Surjective ⇑(f (Fin.last n))
⊢ ∑ i, (-1) ^ ↑i * ↑(finrank k (V i)) = 0

Tactic:
by
  replace inj := LinearMap.finrank_range_of_inj inj
  replace surj := LinearMap.range_eq_top.mpr surj
  simp_rw [← smul_eq_mul]
  refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_
  · aesop
  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
      ```
      -/
    have hrn := (f i.succ).finrank_range_add_finrank_ker
    have hker : finrank k ↥(LinearMap.ker (f i.succ)) =
        finrank k ↥(LinearMap.range (f i.castSucc)) :=
      congrArg (fun S : Submodule k (V i.succ.castSucc) => finrank k ↥S)
        (h_exact i).linearMap_ker_eq
    omega
  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [finrank_top]
      ```
      -/
    rw [surj, finrank_top, Fin.succ_last]

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
← h'.geom_sum₂_mul,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)

Tactic:
rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)

Tactic:
simp only [map_mul, *]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeSemigroup α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : f (of x) = g (of x)
hy : f y = g y
⊢ f (of x * y) = g (of x * y)

Tactic:
simp only [map_mul, *]

Goal state after: