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

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (equiv x✝¹) (f h (↑t x✝)) = piLTProj h ((equiv x✝) (↑t x✝))

Tactic:
;

Goal state after:
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (equiv x✝¹) (f h (↑t x✝)) = piLTProj h ((equiv x✝) (↑t x✝))
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ (map (fun x ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ (map (fun x ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (G i)
inst✝⁵ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁴ : DecidableEq ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i✝ : ι
x✝ : G i✝
⊢ ((map g₂ hg₂ ∘ₗ map g₁ hg₁) ∘ₗ of R ι G f i✝) x✝ = (map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i✝) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (G i)
inst✝⁵ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁴ : DecidableEq ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i✝ : ι
x✝ : G i✝
⊢ ((map g₂ hg₂ ∘ₗ map g₁ hg₁) ∘ₗ of R ι G f i✝) x✝ = (map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i✝) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝ : ↑(Iio i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) t)) x✝ = ↑t x✝

Tactic:
;

Goal state after:
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝ : ↑(Iio i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) t)) x✝ = ↑t x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) t)) = ↑t

Tactic:
;

Goal state after:
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) t)) = ↑t
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝ : ↑(Iio i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) t)) x✝ = ↑t x✝

Tactic:
;

Goal state after:
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝ : ↑(Iio i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) t)) x✝ = ↑t x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj✝ : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ ((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨k, ⋯⟩) (f h t) =
    piLTProj h (((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨j, hj⟩) t)

Tactic:
;

Goal state after:
case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj✝ : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ ((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨k, ⋯⟩) (f h t) =
    piLTProj h (((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨j, hj⟩) t)
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯) ∘ₗ Module.of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ Module.of R ι G f i✝) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯) ∘ₗ Module.of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ Module.of R ι G f i✝) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv

Tactic:
;

Goal state after:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i : ↑s
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv i = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv i

Tactic:
;

Goal state after:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i : ↑s
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv i = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv i
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯) ∘ₗ of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯) ∘ₗ of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ of R ι G f i✝) x✝
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ AddMonoidHom.id (G x)) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ AddMonoidHom.id (G x)) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.refl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
case inl.refl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → G i →+ G' i
g₂ : (i : ι) → G' i →+ G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G f i✝)) x✝ = ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → G i →+ G' i
g₂ : (i : ι) → G' i →+ G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G f i✝)) x✝ = ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G f i✝)) x✝
Module: Mathlib.Data.DFinsupp.Small

Goal state before:
pp: ι : Type u
π : ι → Type v
inst✝² : (i : ι) → Zero (π i)
inst✝¹ : Small.{w, u} ι
inst✝ : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq : (fun x j ↦ x j) f = (fun x j ↦ x j) f'
j : ι
⊢ f j = f' j

Tactic:
;

Goal state after:
ι : Type u
π : ι → Type v
inst✝² : (i : ι) → Zero (π i)
inst✝¹ : Small.{w, u} ι
inst✝ : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq : (fun x j ↦ x j) f = (fun x j ↦ x j) f'
j : ι
⊢ f j = f' j
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case zero
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
m : ℕ
inst✝ : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

pp: case prime
σ : Type u
R : Type v
inst✝ : CommSemiring R
p m : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
;

Goal state after:
case zero
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
m : ℕ
inst✝ : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

case prime
σ : Type u
R : Type v
inst✝ : CommSemiring R
p m : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (MvPolynomial σ R) p
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : N
⊢ ((AlgebraTensorModule.curry (rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : N
⊢ ((AlgebraTensorModule.curry (rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g)) x✝¹) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
i✝ : ι
hj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
i✝ : ι
hj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝ ∈ restrictSupport R univ ↔ x✝ ∈ ⊤

Tactic:
;

Goal state after:
σ : Type u
R : Type v
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝ ∈ restrictSupport R univ ↔ x✝ ∈ ⊤
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩