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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
⊢ IsLimit (F.interUnionPullbackCone U V)

Tactic:
have hι : U ⊔ V = iSup ι := by
    ext
    rw [Opens.coe_iSup, Set.mem_iUnion]
    constructor
    · rintro (h | h)
      exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
    · rintro ⟨⟨_ | _⟩, h⟩
      exacts [Or.inl h, Or.inr h]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
⊢ IsLimit (F.interUnionPullbackCone U V)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ

Tactic:
nth_rw 2 [← induced_id (t := τ)]

Goal state after:
case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = TopologicalSpace.induced id τ
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (↑f * f.inv) x = x

Tactic:
rw [f.val_inv]
          simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
x✝² : (coyoneda.obj (op X) ⋙ uliftFunctor.{t, v₁}).IsCardinalAccessible κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J (coyoneda.obj (op X))

Tactic:
have := Functor.preservesColimitsOfShape_of_isCardinalAccessible
    (coyoneda.obj (op X) ⋙ uliftFunctor.{t}) κ J

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
x✝² : (coyoneda.obj (op X) ⋙ uliftFunctor.{t, v₁}).IsCardinalAccessible κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J (coyoneda.obj (op X) ⋙ uliftFunctor.{t, v₁})
⊢ PreservesColimitsOfShape J (coyoneda.obj (op X))
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
⊢ Cocone F

Tactic:
let c₁ := cocone (F ⋙ Prod.fst _ _) hC
    let c₂ := cocone (F ⋙ Prod.snd _ _) hC
    exact
      { pt := (c₁.pt, c₂.pt)
        ι.app i := (c₁.ι.app i, c₂.ι.app i)
        ι.naturality {i j} f := by
          ext
          · simpa using c₁.w f
          · simpa using c₂.w f }

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

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

Tactic:
← tmul_sum

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
have := sub_eq_zero.mpr (hy₁.trans hy₂.symm)

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
this : f₂ y₁ - f₂ y₂ = 0
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
⊢ (MorphismProperty.costructuredArrowObj L P).limitsOfShape WalkingCospan ≤ MorphismProperty.costructuredArrowObj L P

Tactic:
rintro Y ⟨pres, hpres⟩
    have h : IsPullback (L.map (pres.π.app .left).left) (L.map (pres.π.app .right).left)
        (L.map (pres.diag.map WalkingCospan.Hom.inl).left)
          (L.map (pres.diag.map WalkingCospan.Hom.inr).left) :=
      IsPullback.of_isLimit_cone <| isLimitOfPreserves
        (CategoryTheory.CostructuredArrow.toOver L X ⋙ CategoryTheory.Over.forget X) pres.isLimit
    rw [MorphismProperty.costructuredArrowObj_iff]
    rw [show Y.hom = L.map (pres.π.app .left).left ≫ (pres.diag.obj .left).hom by simp]
    apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hpres _)
    exact P.of_postcomp _ (pres.diag.obj WalkingCospan.one).hom (hpres .one)
      (by simpa using hpres .right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasLimitsOfShape (Discrete PEmpty.{1}) (Comma (𝟭 T) (Functor.fromPUnit X))

Tactic:
exact inferInstanceAs (HasLimitsOfShape _ (Over X))

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
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
let hc : IsLimit c := Under.equalizerForkIsLimit f g

Goal state after:
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
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
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
⊢ tensorKerInv S M f ∘ₗ tensorKer S M f = id

Tactic:
by
      ext m x
      apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype
        (ker f).injective_subtype)
      simp

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

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o 0 = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'

Tactic:
change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
⊢ (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s

Tactic:
by rw [Nat.zero_min, take_zero, List.take_nil]

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

Goal state before:
pp: case think
α : 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 : Computation α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g)
    ((s.think.bind f).bind g).destruct (s.think.bind fun x ↦ (f x).bind g).destruct

Tactic:
simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b).destruct

Tactic:
rw [mem_unique (ret_mem _) mb]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b').destruct
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 ι
i : ι
x : G i
hix : (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) x = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
have := Nonempty.intro i

Goal state after:
ι : 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 ι
i : ι
x : G i
hix : (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) x = 0
this : Nonempty ι
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
rcases exists_add_of_le hn with ⟨n, rfl⟩
  rw [← tsub_pos_iff_lt, add_comm 2, add_right_comm, fib_add_two, add_tsub_cancel_right, fib_pos]
  exact succ_pos n

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : g.convs (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) =
    ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')

Tactic:
obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
          simp [*, g', pA, pB, ppA, ppB, pA', pB', ppA', ppB',
            (contsAux_eq_contsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
            (contsAux_eq_contsAux_squashGCF_of_le n'.le_succ).symm]
        symm
        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
⊢ ∑ i, idempotent V i = 1

Tactic:
by
    apply (decompose V).injective
    refine DFunLike.ext _ _ fun i ↦ ?_
    rw [decompose_sum, DFinsupp.finsetSum_apply]
    simp [idempotent, of_apply]

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

Goal state before:
pp: case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
calc
        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Tactic:
rw [roots, map_toPoly]

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

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

Tactic:
exact le_of_succ_get?_den nth_partDen_eq

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
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
have : Directed (ι := { i : ℕ // i ≤ k }) (· ≤ ·) fun i ↦ LinearMap.ker ((f - μ • 1) ^ (i : ℕ)) :=
    Monotone.directed_le fun m n h ↦ by simpa using (f - μ • 1).iterateKer.monotone h

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
⊢ (trace R M) ⁅f, g⁆ = 0

Tactic:
by
  rw [Ring.lie_def, map_sub, trace_mul_comm]
  exact sub_self _

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

Goal state before:
pp: 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
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Submodule.map ((f - μ • 1) ^ finrank K V)
      (⊤ ⊓ Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V))) ≤
    ⊥

Tactic:
top_inf_eq,

Goal state after:
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
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Submodule.map ((f - μ • 1) ^ finrank K V)
      (Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V))) ≤
    ⊥
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_6
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
M : Type u_7
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
e : M →ₗ[R] M
he : IsIdempotentElem e
inst✝³ : Free R ↥e.range
inst✝² : Module.Finite R ↥e.range
inst✝¹ : Free R ↥e.ker
inst✝ : Module.Finite R ↥e.ker
⊢ ↑(finrank R ↥e.range) = 0 ↔ e = 0

Tactic:
Nat.cast_eq_zero,

Goal state after:
R : Type u_6
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
M : Type u_7
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
e : M →ₗ[R] M
he : IsIdempotentElem e
inst✝³ : Free R ↥e.range
inst✝² : Module.Finite R ↥e.range
inst✝¹ : Free R ↥e.ker
inst✝ : Module.Finite R ↥e.ker
⊢ finrank R ↥e.range = 0 ↔ e = 0
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 - ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ ρ : R
⊢ (f + -(ρ • LinearMap.id)).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)
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
⊢ (ρ • LinearMap.id - f).HasEigenvalue μ ↔ f.HasEigenvalue (ρ - μ)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ ρ : R
⊢ (ρ • LinearMap.id + -f).HasEigenvalue μ ↔ f.HasEigenvalue (ρ - μ)
Module: Mathlib.Algebra.Field.GeomSum

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

Tactic:
by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1

Tactic:
by
        rw [mul_inv_cancel, mul_one, mul_inv_cancel]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).toWord = List.replicate n (a, true)

Tactic:
rw [of, pow_mk, List.flatten_replicate_singleton, toWord]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ #(MonoidAlgebra R (FreeMonoid X)) = 1

Tactic:
mk_eq_one

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ 1 = 1
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : α
xs : List α
this : ∀ (x : FreeMonoid α), List.foldl (fun x1 x2 ↦ x1 * x2) x (List.map FreeMonoid.of xs) = x * ofList xs
⊢ toFreeMonoid { head := x, tail := xs } = ofList (x :: xs)

Tactic:
simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : α
xs : List α
y : α
ys : List α
h : toFreeMonoid { head := x, tail := xs } = toFreeMonoid { head := y, tail := ys }
⊢ { head := x, tail := xs } = { head := y, tail := ys }

Tactic:
simp only [toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq] at h

Goal state after:
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h : x :: xs = y :: ys
⊢ { head := x, tail := xs } = { head := y, tail := ys }