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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen 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 c : α
hac : r a c
⊢ ReflTransGen r a a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b 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 : TransGen r x y
⊢ TransGen r y x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ ReflGen r = r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : Std.Refl r'
h : r ≤ r'
⊢ ReflGen r ≤ r'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b : α
h : TransGen r a 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
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : IsTrans α r'
h : r ≤ r'
⊢ TransGen r ≤ r'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (TransGen r) ≤ TransGen (Function.swap r)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
a b : α
h : ReflTransGen r a 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
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
⊢ ReflTransGen r ≤ (ReflTransGen p on f)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (ReflTransGen r) ≤ ReflTransGen (Function.swap r)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflGen (TransGen r) = ReflTransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen (ReflGen r) = ReflTransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (ReflGen r) = ReflTransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (TransGen r) = ReflTransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ ReflTransGen r = TransGen r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflTransGen r = ReflGen r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
⊢ EqvGen r ≤ EqvGen p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : 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:
by

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (SymmGen r) = EqvGen r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x.out ≈ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out ≈ y.out ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid (α i)
⊢ Setoid ((i : ι) → α i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid (α i)
q : Quotient inferInstance
i : ι
x✝¹ x✝ : (i : ι) → α i
h : x✝¹ ≈ x✝
⊢ x✝¹ i ≈ x✝ i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Opposites

Goal state before:
pp: α : Type u_1
inst✝ : Add α
⊢ IsCancelAdd αᵐᵒᵖ ↔ IsCancelAdd α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
h : r' ≤ r
⊢ ReflTransGen r' ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f' (gb x) = ga (f' x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n.succ] = id

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
⊢ e₁ = e₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.7
h : α = β
⊢ LeftInverse (cast ⋯) (cast h)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.7
h : α = β
⊢ RightInverse (cast ⋯) (cast h)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[n.succ] x = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ⇑e = id

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g ∘ f^[0] = g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast h).trans (Equiv.cast h2)) x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h) a = b ↔ a ≍ b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f^[m + 1] = g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ e.symm x = y ↔ x = e y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ y = e.symm x ↔ e y = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ (Equiv.refl α).trans e = e

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.symm.trans e = Equiv.refl β

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans e.symm = Equiv.refl α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
bc : β ≃ γ
cd : γ ≃ δ
⊢ (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ f = e.symm.trans g

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ e = g.trans f.symm

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
⊢ Semiconj f^[n] (g k) (g (n + k))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' b = g (f.symm b)

Tactic:
by

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

Goal state before:
pp: α : Type u
f g : α → α
h : Commute f g
n✝ : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[n.succ] x = g^[n.succ] x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun bd ↦ ab.trans (bd.trans cd.symm)) ((fun ac ↦ (ab.symm.trans ac).trans cd) ac) = ac

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
⊢ (fun ac ↦ (ab.symm.trans ac).trans cd) ((fun bd ↦ ab.trans (bd.trans cd.symm)) ac) = ac

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Tactic:
by

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

Goal state before:
pp: α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ e.permCongr (Equiv.refl α') = Equiv.refl β'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
x : α
⊢ f^[n.succ] x = f (f^[n] x)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
⊢ (fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) ((fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
⊢ (fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) ((fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[n.pred] = f^[n]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ (ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
f₁ f₂ : α → α
⊢ e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

Tactic:
by

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

Goal state before:
pp: α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[n.succ] f^[n.succ]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f = g.symm

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f.symm = g

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : Prop
⊢ (fun b ↦ b = true) ((fun p ↦ decide p) p) = p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun p ↦ decide p) ((fun b ↦ b = true) b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type ?u.16
e : α₁ ≃ α₂
x✝ : (a : α₁) × β (e a)
a : α₁
b : β (e a)
⊢ (fun a ↦ ⟨e.symm a.fst, ⋯ ▸ a.snd⟩) ((fun a ↦ ⟨e a.fst, a.snd⟩) ⟨a, b⟩) = ⟨a, b⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type ?u.16
e : α₁ ≃ α₂
x✝ : (a : α₂) × β a
a : α₂
b : β a
⊢ (fun a ↦ ⟨e a.fst, a.snd⟩) ((fun a ↦ ⟨e.symm a.fst, ⋯ ▸ a.snd⟩) ⟨a, b⟩) = ⟨a, b⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h : ∀ (a : α), q (e a)
a : β
⊢ q a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝ : ∃ b, q b
a : β
h : q a
⊢ q (e (e.symm a))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃ a, p a) ↔ ∃ b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝¹ : α
x✝ : q (e x✝¹)
⊢ ∀ (a : α), q (e a) → a = x✝¹ ↔ q (e a) → e a = e x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α),
    ((fun a ↦ q (e a)) a ∧ ∀ (y : α), (fun a ↦ q (e a)) y → y = a) ↔
      (fun b ↦ q b) (e a) ∧ ∀ (y : β), (fun b ↦ q b) y → y = e a

Tactic:
by

Goal state after: