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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
G : Presheaf C X
f : F.obj ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f))
s t : CC (F.obj.obj (op U))
hst : (ConcreteCategory.hom (f.app (op U))) s = (ConcreteCategory.hom (f.app (op U))) t
x : ↑X
hx : x ∈ U
⊢ (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) s) =
    (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) t)

Tactic:
hst

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
G : Presheaf C X
f : F.obj ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f))
s t : CC (F.obj.obj (op U))
hst : (ConcreteCategory.hom (f.app (op U))) s = (ConcreteCategory.hom (f.app (op U))) t
x : ↑X
hx : x ∈ U
⊢ (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) t) =
    (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) t)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ 1 x = x

Tactic:
one_apply_eq_self

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ x = x
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T (↑T⁻¹ x) = x

Tactic:
rw [← mul_apply_eq_comp, Units.mul_inv, one_apply_eq_self]

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

Tactic:
obtain ⟨z, hz⟩ := (Submodule.Quotient.eq _).mp 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
z : ↑S.X₁.toModuleCat
hz : ↑(Hom.hom S.f) z = y - x
⊢ (ConcreteCategory.hom S.g) x = 0
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
A : C
J : Type w
x✝³ : SmallCategory J
x✝² : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
x✝¹ : J
x✝ : ⋯.some ⟶ x✝¹
⊢ IsIso ((F ⋙ (const C).obj A).map x✝)

Tactic:
by dsimp; infer_instance

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

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

pp: 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) ⋯)) ⋯)

Tactic:
· simpa using! congr(($e₁).right)

Goal state after:
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.MixedCharZero

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

Tactic:
intro I hI

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)
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'
h : (fun a' ↦ (a', tail ⟨f, al⟩)) <$> some a' = some (a, s')
⊢ ⟨f, al⟩ = cons a s'

Tactic:
injections _ h1 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 s'
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 (tail ⟨f, al⟩))

Tactic:
dsimp [tail, cons]

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 = some a :: f.tail
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]
      apply think

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

Goal state before:
pp: case mp
α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates → s.Terminates

Tactic:
intro ⟨n, h⟩

Goal state after:
case mp
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x : α
s : Seq α
⊢ s.Terminates → (cons x s).Terminates

Tactic:
intro ⟨n, h⟩

Goal state after:
case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates
Module: Mathlib.Data.Seq.Defs

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

Tactic:
| cons b s' =>

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

Goal state before:
pp: case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1

pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
· simp [length'_of_terminates h, length'_of_terminates h', length_cons h']

Goal state after:
case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by_cases h : s.Terminates

Goal state after:
case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by_cases h : s.Terminates

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

case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
⊢ x ∈ take n s

Tactic:
obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
    rw [← hl, take, head_eq_some h_get]
    simp

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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ ((cons a s).append t).destruct = some (a, s.append t)

Tactic:
by
    dsimp [append]; rw [corec_eq]
    dsimp [append]; rw [destruct_cons]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
⊢ ∏ i ∈ Finset.range (n + 1), -1 = (-1) ^ (n + 1)

Tactic:
Finset.prod_const,

Goal state after:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
⊢ (-1) ^ (Finset.range (n + 1)).card = (-1) ^ (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
c₂ : Computation α
⊢ ((pure a).orElse fun x ↦ c₂).destruct = Sum.inl a

Tactic:
simp [orElse]

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

Goal state before:
pp: α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think.orElse fun x ↦ pure a).destruct = Sum.inl a

Tactic:
simp [orElse]

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

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think.orElse fun x ↦ c₂.think).destruct = Sum.inr (c₁.orElse fun x ↦ c₂)

Tactic:
simp [orElse]

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

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map id) s = s

Tactic:
rw [Option.map_id, Stream'.map_id]

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

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

Tactic:
by apply Subtype.ext; dsimp [tail, map]

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

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
⊢ (map f s).length' = s.length'

Tactic:
by_cases h : (s.map f).Terminates

Goal state after:
case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).length' = s.length'

case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Basic

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

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

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
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Monoid α
inst✝⁴ : Monoid β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a b : α
c d : β
hab : a ∣ b
hcd : c ∣ d
⊢ a • c ∣ b • d

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hab, hcd

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Monoid α
inst✝⁴ : Monoid β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
c : β
x : α
y : β
⊢ a • c ∣ (a * x) • (c * y)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝

Tactic:
obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx

Goal state after:
case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
w✝ : α
left✝ : w✝ ∈ s
hx' : f w✝ = x✝
⊢ p x✝
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
⊢ v = (of v).convs (n + 1 - 1)

Tactic:
let g := of v
    change v = g.convs n
    obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
    · cases n with
      | zero => contradiction
      | succ n' =>
        -- IntFractPair.stream v 0 ≠ none
        have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
        have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
        rw [this]
        exact IH nth_stream_eq_none
    · simpa [nth_stream_fr_eq_zero, compExactValue] using!
        compExactValue_correctness_of_stream_eq_some nth_stream_eq

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

Goal state before:
pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
obtain ⟨ppred_conts, ppred_conts_eq⟩ :=
            IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1

Goal state after:
case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]

Goal state after:
case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ IntFractPair.of q = ifp_zero

Tactic:
injection stream_zero_eq

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ (fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) ((fun P ↦ ⟨P.toPoly, ⋯⟩) P) =
    P

Tactic:
by ext <;> simp only [coeffs]

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
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ g.partDens.get? n = none

Tactic:
by rwa [Stream'.Seq.TerminatedAt] at terminated

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}
⊢ ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
and_self_iff,

Goal state after:
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}
⊢ ((P.a ≠ 0 ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f - μ • 1) ^ n).ker ≤ ((f - μ • 1) ^ finrank K V).ker

Tactic:
apply ker_pow_le_ker_pow_finrank

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ ∀ (i : { l // ↑l ≤ k }) (i_1 : { l_1 // ↑l_1 ≤ l }), Disjoint ((f.genEigenspace μ₁) ↑↑i) ((f.genEigenspace μ₂) ↑↑i_1)

Tactic:
rintro ⟨k, -⟩ ⟨l, -⟩

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
⊢ Disjoint ((f.genEigenspace μ₁) ↑↑⟨k, property✝¹⟩) ((f.genEigenspace μ₂) ↑↑⟨l, property✝⟩)
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    simp_rw [Finset.prod_insert has]
    exact (Rat.mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (C g.leadingCoeff + r).leadingCoeff ∈ P

Tactic:
leadingCoeff,

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (C g.leadingCoeff + r).coeff (C g.leadingCoeff + r).natDegree ∈ P