mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
⊢ Injective g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
x y : α
⊢ (fun x_1 ↦ (g x_1).getD x) (f y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
⊢ IsPartialInv (h ∘ f) fun x ↦ (i x).bind g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
b : β
h : ∃ a, f a = b
⊢ f (invFun f b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
⊢ (Surjective fun x ↦ g ∘ x) ↔ Surjective g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ f₂ : α → β
hf : f₁ = f₂
a'₁ a'₂ : α
ha' : a'₁ = a'₂
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₂ a'₂ v₂ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ update f a b = f ↔ b = f a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ f = update f a b ↔ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
α : κ → Sort u_3
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
ctor : ι → κ
x✝ : Injective ctor
recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i
h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i
h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k
f : (i : ι) → α (ctor i)
i : ι
x : α (ctor i)
⊢ recursor (update f i x) = update (recursor f) (ctor i) x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k ↦ f k (g k) (h k)) i (f i v w) j

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
P : ⦃a : α⦄ → β a → Prop
f : (a : α) → β a
a' : α
v : β a'
a : α
⊢ P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
⊢ Pi.map f (update g i a) = update (Pi.map f g) i (f i a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
⊢ extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ g x✝¹ = g x✝

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g ↦ extend f g e'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
⊢ (Surjective fun g ↦ g ∘ f) ↔ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g ↦ g ∘ f) (g ∘ surjInv ⋯) = g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
⊢ curry (update f aa' b) = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
f : α → α
⊢ (Std.Symm fun x1 x2 ↦ f x1 = x2) ↔ Involutive f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 ↦ f x1 = x2

Tactic:
by

Goal state after:
Module: Mathlib.Data.FunLike.Equiv

Goal state before:
pp: E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a ↔ b = e a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ r = fun x1 x2 ↦ f x1 = x2

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mp

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mpr

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective (cast h)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ C (g (f a)) ≍ C a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast ⋯ (C (g (f a))) = C a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
⊢ B.SeparatesPoints

Tactic:
by

Goal state after:
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ ⇑f = ⇑g

Tactic:
by

Goal state after:
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
⊢ (if h : P then f h else g h) x = if h : P then (f h) x else (g h) x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Refl r
x y : α
hr : x ≠ y → r x y
⊢ r x y

Tactic:
grind [Std.Refl]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Refl r
x y : α
hr : x ≠ y → r x y
⊢ r x y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r

Tactic:
grind [Std.Refl]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ r ≤ Ne

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
⊢ (r ∘r fun x1 x2 ↦ x1 = f x2) = fun x1 x2 ↦ r x1 (f x2)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
⊢ (fun x1 x2 ↦ f x1 = x2) ∘r r = fun x ↦ r (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : Prop → α → Prop
⊢ (fun x1 x2 ↦ x1 ↔ x2) ∘r r = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → Prop → Prop
⊢ (r ∘r fun x1 x2 ↦ x1 ↔ x2) = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')

Tactic:
exact ih a' hr'

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
rβ : β → β → Prop
f : α → β
dc : ∀ {a : α} {b : β}, rβ b (f a) → ∃ c, f c = b
a✝ : α
ha : Acc (InvImage rβ f) a✝
a : α
x✝ : β
h : rβ x✝ (f a)
a' : α
he : f a' = x✝
⊢ InvImage rβ f a' a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Injective f
hg : Injective g
r : α → β → Prop
a : α
b : β
⊢ Relation.Map r f g (f a) (g b) ↔ r a b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Relation.Map r id id = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : α → β
hf : Surjective f
x : β
⊢ Relation.Map r f f x x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r✝ : α → β → Prop
f✝ : α → γ
g : β → δ
c : γ
d : δ
r : α → α → Prop
inst✝ : Std.Symm r
f : α → β
x✝¹ x✝ : β
⊢ Relation.Map r f f x✝¹ x✝ → Relation.Map r f f x✝ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
⊢ IsTrans β (Relation.Map r f f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ r ≤ (Relation.Map r f f on f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
hinj : Injective f
⊢ (Relation.Map r f f on f) = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ Relation.Map (r on f) f f ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
⊢ Relation.Map (r on f) f f = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ (Relation.Map (r on f) f f on f) = (r on f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
a₁ a₂ : α
⊢ Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hp : r ≤ p
a : α
⊢ ReflGen p a a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : ReflGen r b c
⊢ ReflGen r a c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : SymmGen r b a
⊢ SymmGen (Function.swap r) a b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p q : α → Prop
h : ∀ (x : α), p x ↔ q x
a1 : { x // p x }
a2 : { x // q x }
⊢ ∀ (a2' : { x // p x }), a1 ≍ a2' ↔ ↑a1 = ↑a2'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x // p x }
b : { y // q y }
h : α = β
h' : p ≍ q
⊢ a ≍ b ↔ ↑a ≍ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : α
h : p a
a' : α
h' : p a'
⊢ ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : { a // p a }
b : α
⊢ ↑a = b ↔ ∃ h, a = ⟨b, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ h, ⟨b, h⟩ = a) ↔ b = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: β : Sort u_2
γ : Sort u_3
p : β → Prop
g : { x // p x } → γ
j : β → γ
b : β
hb : ¬p b
⊢ extend val g j b = j b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict p f x = f ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
f : (x : Subtype p) → β ↑x
⊢ ((fun f ↦ restrict p f) fun x ↦ if h : p x then f ⟨x, h⟩ else ⋯.some) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f ↦ restrict p f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_4
β : Sort u_5
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : coind f h x = coind f h y
⊢ f x = f y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ ReflTransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → TransGen r a b → Prop
a : α
h : TransGen r a b
single : ∀ {a : α} (h : r a b), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
by

Goal state after: