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

Goal state before:
pp: R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
X Y : Type u_2
e : X ≃ Y
a✝ :
  ∀ {A : X → Type u_3} [inst : (i : X) → AddCommMonoid (A i)] [inst_1 : (i : X) → Module R (A i)]
    [inst_2 : (i : X) → TopologicalSpace (A i)] [∀ (i : X), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : X) → A i)
A : Y → Type u_3
inst✝³ : (i : Y) → AddCommMonoid (A i)
inst✝² : (i : Y) → Module R (A i)
inst✝¹ : (i : Y) → TopologicalSpace (A i)
inst✝ : ∀ (i : Y), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Y) → A i)

Tactic:
exact .iso (ContinuousLinearEquiv.piCongrLeft R A e)

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : WithOne α →* β
hf : Function.Injective ⇑f
x✝¹ x✝ : α
⊢ (lift.symm f) x✝¹ = (lift.symm f) x✝ → x✝¹ = x✝

Tactic:
by simp [hf.eq_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j : J
⊢ s.π.app j ≫ (F.obj j).hom = (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).obj j).hom

Tactic:
obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
hik : k ⟶ i
hjk : k ⟶ j
⊢ s.π.app j ≫ (F.obj j).hom = (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).obj j).hom
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
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map (γ ≫ minToRight i₀ j)

Tactic:
F.map_comp,

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
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β ≫ F.map δ = F.map (rightToMax i₀ j ≫ γ)

Tactic:
F.map_comp,

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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β ≫ F.map δ = F.map (rightToMax i₀ j) ≫ F.map γ
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j ≫ γ) =
    F.map (rightToMax i₀ j) ≫ F.map γ

Tactic:
F.map_comp,

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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j) ≫ F.map γ =
    F.map (rightToMax i₀ j) ≫ F.map γ
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
heq : Y.hom = hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ MorphismProperty.structuredArrowObj L P Y

Tactic:
rw [P.structuredArrowObj_iff, heq, ← (hc _).lift_comp_conePointUniqueUpToIso_hom hd,
      P.cancel_right_of_respectsIso]

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
heq : Y.hom = hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ P ((hc (d.diag ⋙ proj X L ⋙ L)).lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } })
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✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ CreatesColimitsOfShape (Discrete PEmpty.{1}) (Under.forget P ⊤ X)

Tactic:
by
  apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed
  · exact inferInstanceAs (HasColimitsOfShape _ (Under X))
  · apply Under.closedUnderColimitsOfShape_discrete_empty _

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ Hom.hom (Under.Hom.right h') =
    (Hom.hom
          (Under.Hom.right
            ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
      (Hom.hom
        (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
          ofHom
            (RingHom.id
              ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                  (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))

Tactic:
ext x <;> rfl

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
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ U ↔ x ∈ V

Tactic:
rw [← mem_restrictScalars K, H, mem_restrictScalars]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : Fin z.natAbs
n : ℤ
h : (z * n + ↑↑k) • p = z • r
⊢ ∃ k, k • p = z • r

Tactic:
exact ⟨_, h⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n✝ : ℕ
n' : (↑s).tail n✝ = none
⊢ (↑s).tail (n✝ + 1) = none

Tactic:
obtain ⟨f, al⟩ := s
    exact al n'

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

Goal state before:
pp: case succ
α : 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
s : Seq α
e : some a = ↑s (k + 1)
⊢ C s

Tactic:
| succ k IH =>

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

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n

Tactic:
induction n with
  | zero => simpa [take] using h 1
  | succ n =>
    have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
    injection h₁

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

Goal state before:
pp: α : Type u
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)

Tactic:
simp only [ofStream, cons]

Goal state after:
α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ s.inits.tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
unfold inits
    rw [inits_core_eq]; rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ map f s

Tactic:
← bind_pure

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
← bind_pure

Goal state after:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (map f s).Terminates

Tactic:
← bind_pure

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates
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 (s1.bind (pure ∘ f1)) (map f2 s2)

Tactic:
← bind_pure

Goal state after:
α : 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 (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
injection oe with h'

Goal state after:
case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Data.Seq.Basic

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

pp: case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x✝ s✝) S).join.destruct (cons a ((cons x✝ s✝).append S.join)).destruct

Tactic:
· simp [join_cons_nil]

Goal state after:
case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x✝ s✝) S).join.destruct (cons a ((cons x✝ s✝).append S.join)).destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
n : ℕ
h_not_terminated : ¬s.TerminatedAt n
⊢ (s.set n x).get? n = some x

Tactic:
by
  simpa [set, update, ← Option.ne_none_iff_exists'] using! h_not_terminated

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : Pairwise R tl
⊢ Pairwise R (Seq.cons hd tl)

Tactic:
simp only [Pairwise] at *
  intro i j h_ij x hx y hy
  cases j with
  | zero => simp at h_ij
  | succ k =>
    simp only [get?_cons_succ] at hy
    cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

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

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ R hd tl_hd ∧ ∀ a ∈ tl_tl, R hd a

Tactic:
exact ⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩

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

Goal state before:
pp: case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Tactic:
rintro (_ | _) n' ih <;>
      simp only [fastFibAux_bit_false, fastFibAux_bit_true, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk_inj] <;>
      simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

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

Goal state before:
pp: case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
← h,

Goal state after:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred.succ + m)) = (fib m).gcd (fib n.pred.succ)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)

Tactic:
rcases map g (f a) with ⟨⟨a, s⟩, S⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s✝ : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
⊢ (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ IntFractPair.of v = ifp_n

Tactic:
by injection nth_stream_eq

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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
⊢ ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b

Tactic:
have : (fib (n + 2) : K) ≤ nextConts.b :=
      fib_le_of_contsAux_b (Or.inr not_terminatedAt_n)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
this : ↑(fib (n + 2)) ≤ nextConts.b
⊢ ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ CompleteOrthogonalIdempotents e ↔ (Pairwise fun x1 x2 ↦ e x1 * e x2 = 0) ∧ ∑ i, e i = 1

Tactic:
by
  rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp]
  intro ⟨ortho, complete⟩ i
  apply_fun (e i * ·) at complete
  rwa [Finset.mul_sum, Finset.sum_eq_single i (fun _ _ ne ↦ ortho ne.symm) (by simp at ·), mul_one]
    at complete

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Tactic:
subst hi; simp [hij]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 ↦ IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ f x - f e' = 0

Tactic:
hx',

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 ↦ IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ f e' - f e' = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i j : n
⊢ (matrix n c) (single i j x) (single i j y)

Tactic:
rwa [matrix_apply_single]

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
hμ : f.HasUnifEigenvalue μ 1
⊢ μ ∈ spectrum R f

Tactic:
by
  refine spectrum.mem_iff.mpr fun h_unit ↦ ?_
  set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
  rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩
  refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))
  rw [hv.apply_eq_smul, sub_self]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ { carrier := Set.range fun x ↦ e * x * e, mul_mem' := ⋯ } ↔ r ∈ Set.range fun x ↦ e * x

Tactic:
mem_mk,

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 * e) ↔ r ∈ Set.range fun x ↦ e * x
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (fun x ↦ e * x * e) (a + b) = (fun x ↦ e * x * e) a + (fun x ↦ e * x * e) b

Tactic:
simp_rw [mul_add, add_mul]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
⊢ e i * ↑(r i) * e i = ↑(r i)

Tactic:
have ⟨r', eq⟩ := (r i).2
      rw [← eq]; simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ ((lift fe).comp (inlAlgHom R A A)).range ⊔ adjoin R (⇑(lift fe) '' {ε}) = Subalgebra.map (↑fe).1 ⊤ ⊔ R[(↑fe).2]

Tactic:
Set.image_singleton,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ ((lift fe).comp (inlAlgHom R A A)).range ⊔ R[(lift fe) ε] = Subalgebra.map (↑fe).1 ⊤ ⊔ R[(↑fe).2]
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
⊢ 0 * a = 0

Tactic:
rwa [left_eq_add] at this

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

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
⊢ a * 0 = 0

Tactic:
rwa [left_eq_add] at this

Goal state after: