mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y f ↔ R f

Tactic:
exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ P.mapRelations F η ≫ P.mapGenerators F η = 0

Tactic:
simp only [mapRelations, GeneratingSections.mapFreeHom, Category.assoc, Iso.inv_hom_id_assoc,
    ← Functor.map_comp, kernel.condition, Functor.map_zero, comp_zero]

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

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
obtain ⟨T, e, he⟩ := hφ.exists_smallRepr

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
T : FGAlgCatSkeleton ↑R
e : ↑(FGAlgCatSkeleton.eval (↑R) T).obj ≃+* ↑S
he : Hom.hom φ = e.toRingHom.comp (algebraMap ↑R ↑(FGAlgCatSkeleton.eval (↑R) T).obj)
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
obtain ⟨n, c, d, hn⟩ := wideSpan b
        (hasCardinalLT_prod (Cardinal.IsRegular.aleph0_le Fact.out) hι hι)

Goal state after:
case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₂
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
x : ↑S
hx : x ∈ hf.finset
this :
  ∀ (x : ↑S),
    (ConcreteCategory.hom (F.map (f₁ x))) ((ConcreteCategory.hom a) x) =
      (ConcreteCategory.hom (F.map (f₂ x))) ((ConcreteCategory.hom b) x)
⊢ (CommRingCat.Hom.hom
        (a ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.fst ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x =
    (CommRingCat.Hom.hom
        (b ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.snd ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x

Tactic:
simp [D, this]

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
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ Under.Hom.right m =
    Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

Tactic:
refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_

Goal state after:
case refine_1
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
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inl ≫ Under.Hom.right m =
    c.inl ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

case refine_2
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
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
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 : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
r : ℕ
hr : q = ringChar R * r
⊢ False

Tactic:
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq

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 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ map Q ⋯ = map Q hg ⋙ map Q hf

Tactic:
by
  fapply Functor.ext
  · simp [map, Comma.mapLeft, CategoryTheory.Comma.mapLeft, Comma.lift]
  · intro U V k
    ext
    simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ), ↑(x * y).num /ₚ ↑(x * y).pnatDen = ↑x.num /ₚ ↑x.pnatDen * (↑y.num /ₚ ↑y.pnatDen)

Tactic:
intro a b
      simp only [← divp_assoc, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq,
        pnatCast_eq_natCast, Rat.coe_pnatDen, Units.val_mul]
      trans (↑((a * b).num * a.den * b.den) : R)
      · simp_rw [Int.cast_mul, Int.cast_natCast]
        ring
      rw [Rat.mul_num_den' a b]
      simp

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

Goal state before:
pp: case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ ↑(z • a✝¹) = ↑(z • a✝) ↔ ∃ k, ⟦a✝¹⟧ = ↑(a✝ + ↑k • (p / ↑z))

Tactic:
QuotientAddGroup.eq_iff_sub_mem,

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • a✝¹ - z • a✝ ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - (a✝ + ↑k • (p / ↑z)) ∈ AddSubgroup.zmultiples p
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' ↔ x = x' ∧ s = s'

Tactic:
constructor
  · apply cons_injective2
  · intro ⟨_, _⟩
    congr

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

Goal state before:
pp: case nil.nil.right
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail

Tactic:
assumption

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
dsimp [Corec.f, destruct]

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ s.get? n = some a✝ ↔ nil.get? n = some a✝

Tactic:
le_stable _ (Nat.zero_le _) h

Goal state after:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ none = some a✝ ↔ nil.get? n = some a✝
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f none = none

Tactic:
assumption

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

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')

Tactic:
assumption

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

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ s.head :: take n s.tail ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
← take_succ,

Goal state after:
α : Type u
s : Stream' α
n : ℕ
⊢ take n.succ s ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n : ℕ
s : Seq α
⊢ (take 0 s)[n]? = if n < 0 then s.get? n else none

Tactic:
simp [take]

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
hle : ∀ (h : s.Terminates), 0 ≤ s.length h
⊢ (take 0 s).length = 0

Tactic:
simp [take]

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

Goal state before:
pp: case pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
fs : Computation β
⊢ match (fs.bind g).destruct, (fs.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp

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

Goal state before:
pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₁
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₁) x

Tactic:
RingHom.comp_apply,

Goal state after:
case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₁
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i) ((f' i₁ i h1) x) = (of G (fun i j h ↦ ⇑(f' i j h)) i₁) x
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₂
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₂) x

Tactic:
RingHom.comp_apply,

Goal state after:
case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₂
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i) ((f' i₂ i h2) x) = (of G (fun i j h ↦ ⇑(f' i j h)) i₂) x
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
by
  have := h; revert this
  generalize e : append s₁ s₂ = ss; intro h; revert s₁
  apply mem_rec_on h _
  intro b s' o s₁
  cases s₁ with
  | nil =>
    intro m _
    apply Or.inr
    simpa using m
  | cons c t₁ =>
    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.Computation

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
⊢ a ∈ c₁

Tactic:
let ⟨b, b1, ab⟩ := h2 a2

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ a ∈ c₁
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]
    rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]

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

Goal state before:
pp: case succ.inr.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]

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
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i : ι
g : G i
⊢ (ringEquiv G f') ((of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) g) = ⟦⟨i, g⟩⟧

Tactic:
simp [ringEquiv]

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

Goal state before:
pp: α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
⊢ (map f s₁).zip s₂ = map (Prod.map f id) (s₁.zip s₂)

Tactic:
convert! zip_map _ _ _ _
  simp

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

Goal state before:
pp: α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
⊢ s₁.zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)

Tactic:
convert! zip_map _ _ _ _
  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
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)
i j : ι
h : i ≤ j
⊢ ((g₂ j).comp (g₁ j)).comp (f i j h) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc]

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ map id (a, s) = (a, s)

Tactic:
simp [map]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
⊢ map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join

Tactic:
simp [map]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ map f (join ((a, Seq.cons x✝ s✝), S)) = (map (map f) ((a, Seq.cons x✝ s✝), S)).join

Tactic:
simp [map]

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

Goal state before:
pp: n : ℕ
ih : fib (n + 1) = ∑ k ∈ Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1

Tactic:
rw [ih, add_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i ∈ ?m.124, e' i = 0
h₆ : (∑ i ∈ ?m.124, e' i) * e₀ = 0
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin (n + 1)
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) i = e i
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 ↦ x * e

Tactic:
mem_corner_iff_mem_range_mul_left idem hc,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (r ∈ Set.range fun x ↦ e * x) ↔ r ∈ Set.range fun x ↦ x * e
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i

Tactic:
simp_rw [dvd_def, funext_iff, Classical.skolem]

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R R' := compHom R' (algebraMap R R[ε])
f' : R[ε] →ₐ[R] R' := { toRingHom := f, commutes' := ⋯ }
⊢ f = g

Tactic:
let g' : R[ε] →ₐ[R] R' :=
    { toRingHom := g
      commutes' r := (DFunLike.congr_fun h₀ r).symm }

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R R' := compHom R' (algebraMap R R[ε])
f' : R[ε] →ₐ[R] R' := { toRingHom := f, commutes' := ⋯ }
g' : R[ε] →ₐ[R] R' := { toRingHom := g, commutes' := ⋯ }
⊢ f = g