mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Injective ⇑(f.prod g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
this : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Surjective ⇑(f.prod g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
ha₀ : a ≠ 0
⊢ a = 0 → Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q✝ : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
x✝ : { q // IsCompl p q }
q : Submodule R E
hq : IsCompl p q
⊢ (fun f ↦ ⟨(↑f).ker, ⋯⟩) ((fun q ↦ ⟨p.projectionOnto ↑q ⋯, ⋯⟩) ⟨q, hq⟩) = ⟨q, hq⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
⊢ g' (τ₂ x₂) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
i : ι
⊢ a + f i ≤ a + ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x : E
⊢ ↑f x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x✝ : ↥p
x : E
hx : x ∈ p
⊢ ↑((codRestrict p ↑f ⋯) ↑⟨x, hx⟩) = ↑⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
⊢ (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // ∀ (x : ↥p), f ↑x = x }
x : E
⊢ (p.subtype ∘ₗ ↑f * p.subtype ∘ₗ ↑f) x = (p.subtype ∘ₗ ↑f) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsIdempotentElem f
x : M
x✝ : x ∈ f.range
y : M
hy : f y = x
⊢ f x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ IsProj f.range f ↔ IsIdempotentElem f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) ↔ IsIdempotentElem f

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ h.codRestrict ↑x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₁₂ : f'.comp τ₁ = τ₂.comp f
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
⊢ MulExact ⇑f ⇑g ↔ MulExact ⇑f' ⇑g'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p f.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Exact ⇑Q.subtype ⇑Q.mkQ

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_8
inst✝⁶ : Ring R
M : Type u_12
N : Type u_13
P : Type u_14
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommMonoid P
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : Module R P
f : M →ₗ[R] N
⊢ Exact ⇑0 ⇑f ↔ Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_8
N : Type u_9
P : Type u_10
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommMonoid P
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : Module R P
f : M →ₗ[R] N
⊢ Exact ⇑f ⇑0 ↔ Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
f : ι → ℕ∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Exact ⇑f ⇑g

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
x : ℕ∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid N'
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid P'
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
inst✝³ : Module R N
inst✝² : Module R N'
inst✝¹ : Module R P
inst✝ : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃
H : Exact ⇑f₁₂ ⇑f₂₃
⊢ Exact ⇑g₁₂ ⇑g₂₃

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯).symm

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
m₁ m₂ : Submodule S M
hf₁ : IsProj m₁ f
hf₂ : IsProj m₂ f
⊢ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
⊢ ∀ x ∈ ⊥, 0 x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : ι → Sort u_4
f : (i : ι) → κ i → ℕ∞
⊢ a + ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a + f i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : ι → Sort u_4
f : (i : ι) → κ i → ℕ∞
⊢ (⨅ i, ⨅ j, f i j) + a = ⨅ i, ⨅ j, f i j + a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
by
  rw [sInf_eq_iInf, add_iInf₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊤ ↔ f = id

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : M × P
e : f x.1 + ↑l x.2 = f y.1 + ↑l y.2
this : x.2 = y.2
⊢ f x.1 = f y.1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊥ ↔ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.range), T.range.subtype u = T ↑u

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.ker), 0 u = T ↑u

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = T.range.projection T.ker ⋯

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.dom = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.cod = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : R.dom = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : R.cod = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
⊢ dom Set.univ = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ cod Set.univ = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
⊢ SetRel.id.inv = SetRel.id

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : SetRel α β
S : SetRel β γ
t : SetRel γ δ
⊢ R ○ S ○ t = R ○ (S ○ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R ○ SetRel.id = R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ SetRel.id ○ R = R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
⊢ (R ○ S).inv = S.inv ○ R.inv

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ ∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ ∅ ○ S = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ Set.univ = {(a, _c) | a ∈ R.dom}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ Set.univ ○ S = {(_b, c) | c ∈ S.cod}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : SetRel α β
S : ι → SetRel β γ
⊢ R ○ ⋃ i, S i = ⋃ i, R ○ S i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : ι → SetRel α β
S : SetRel β γ
⊢ (⋃ i, R i) ○ S = ⋃ i, R i ○ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
𝒮 : Set (SetRel β γ)
⊢ R ○ ⋃₀ 𝒮 = ⋃ S ∈ 𝒮, R ○ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : N
⊢ g (x - ↑l (g x)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : N
⊢ g (x - ↑l (g x)) = 0

Tactic:
by simp [h₁, g.map_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ p.range = q.range ∧ p.ker = q.ker

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ℛ : Set (SetRel α β)
S : SetRel β γ
⊢ ⋃₀ ℛ ○ S = ⋃ R ∈ ℛ, R ○ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t₁ t₂ : Set β
ht : (t₁ ∩ t₂).Nonempty
s : Set α
u : Set γ
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
E : Type u_7
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
x : E
hx : x ∈ (id - p).ker
⊢ p x = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
E : Type u_7
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
⊢ p.ker = (id - p).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : N
y : M
hy : f y = x - ↑l (g x)
⊢ (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) (y, g x) = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_7
inst✝³ : AddCommGroup M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : M →ₗ[S] E
⊢ p ∘ₗ q = p ↔ q.ker ≤ p.ker

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image ∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = (p.prodEquivOfIsCompl f.ker ⋯).conj (id.prodMap 0)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage ∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image Set.univ = R.cod

Tactic:
by

Goal state after: