mathlib-initiative/mathlib-tactics huggingface dataset:
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 : BinaryFan (Over.mk f) (Over.mk g)
⊢ (({ 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).fst =
    (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).pt.left)
          ⋯).hom ≫
      ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).fst

Tactic:
ext; simp

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 : BinaryFan (Over.mk f) (Over.mk g)
⊢ (({ 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).snd =
    (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).pt.left)
          ⋯).hom ≫
      ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).snd

Tactic:
ext; simp

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
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext hc

Goal state after:
case h₀
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.fst = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.fst

case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd
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✝ : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : PushoutCocone f✝ g
f : X✝ ⟶ Y✝
⊢ (𝟭 (PushoutCocone f✝ g)).map f ≫ Y✝.eta.hom =
    X✝.eta.hom ≫
      ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
ext; simp

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 : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).inl ≫
      (Under.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.right)
          ⋯).hom =
    ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inl

Tactic:
ext; simp

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 : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).inr ≫
      (Under.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.right)
          ⋯).hom =
    ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inr

Tactic:
ext; simp

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 : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents (fun c ↦ c.eta) ⋯).hom.app c) ≫
      (NatIso.ofComponents
              (fun X_1 ↦
                BinaryCofan.ext
                  (Under.isoMk
                    (Iso.refl
                      (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                                  map_comp := ⋯ } ⋙
                                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                                  map_comp := ⋯ }).obj
                            X_1).pt.right)
                    ⋯)
                  ⋯ ⋯)
              ⋯).hom.app
        ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
          c) =
    𝟙
      ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
        c)

Tactic:
ext; simp

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 : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
this : Under.homMk m ⋯ = hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))

Tactic:
exact congr(($this).right)

Goal state after:
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
⊢ tensorEqLocus S M f g ∘ₗ tensorEqLocusInv S M f g = id

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
by
  intro I hI
  constructor
  intro a b h_ab
  contrapose! hI
  -- `↑a - ↑b` is a unit contained in `I`, which contradicts `I ≠ ⊤`.
  refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))
  · simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]
  simpa only [Ne, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI

Goal state after:
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'
inst✝¹ : Algebra L L'
inst✝ : IsScalarTower K L L'
⊢ ↑(toAlgHom K L L').fieldRange = Set.range ⇑(algebraMap L L')

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ ↑n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
← natCast_zsmul θ,

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ ↑n • ψ = ↑n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a s'

Tactic:
← h2

Goal state after:
case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a (tail ⟨f, al⟩)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H : s.destruct = Sum.inr ⟨a, s'⟩
⊢ motive s

Tactic:
rw [destruct_eq_think H]

Goal state after:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H : s.destruct = Sum.inr ⟨a, s'⟩
⊢ motive (Computation.think ⟨a, s'⟩)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i✝ : ℕ
h₁✝ : i✝ < x.length
h₂✝ : i✝ < y.length
⊢ x[i✝] = y[i✝]

Tactic:
rw [← get_append_left, ← get_append_left, h]

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

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get (n + 1) = (initsCore (a :: l) s).get (n + 1)

Tactic:
rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)
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
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + (m' + 1))

Tactic:
exact results_think (h3 h1)

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

Goal state before:
pp: case cons
α : 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 α
⊢ a ∈ (cons c t₁).append s₂ → (cons c t₁).append s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
intro m e
    have := congr_arg destruct e
    rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
    · rw [e']
      exact Or.inl (mem_cons _ _)
    · obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa using e
      rcases o with e' | IH
      · simp [i1, e']
      · exact Or.imp_left (mem_cons_of_mem _) (IH m i2)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))

Tactic:
dsimp [cons, map]

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
⊢ lift G f P (fun i ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
⊢ lift G f (DirectLimit G f) (of G f) ⋯ = RingHom.id (DirectLimit G f)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
⊢ (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯).comp
      (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯) =
    RingHom.id (_root_.DirectLimit G f')

Tactic:
ext; simp

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

Goal state before:
pp: case bisim.nil.nil
α : Type u
S T✝ T : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (nil.append (nil.append T).join).destruct (nil.append (nil.join.append T.join)).destruct

Tactic:
cases T with

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
⊢ (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯).comp
      (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯) =
    RingHom.id (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3))

Tactic:
ext; simp

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

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

Tactic:
exact ⟨nil, S, T, by simp, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
⊢ map (fun x ↦ RingHom.id (G x)) ⋯ = RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
⊢ (map g₂ hg₂).comp (map g₁ hg₁) = map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i j : ι
h : i ≤ j
x : G' i
⊢ ((↑(e j).symm).comp (f' i j h)) x = ((f i j h).comp ↑(e i).symm) x

Tactic:
by
      have eq1 := DFunLike.congr_fun (he i j h) ((e i).symm x)
      simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
        RingEquiv.apply_symm_apply] at eq1 ⊢
      simp [← eq1]

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Tactic:
exact fib_le_of_contsAux_b this

Goal state after:
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
hd : P.d ≠ 0
⊢ P.toPoly.degree = 0

Tactic:
rw [of_c_eq_zero ha hb hc, degree_C hd]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly =
    { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }.toPoly

pp: case inj
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Function.Injective toPoly

Tactic:
· rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]

Goal state after:
case inj
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Function.Injective toPoly
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_1
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₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ f (1 - (1 - a ^ n) ^ n) = f e₁

Tactic:
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]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ matrix n ⊤ = ⊤

Tactic:
ext; simp

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
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * (1 - e a) * c = (1 - e a) * c

Tactic:
(he.idem a).one_sub.eq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * c = (1 - e a) * c
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : R
i j : n
⊢ c.ofMatrix x y ↔ c (single i j x) (single i j y)

Tactic:
refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩
  simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

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

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x

Tactic:
intro h
    exact h _ le_rfl

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Ring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ asIdeal (matrix n I) = Ideal.matrix n (asIdeal I)

Tactic:
ext; simp

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
μ : R
⊢ f.maxGenEigenspace μ = (f - μ • 1).maxGenEigenspace 0

Tactic:
ext; simp

Goal state after: