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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
⊢ R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
s : ι → Set α
⊢ R.image (⋃ i, s i) = ⋃ i, R.image (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
S : Set (Set α)
⊢ R.image (⋃₀ S) = ⋃ s ∈ S, R.image s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
t : ι → Set β
⊢ R.preimage (⋃ i, t i) = ⋃ i, R.preimage (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
T : Set (Set β)
⊢ R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.image s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.preimage s = 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 α β
S : SetRel β γ
s : Set α
⊢ (R ○ S).image s = S.image (R.image s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T

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 β γ
u : Set γ
⊢ (R ○ S).preimage u = R.preimage (S.preimage u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ ∅.image s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅.preimage t = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
⊢ image Set.univ s = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ preimage Set.univ t = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
h : R.dom ⊆ s
⊢ R.image s = R.cod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
h : R.cod ⊆ t
⊢ R.preimage t = R.dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image (s ∩ R.dom) = R.image s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
h : Commute f T
⊢ f * (T * f) = T * f ∧ f * (T * f) = f * T

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage (t ∩ R.cod) = R.preimage t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ s ∩ R.dom ⊆ R.preimage (R.image s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ t ∩ R.cod ⊆ R.image (R.preimage t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image s = ⋃ x ∈ s, {y | (x, y) ∈ R}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage t = ⋃ y ∈ t, {x | (x, y) ∈ R}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: β : Type u_2
t : Set β
⊢ SetRel.id.core t = t

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 β γ
u : Set γ
⊢ (R ○ S).core u = R.core (S.core u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
t : Set β
⊢ R.image s ⊆ t ↔ s ⊆ R.core t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsRefl
⊢ SetRel.id ⊆ R

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
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsRefl
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsRefl

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
S : SetRel β β
R : SetRel α β
inst✝ : S.IsRefl
⊢ R ⊆ R ○ S

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hT : IsUnit T
hf : IsIdempotentElem f
⊢ Commute f T ↔ map T f.range = f.range ∧ map T f.ker = f.ker

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α α
inst✝ : R.IsRefl
S : SetRel α β
⊢ S ⊆ R ○ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
⊢ ∃ x, s = {x} ∧ t = {x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsSymm
⊢ R.inv = R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
hR : R.inv = R
a b : α
hab : (a, b) ∈ R
⊢ (b, a) ∈ R

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst✝ : R.IsSymm
⊢ R.inv.IsSymm

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ ∅ → (x✝, x✝¹) ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x y : RelSeries r
length_eq : x.length = y.length
⊢ x.length + 1 = y.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x y : RelSeries r
length_eq : x.length = y.length
toFun_eq : x.toFun = y.toFun ∘ Fin.cast ⋯
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.IsTrans
x : RelSeries r
i j : Fin (x.length + 1)
h : i ≤ j
x✝ : i = j
⊢ x.toFun i = x.toFun j

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).toList = [x]

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ i < x.length

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x.toList

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
⊢ ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).length = x.length

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ Set.univ → (x✝, x✝¹) ∈ Set.univ

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
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsSymm
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsSymm

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst✝ : R.IsSymm
⊢ ∀ (a b : β), (a, b) ∈ Prod.map f f '' R → (b, a) ∈ Prod.map f f '' R

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
⊢ ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).toFun = x.toFun ∘ Fin.cast ⋯

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝¹ a₁ a₂ : α
b✝ : β
c✝¹ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a✝ b c✝ a c : α
⊢ (a, c) ∈ R ○ R.inv → (c, a) ∈ R ○ R.inv

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst✝ : R.IsSymm
⊢ (R ○ R).IsSymm

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
n : ℕ
hn1 : n < (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).length
x✝ : n < (↑x).length
⊢ (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).get ⟨n, hn1⟩ = (↑x).get ⟨n, x✝⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ R.preimage s = R.image s

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
⊢ (fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ Nonempty α

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ ∅ → (x✝¹, x✝) ∈ ∅ → (x✝², x✝) ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ s.toList ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.length + 1 = 1

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ Set.univ → (x✝¹, x✝) ∈ Set.univ → (x✝², x✝) ∈ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
⊢ {x | x ∈ s}.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
⊢ s.toFun 0 ∈ {x | x ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
⊢ s.toFun 1 ∈ {x | x ∈ s}

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
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
x : α × α
x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ {x} → (x✝¹, x✝) ∈ {x} → (x✝², x✝) ∈ {x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ 0 < s.length

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
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsTrans
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsTrans

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Injective graph

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
⊢ graph (f ∘ g) = graph g ○ graph f

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ s.length = 0 ↔ {x | x ∈ s}.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).head = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.graph ⇑f.symm = (Function.graph ⇑f).inv

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).last = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toList.head ⋯ = p.head

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ i < p.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ p.toList[i] = p.toFun ⟨i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
⊢ (fromListIsChain l l_ne_nil hl).head = l.head l_ne_nil

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
⊢ p.toList ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toList.getLast ⋯ = p.last

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ ∀ (y : α → β), (fun f ↦ Function.graph f = R) y → y = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ p.length + q.length + 1 + 1 = p.length + 1 + (q.length + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
⊢ p.length + 1 ≤ p.length + q.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∃! f, Function.graph f = R) ↔ ∀ (a : α), ∃! b, (a, b) ∈ R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = (Function.graph f).image s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).preimage s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).core s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A : Finset ((i : ι) → G i)
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
by

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

Goal state before:
pp: case refine_5
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
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

Tactic:
· rintro ⟨e, rfl, rfl⟩
    ext1
    apply LinearEquiv.symm_bijective.injective
    ext
    apply e.injective
    ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
⊢ TwoUniqueProds (G × H)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
⊢ p.length + q.length + 1 < p.length + 1 + (q.length + 1)

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 // g ∘ₗ l = LinearMap.id } ≃ { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
⊢ x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
⊢ ↑i < p.length + (q.length + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
⊢ y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ ↑i < p.length + 1 + q.length

Tactic:
by

Goal state after: