mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
rw [nhdsWithin_Ioo_eq_nhdsGT hab]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
y : G
y_mem : y ∈ u i
hy : ↑y = x b / x a
⊢ ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
refine
      ⟨y⁻¹ * g, by
        simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem, ?_⟩

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
y : G
y_mem : y ∈ u i
hy : ↑y = x b / x a
⊢ x a = ↑(y⁻¹ * g)
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual f.range.mkQ) c = 0

Tactic:
refine hf ?_

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual f) ((dual f.range.mkQ) c) = (dual f) 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
intro _ A a
    exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((Hom.hom ((μIso R X Y).hom ▷ (free R).obj Z))
          ((Hom.hom ((μIso R X Y).inv ▷ (free R).obj Z)) (freeMk ((x, y), z).1 ⊗ₜ[R] freeMk ((x, y), z).2)))) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          ((Hom.hom ((μIso R X Y).inv ▷ (free R).obj Z)) (freeMk ((x, y), z).1 ⊗ₜ[R] freeMk ((x, y), z).2))))

Tactic:
MonoidalCategory.whiskerRight_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((Hom.hom ((μIso R X Y).hom ▷ (free R).obj Z))
          ((ConcreteCategory.hom (μIso R X Y).inv) (freeMk ((x, y), z).1) ⊗ₜ[R] freeMk ((x, y), z).2))) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          ((ConcreteCategory.hom (μIso R X Y).inv) (freeMk ((x, y), z).1) ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((Hom.hom ((μIso R X Y).hom ▷ (free R).obj Z))
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2))) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
MonoidalCategory.whiskerRight_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((ConcreteCategory.hom (μIso R X Y).hom) (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2) ⊗ₜ[R]
          freeMk ((x, y), z).2)) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : γ ≫ homologyMap φ = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = π₁ ≫ 0

Tactic:
comp_zero

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : γ ≫ homologyMap φ = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ π₂ ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μ (free R) X Y)) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
by
  apply FreeMonoidal.μIso_hom_freeMk_tmul_freeMk

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0

Tactic:
by rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ π₁ ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.v₁₂.τ₂)
      ((ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) =
    (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
eq₁

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.v₁₂.τ₂) x₂ = (ConcreteCategory.hom D.L₂.f) x₁
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
hij' : i ≤ j
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest hij'

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
hij' : i ≤ j
k : ℕ
hk : i + k = j
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      have hij' := leOfHom hij
      simp only [Fin.mk_le_mk] at hij'
      obtain ⟨k, hk⟩ := Nat.le.dest hij'
      exact this k i j hk (by valid)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
x✝¹ x✝ : T.Algebra
f : (Monad.comparison T.adj).obj x✝¹ ⟶ (Monad.comparison T.adj).obj x✝
⊢ T.map f.f ≫ x✝.a = x✝¹.a ≫ f.f

Tactic:
by simpa using! f.h

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X✝ Y✝ : G.Coalgebra
f : (Comonad.comparison G.adj).obj X✝ ⟶ (Comonad.comparison G.adj).obj Y✝
⊢ X✝.a ≫ G.map f.f = f.f ≫ Y✝.a

Tactic:
by simpa using! f.h

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ ((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
      (coreflectorAdjunction R).toComonad.map (asIso ((coreflectorAdjunction R).counit.app X.A)).hom =
    (asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫ X.a

Tactic:
rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
        (coreflectorAdjunction R).toComonad.map (asIso ((coreflectorAdjunction R).counit.app X.A)).hom) ≫
      (coreflectorAdjunction R).counit.app X.A =
    ((asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫ X.a) ≫ (coreflectorAdjunction R).counit.app X.A
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
j : J✝
⊢ c.ι.app j ≫ m.f = c.ι.app j ≫ { f := t.desc (T.forget.mapCocone s), h := ⋯ }.f

Tactic:
simpa using congr_arg Algebra.Hom.f (J j)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ c.ι.app j ≫ t.desc (newCocone D c) ≫ T.δ.app c.pt =
    c.ι.app j ≫ t.desc (newCocone D c) ≫ T.map (t.desc (newCocone D c))

Tactic:
by
    simp only [Functor.comp_obj, forget_obj, IsColimit.fac_assoc,
      newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map]
    rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R
inst✝³ : MulSemiringAction M R
inst✝² : MulSemiringAction N R
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N R
x : M
y : N
z : Ideal R
⊢ (x • y) • z = x • y • z

Tactic:
by
    simp_rw [pointwise_smul_def, map_map]
    congr
    ext
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm ((I.inertiaEquiv e he) ((I.inertiaEquiv e he).symm n)) • x =
    (I.inertiaEquiv e he).symm n • x

Tactic:
(inertiaEquiv I e he).apply_symm_apply

Goal state after:
M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm n • x = (I.inertiaEquiv e he).symm n • x
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₂
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit ((Ideal.Quotient.mk J) x)
⊢ IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) x))

Tactic:
exact
      h₃.map
        ((DoubleQuot.quotQuotEquivQuotSup I J).trans
              (Ideal.quotEquivOfEq (sup_eq_right.mpr e))).symm.toRingHom

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
⊢ IsUnit ((mk (I ^ n)) x) ↔ x ∉ I

Tactic:
let := Ideal.Quotient.field I

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ IsUnit ((mk (I ^ n)) x) ↔ x ∉ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ mk' S a s * mk' S b t ∈ J

Tactic:
ha,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ x * mk' S b t ∈ J
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ invFun R A ((toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p

Tactic:
dsimp only [invFun]

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
p✝ : Submonoid R
inst✝¹³ : IsLocalization p✝ S
M : Type u_3
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : IsScalarTower R S M
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Flat A B
p : Ideal A
inst✝⁴ : p.IsPrime
P : Ideal B
inst✝³ : P.IsPrime
inst✝² : P.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p P
⊢ Module.Flat (Localization.AtPrime p) (Localization.AtPrime P)

Tactic:
by
  rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]
  exact Module.Flat.trans A B (Localization.AtPrime P)

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * (↑sx * ↑sy * ↑sz) ∈ P

Tactic:
rw [← ht]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * ((rx * ↑sy + ry * ↑sx) * rz) ∈ P
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_4
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y

Tactic:
rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ toLaurent ((monomial n) r) = C r * T ↑n

Tactic:
by simp [toLaurent]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
n : ℤ
⊢ T (-n) * T n = 1

Tactic:
by rw [← T_add, neg_add_cancel, T_zero]

Goal state after: