mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g✝¹ : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) ((f i j hij) x) = (g✝¹ i) x
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
hg : ∀ (i j : ι) (h : i ≤ j), g✝ j ∘ₗ f i j h = f' i j h ∘ₗ g✝ i
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of R ι G' f' i) ((g✝ i) g) = (of R ι G' f' i) ((g✝ i) g)

Tactic:
]

Goal state after:
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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
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 j : ι
h : i ≤ j
⊢ f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i = f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i

Tactic:
]

Goal state after:
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✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ piLTProj h ((equiv ⟨↑x✝, ?hj⟩) ((fun l ↦ (equiv l).symm (↑t l)) x✝)) = piLTProj h (↑t x✝)

pp: case hj
ι✝ : 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✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ ↑x✝ ∈ Iio i

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✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ piLTProj h ((equiv ⟨↑x✝, ?hj⟩) ((fun l ↦ (equiv l).symm (↑t l)) x✝)) = piLTProj h (↑t x✝)

case hj
ι✝ : 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✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ ↑x✝ ∈ Iio 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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
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
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h

Tactic:
]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

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

Tactic:
Equiv.trans_apply

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

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

Tactic:
]

Goal state after:
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
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h

Tactic:
]

Goal state after:
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✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_1.inr
ι : 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
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ piLTProj ⋯ ((e₂ ⟨i⁺, ?m.195⟩) x) ⟨↑⟨j, hj✝⟩, hj⟩ = (e₂ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩

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
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ i⁺ ∈ s

Tactic:
]

Goal state after:
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)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g✝¹ : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) ((f i j hij) x) = (g✝¹ i) x
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
hg : ∀ (i j : ι) (h : i ≤ j), (g✝ j).comp (f i j h) = (f' i j h).comp (g✝ i)
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of G' f' i) ((g✝ i) g) = (of G' f' i) ((g✝ i) g)

Tactic:
]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_2
ι : 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
i : ι
lim : IsSuccPrelimit i
ih : ∀ b < i, ∀ (h : b ∈ s), e₁ ⟨b, h⟩ = e₂ ⟨b, h⟩
hi : i ∈ s
x : F ↑⟨i, hi⟩
j : ↑(Iio ↑⟨i, hi⟩)
k : ι
hjk : ↑j < k
hki : k < i
hk : k ∈ s
⊢ (e₂ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩ = (e₂ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩

Tactic:
]

Goal state after:
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)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
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 j : ι
h : i ≤ j
⊢ (f'' i j h).comp ((g₂ i).comp (g₁ i)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict).range = (lTensor Q g.range.subtype).range

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict).range = (lTensor Q g.range.subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(lTensor Q g.rangeRestrict)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(lTensor Q g.rangeRestrict)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(lTensor A g)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(lTensor A g)
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharP R p
n : ℕ
⊢ p ∣ n ↔ p ∣ n

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : x = y
⊢ x = y

Tactic:
]

Goal state after:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : x = y
⊢ x = y
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
classical
  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict).range = (rTensor Q g.range.subtype).range

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict).range = (rTensor Q g.range.subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(rTensor Q g.rangeRestrict)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(rTensor Q g.rangeRestrict)
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R t)

Tactic:
]

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R 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
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.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
hfg : Exact ⇑f ⇑g
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
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)
inst✝ : InverseSystem f
equivLim : F i ≃ ↑(limit f i)
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
i✝ : ι
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)
⊢ 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)
inst✝ : InverseSystem f
equivLim : F i ≃ ↑(limit f i)
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
i✝ : ι
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)